From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA13967; Mon, 24 Mar 2003 17:06:42 +0100 (MET) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id RAA13469 for ; Mon, 24 Mar 2003 17:06:40 +0100 (MET) Received: from nef.ens.fr (nef.ens.fr [129.199.96.32]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h2OG6eX03403 for ; Mon, 24 Mar 2003 17:06:40 +0100 (MET) Received: from dmi.ens.fr (dmi.ens.fr [129.199.96.11]) by nef.ens.fr (8.12.8/1.01.28121999) with ESMTP id h2OG6XqZ074211 ; Mon, 24 Mar 2003 17:06:33 +0100 (CET) Received: from basilic.ens.fr (monniaux@basilic [129.199.99.48]) by dmi.ens.fr (8.10.1/jb-1.3-180200) id h2OG6W709389 ; Mon, 24 Mar 2003 17:06:32 +0100 (MET) Received: from localhost (monniaux@localhost) by basilic.ens.fr (8.11.0/jb-1.1) id h2OG6UW10459 ; Mon, 24 Mar 2003 17:06:30 +0100 (MET) X-Authentication-Warning: basilic.ens.fr: monniaux owned process doing -bs Date: Mon, 24 Mar 2003 17:06:30 +0100 (MET) From: David Monniaux X-Sender: monniaux@basilic.ens.fr To: Damien cc: caml-list@inria.fr Subject: Re: [Caml-list] beta-reduction rules In-Reply-To: <20030324140858.592550a5.Damien.Pous@ens-lyon.fr> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=ISO-8859-1 Content-Transfer-Encoding: 8BIT X-Spam: no; 0.00; monniaux:01 caml-list:01 damien:01 val:01 'a-:01 evaluates:01 closure:01 rec:01 exception:02 uncaught:02 wrote:03 let:04 l'ecole:04 raise:05 meant:05 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Mon, 24 Mar 2003, Damien wrote: > I expected f0, f1 and f2 to be equivalent, No, they are not. To speak in a pretentious way: properties involving side effects or non-termination are NOT preserved by eta-expansion. Incomplete applications may yield different results. In your example: # let g f i = f i;; val g : ('a -> 'b) -> 'a -> 'b = # let rec f0 x = fun i -> (f0 x) i;; (* I assume you meant f0 here *) val f0 : 'a -> 'b -> 'c = # let rec f1 x i = (f1 x) i;; val f1 : 'a -> 'b -> 'c = # let rec f2 x = g (f2 x);; val f2 : 'a -> 'b -> 'c = f0 and f1 are equivalent up to syntactic sugar. f2 is *NOT* equivalent. Let me show you the evaluation chains: f1 () evaluates to a closure representing fun i -> ... f2 () starts looping. Compare: # let rec f x i = f x i;; val f : 'a -> 'b -> 'c = # let rec g x = ((g x) : 'a->'b);; val g : 'a -> 'b -> 'c = f 4 5 and g 4 5 do not terminate. f 4 terminates (and yields a closure) while g 5 does not terminate. Compare: # let f x y = raise Exit;; val f : 'a -> 'b -> 'c = # let g x = raise Exit; fun y -> raise Exit;; val g : 'a -> 'b -> 'c = Complete applications are equivalent: f () () and g () () yield an uncaught exception. Incomplete applications are *not* equivalent: f () yields a function while g () yields an uncaught exception. > Is it a normal feature ? Yes, it is normal in an eager functional programming language. David Monniaux http://www.di.ens.fr/~monniaux Laboratoire d'informatique de l'École Normale Supérieure, Paris, France ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners