How do I define y-combinator without "let rec"?

Question

In almost all examples, a y-combinator in ML-type languages is written like this:

let rec y f x = f (y f) x
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1))

This works as expected, but it feels like cheating to define the y-combinator using let rec ....

I want to define this combinator without using recursion, using the standard definition:

Y = λf·(λx·f (x x)) (λx·f (x x))

A direct translation is as follows:

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;

However, F# complains that it can't figure out the types:

  let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;
  --------------------------------^

C:\Users\Juliet\AppData\Local\Temp\stdin(6,33): error FS0001: Type mismatch. Expecting a
    'a    
but given a
    'a -> 'b    
The resulting type would be infinite when unifying ''a' and ''a -> 'b'

How do I write the y-combinator in F# without using let rec ...?

Answer 1

I would say it's impossible, and asked why, I would handwave and invoke the fact that simply typed lambda calculus has the normalization property. In short, all terms of the simply typed lambda calculus terminate (consequently Y can not be defined in the simply typed lambda calculus).

F#'s type system is not exactly the type system of simply typed lambda calculus, but it's close enough. F# without let rec comes really close to the simply typed lambda calculus -- and, to reiterate, in that language you cannot define a term that does not terminate, and that excludes defining Y too.

In other words, in F#, "let rec" needs to be a language primitive at the very least because even if you were able to define it from the other primitives, you would not be able to type this definition. Having it as a primitive allows you, among other things, to give a special type to that primitive.

EDIT: kvb shows in his answer that type definitions (one of the features absent from the simply typed lambda-calculus but present in let-rec-less F#) allow to get some sort of recursion. Very clever.

Answer 2

As the compiler points out, there is no type that can be assigned to x so that the expression (x x) is well-typed (this isn't strictly true; you can explicitly type x as obj->_ - see my last paragraph). You can work around this issue by declaring a recursive type so that a very similar expression will work:

type 'a Rec = Rec of ('a Rec -> 'a)

Now the Y-combinator can be written as:

let y f =
  let f' (Rec x as rx) = f (x rx)
  f' (Rec f')

Unfortunately, you'll find that this isn't very useful because F# is a strict language, so any function that you try to define using this combinator will cause a stack overflow. Instead, you need to use the applicative-order version of the Y-combinator (\f.(\x.f(\y.(x x)y))(\x.f(\y.(x x)y))):

let y f =
  let f' (Rec x as rx) = f (fun y -> x rx y)
  f' (Rec f')

Another option would be to use explicit laziness to define the normal-order Y-combinator:

type 'a Rec = Rec of ('a Rec -> 'a Lazy)
let y f =
  let f' (Rec x as rx) = lazy f (x rx)
  (f' (Rec f')).Value

This has the disadvantage that recursive function definitions now need an explicit force of the lazy value (using the Value property):

let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1)))

However, it has the advantage that you can define non-function recursive values, just as you could in a lazy language:

let ones = y (fun ones -> LazyList.consf 1 (fun () -> ones.Value))

As a final alternative, you can try to better approximate the untyped lambda calculus by using boxing and downcasting. This would give you (again using the applicative-order version of the Y-combinator):

let y f =
  let f' (x:obj -> _) = f (fun y -> x x y)
  f' (fun x -> f' (x :?> _))

This has the obvious disadvantage that it will cause unneeded boxing and unboxing, but at least this is entirely internal to the implementation and will never actually lead to failure at runtime.

Answer 3

Case and let statements in ML derivatives are what makes it Turing Complete, I believe they're based on System F and not simply typed but the point is the same.

System F cannot find a type for the any fixed point combinator, if it could, it wasn't strongly normalizing.

What strongly normalizing means is that any expression has exactly one normal form, where a normal form is an expression that cannot be reduced any further, this differs from untyped where every expression has at max one normal form, it can also have no normal form at all.

If typed lambda calculi could construct a fixed point operator in what ever way, it was quite possible for an expression to have no normal form.

Another famous theorem, the Halting Problem, implies that strongly normalizing languages are not Turing complete, it says that's impossible to decide (different than prove) of a turing complete language what subset of its programs will halt on what input. If a language is strongly normalizing, it's decidable if it halts, namely it always halts. Our algorithm to decide this is the program: true;.

To solve this, ML-derivatives extend System-F with case and let (rec) to overcome this. Functions can thus refer to themselves in their definitions again, making them in effect no lambda calculi at all any more, it's no longer possible to rely on anonymous functions alone for all computable functions. They can thus again enter infinite loops and regain their turing-completeness.