The need to specify 'rec' in a recursive function defintion
[
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:  20100210 (07:19) 
From:  Andrej Bauer <andrej.bauer@a...> 
Subject:  Re: [Camllist] The need to specify 'rec' in a recursive function defintion 
On Tue, Feb 9, 2010 at 11:01 PM, Gerd Stolpmann <gerd@gerdstolpmann.de> wrote: > For defining the operational meaning of a recursive function a special > helper is needed, the Ycombinator. It gets quite complicated here from > a theoretical point of view because the Ycombinator 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 fixedpoint 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 lambdacalculus definition of y, which gets us recursion out of nothing isn't typeable because selfapplication 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 nonrecursive 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