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

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Andrej Bauer <Andrej.Bauer@f...> 
Subject:  Re: [Camllist] 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 "socalled 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 curryinguncurrying) 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 fixpoint 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 betareducing: 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 betaeta 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)?