This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Unexpected restriction in "let rec" expressions
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2008-02-27 (08:55) From: Andrej Bauer Subject: Re: [Caml-list] Unexpected restriction in "let rec" expressions
```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)?

```