On Tue, Feb 9, 2010 at 11:01 PM, Gerd Stolpmann <g...@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
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
