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 LAA06239; Wed, 28 Jul 2004 11:13:06 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 LAA06656; Wed, 28 Jul 2004 11:13:05 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.12.10/8.12.10) with ESMTP id i6S9D4EV013053; Wed, 28 Jul 2004 11:13:04 +0200 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA04589; Wed, 28 Jul 2004 11:13:04 +0200 (MET DST) From: Pierre Weis Message-Id: <200407280913.LAA04589@pauillac.inria.fr> Subject: Re: lazyness in ocaml (was : [Caml-list] kprintf with user formatters) In-Reply-To: <1091001993.5870.891.camel@pelican.wigram> from skaller at "Jul 28, 104 06:06:33 pm" To: skaller@users.sourceforge.net Date: Wed, 28 Jul 2004 11:13:04 +0200 (MET DST) Cc: pierre.weis@inria.fr, daniel.buenzli@epfl.ch, caml-list@inria.fr X-Mailer: ELM [version 2.4ME+ PL28 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41076E20.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; pierre:01 weis:01 pierre:01 weis:01 lazyness:01 caml-list:01 kprintf:01 formatters:01 2004:99 expr:01 expr:01 f'':01 parlance:01 flamewar:01 failwith:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > On Wed, 2004-07-28 at 17:26, Pierre Weis wrote: > > > There is nothing such as your ``substitution principle'' in Caml, > > except if we restrict the language to truly trivial expressions (as > > soon as expressions may incoporate basic operators such as the integer > > addition your ``principle'' does not stand anymore). > > I thought: > > let x = expr in f x > > and > > f expr > > are identical in all circumstances in Ocaml > for all terms 'expr', I must have missed > something .. do you have a counter example? We have to precisely state the statement here: - if you mean that ``f'' is just an ident (more precisely, a lowercase ident in the Caml parser parlance) bound to a unary function, then the two expressions are equivalent. - if f can have more than one argument, then the two expressions are obviously not equivalent since the first one fixes the order of evaluation when the second does not. This is true in particular if f is ( + ): let x = expr in expr2 + x and expr2 + x may not evaluate the same (depending on the compiler: a lot of flamewar already occurred on this list about that feature). - if f can be more than a lowercase ident and in particular if f can introduce a lazy construction, then the two expressions are not equivalent (as desired), since the first one explicitely evaluates expr when the second may not. Consider f being ``lazy'' and expr being ``failwith "evaluated"'': # let x = failwith "evaluated" in lazy x;; Exception: Failure "evaluated". # lazy (failwith "evaluated");; - : 'a lazy_t = Here, you check again that lazy evaluation just breaks the eagerness of the language (and hence breaks your ``identity'' a bit more): lazyness changes the default evaluation regime, just as desired. It's no surprise, something has changed after the introduction of lazyness! What I propose is a smoother interaction with the rest of the language with the (re)-introduction of lazy constructors, lazy labels and a new typing (and compilation) rule to facilitate the use of lazy functions. Best regards, Pierre Weis INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/ ------------------- 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