Re: [Caml-list] The need to specify 'rec' in a recursive function defintion

[Andrej Bauer <andrej.bauer@andrej.com>]

On Tue, Feb 9, 2010 at 11:01 PM, Gerd Stolpmann <gerd@gerd-stolpmann.de> wrote:
> For defining the operational meaning of a recursive function a special
> helper is needed, the Y-combinator. It gets quite complicated here from
> a theoretical point of view because the Y-combinator is not typable. But
> generally, the idea is to have a combinator y that can be applied to a
> function like
>   y (fun f arg -> expr) arg
> and that "runs" this function recursively, where "f" is the recursion.

A small correction: y is typeable. It's a fixed-point operator, so it's type is

('a -> 'a) -> 'a

or if we only care about recursive functions it is:

# let rec y f x = f (y f) x ;;
val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>

(Yes, I know I used "let rec", it doesn't matter for checking that y
has a type). Let's check that it works:

# let fac = y (fun f n -> if n = 0 then 1 else n * f (n - 1)) ;;
val fac : int -> int = <fun>

# fac 7 ;;
- : int = 5040

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. But
again, it's an intermediate definition that is not typeable, not y
itself (here adapted so that it works for functions in an eager
language):

$ ocaml -rectypes
        Objective Caml version 3.11.1

# let z = fun u v w -> v (u u v) w ;;
val z : ('a -> ('b -> 'c -> 'd) -> 'b as 'a) -> ('b -> 'c -> 'd) -> 'c
-> 'd = <fun>

# let y = z z ;;
val y : (('_a -> '_b) -> '_a -> '_b) -> '_a -> '_b = <fun>

Observe that y has a non-recursive type, it's the auxiliary z that
requires a recursive one. And this y also works:

# let fac = y (fun f n -> if n = 0 then 1 else n * f (n - 1)) ;;
val fac : int -> int = <fun>

# fac 7 ;;
- : int = 5040

Can anyone get rid of the pesky underscores in the type of y above, so
that it becomes truly polymorphic?

With kind regards,

Andrej