"Andrej Bauer" <andrej.bauer@andrej.com> wrote:
>
> What Gerd probably meant was that the usual untyped lambda-calculus
> definition of y, which gets us recursion out of nothing isn't typeable
> because self-application requires unrestricted recursive types.

Fortunately, even that is not quite correct: Y is perfectly typable in
plain ML, you just need to introduce the recursive type it employs
explicitly:

type 'a fix = Fix of ('a fix -> 'a)
let fix f = let z = fun (Fix g' as g) x -> f (g' g) x in z (Fix z)

Now, for example:

let fac = fix (fun fac n -> if n = 0 then 1 else n * fac (n-1))
let n = fac 7

Best,
/Andreas