From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 4BA19BC37 for ; Wed, 10 Feb 2010 08:19:11 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ar4BACvtcUvRVdzgkGdsb2JhbACDCZAMh0gIFQEBAQEJCQwHEwMgrD6QGYEvgktbBA X-IronPort-AV: E=Sophos;i="4.49,442,1262559600"; d="scan'208";a="44220370" Received: from mail-fx0-f224.google.com ([209.85.220.224]) by mail2-smtp-roc.national.inria.fr with ESMTP; 10 Feb 2010 08:19:11 +0100 Received: by fxm24 with SMTP id 24so78176fxm.3 for ; Tue, 09 Feb 2010 23:19:10 -0800 (PST) MIME-Version: 1.0 Received: by 10.87.71.30 with SMTP id y30mr2209485fgk.58.1265786350563; Tue, 09 Feb 2010 23:19:10 -0800 (PST) In-Reply-To: <1265752863.5482.42.camel@flake.lan.gerd-stolpmann.de> References: <1e7471d51002091250of7a686fq537a03c9401c868f@mail.gmail.com> <1265752863.5482.42.camel@flake.lan.gerd-stolpmann.de> Date: Wed, 10 Feb 2010 08:19:10 +0100 Message-ID: <7d8707de1002092319j4d6bfca5s169914a992d57be2@mail.gmail.com> Subject: Re: [Caml-list] The need to specify 'rec' in a recursive function defintion From: Andrej Bauer To: Gerd Stolpmann Cc: saptarshi.guha@gmail.com, caml-list@yquem.inria.fr Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; recursive:01 defintion:01 andrej:01 andrej:01 gerd:01 stolpmann:01 gerd:01 recursive:01 typable:01 combinator:01 expr:01 recursion:01 val:01 val:01 untyped:01 On Tue, Feb 9, 2010 at 11:01 PM, Gerd Stolpmann wr= ote: > 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 > =C2=A0 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 typ= e is ('a -> 'a) -> 'a or if we only care about recursive functions it is: # let rec y f x =3D f (y f) x ;; val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b =3D (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 =3D y (fun f n -> if n =3D 0 then 1 else n * f (n - 1)) ;; val fac : int -> int =3D # fac 7 ;; - : int =3D 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 =3D fun u v w -> v (u u v) w ;; val z : ('a -> ('b -> 'c -> 'd) -> 'b as 'a) -> ('b -> 'c -> 'd) -> 'c -> 'd =3D # let y =3D z z ;; val y : (('_a -> '_b) -> '_a -> '_b) -> '_a -> '_b =3D 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 =3D y (fun f n -> if n =3D 0 then 1 else n * f (n - 1)) ;; val fac : int -> int =3D # fac 7 ;; - : int =3D 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