Re: [Caml-list] Unexpected restriction in "let rec" expressions

[Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>]

Loup Vaillant wrote:
> loop :: ((a,c) -> (b,c)) -> a -> b
> loop f a = b
>   where (b,c) = f (a,c)

You said the above was a "so-called fixpoint operator". To see in what 
sense this really is a fixpoint operator consider the type:

   ((a * c) -> (b * c)) -> a -> b                    (1)

It is equivalent (under currying-uncurrying) to

   (a -> (c -> b) * (c -> c)) -> a -> b              (2)

We could write down a term of this type if we had a way of going from
type c -> c to type c. More precisely, consider any term

   fix : (c -> c) -> c,

where the name "fix" suggests that we will plug in a fix-point operator 
at the end of the day. Before reading on, you should try to write down a 
term of type (2), given that we have fix. I will bet that your brain 
will produce the same solution as described below.

We can get a term of type (2) by defining

   let loop' f x =
     let (g, h) = f x in g (fix h)

Converting from (2) back to (1) gives us an equivalent term

   let loop f x =
     let f' y = (fun z -> fst (f (y, z))), (fun z -> snd (f (y, z))) in
       loop' f' x

or by beta-reducing:

   let loop f x =
     fst (f (x, fix (fun z -> snd (f (x, z)))))

You are now free to plug in whatever you wish for fix, but presumably 
you would like fix to compute fixed points. This may be somewhat 
troublesome in an eager language, especially if c is not a function type.

In fact, we may recover fix from loop as follows:

   let fix' f = loop (fun (_, z) -> (z, f z)) ()

To see that fix' is the same as fix, we just beta-eta reduce:

   fix' f =
   loop (fun (_, z) -> (z, f z)) () =
   fst (fix (fun z -> f z), f (fix (fun z -> f z))) =
   fix (fun z -> f z) =
   fix f

Indeed, loop is a generalized fixpoint operator.

But I think the nice picture drawn by Nicolas Pouillard is worth a 
thousand lambda terms.

Best regards,

Andrej

P.S. Can someone think of anything else other than a fixpoint operator 
that we could use in place of fix to get an interesting program (maybe 
for special cases of c, such as c = int -> int)?