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 MAA08399; Wed, 28 Jul 2004 12:18:49 +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 MAA08609 for ; Wed, 28 Jul 2004 12:18:48 +0200 (MET DST) Received: from regyva.canterbury.ac.nz (regyva.canterbury.ac.nz [132.181.2.35]) by nez-perce.inria.fr (8.12.10/8.12.10) with ESMTP id i6SAIjEV020249 for ; Wed, 28 Jul 2004 12:18:47 +0200 Received: from CONVERSION-A1.it.canterbury.ac.nz by it.canterbury.ac.nz (PMDF V6.2-X27 #30791) id <01LD0EBL4NB4D182C4@it.canterbury.ac.nz> for caml-list@inria.fr; Wed, 28 Jul 2004 22:18:42 +1200 (NEW ZEALAND STANDARD TIME) Received: from Praxis (Praxis.cosc.canterbury.ac.nz [132.181.9.181]) by it.canterbury.ac.nz (PMDF V6.2-X27 #30791) with SMTP id <01LD0EBKDDWMD0XOWX@it.canterbury.ac.nz> for caml-list@inria.fr; Wed, 28 Jul 2004 22:18:42 +1200 (NEW ZEALAND STANDARD TIME) Date: Wed, 28 Jul 2004 22:17:09 +1200 From: Jason Smith Subject: Re: lazyness in ocaml (was : [Caml-list] kprintf with user formatters) To: caml-list Message-id: <190e01c4748c$0b657b20$b509b584@Praxis> MIME-version: 1.0 X-MIMEOLE: Produced By Microsoft MimeOLE V6.00.2800.1106 X-Mailer: Microsoft Outlook Express 6.00.2800.1106 Content-type: text/plain; charset=iso-8859-1 Content-transfer-encoding: 7bit X-Priority: 3 X-MSMail-priority: Normal References: <200407280726.JAA01775@pauillac.inria.fr> X-Miltered: at nez-perce with ID 41077D85.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; jns:99 canterbury:99 lazyness:01 caml-list:01 kprintf:01 formatters:01 haskell:01 newbie:01 expr:01 expr:01 strictness:01 thunks:01 complained:01 non-issue:01 intuitively:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Hello, first off I come from a Haskell background, and especially ghc so I might be a little off key here, but I thought I'd add my thoughts come what may. Also I'm a newbie so go easy if I'm off base :) (which is more then likely!) > I cannot understand that one. We have that in Caml already and we had > it from the very begining of Caml (1984). For instance, if I write > > f (expr) > > could you tell me ``if f(expr) can modifiy expr or not [without > finding which 'f' it is and examining it]'' ? > > To the best of my knowledge, the answer is no. Well thats kinda what strictness analysis does. If f is going to use the expression then we evaluate it before entering the function so we don't have to pass around THUNKS. But yes we have to know what the 'f' is were playing with. > To the best of my knowledge, nobody never complained about that feature. Its an optimization that is performed regularly in the ghc compiler, and yeah no one complains about its abscence! :) > > > In the lazy case it would destroy an important identity: > > > > f x <==> let x' = x in f x' > > > > With your rule, the LHS might not evaluate x, whereas the RHS > > would. I'm not exactly sure why u defined the substitution principle like this, the syntax should be a non-issue. The way I learned it (from Mitchells excellent book) was the following. The substitution lemma intuitively says that susbtituting a term N for a variable x in M is the same effect on the meaning of M as changing the environment so that the value of x is the value of N. The meaning is what matters, not its syntactic form. If we use just plain alegbra here, where S is the set of sorts, G the environment assigning types to terms, we can define it as given M 'elem' Terms(S, G, x:s'), and N 'elem' Terms(S, G), so that [N/x]M 'elem' Terms(S, G). Then for any environment E, we can say that the denotational meaning (given by the meaning function < >) for each is the same, i.e. <[N/x]M>E == E{x -> a} where a = E is the meaning of N at E. In the above, the meanings of an evaluated expression and an unevaluated expression are as far as I'm aware identical. In the prescence of side-effects this complicates the operational semantics (and invalidates equivalences in the denotational semantics), because side-effects change the storage semantics of the environment and can invalidate the meaning function. For example when we substitute N for x in M, evaluating N may change the meaning of a variable other then x free in M. There are a number of papers by Sullivan and Wand discussing various transformations like lambda lifting in a denotational model based on a operational based term model where interaction is the basic observable, and they don't consider the store as the final part of the congruence proof. Anywayz, the problem with the above is that this equivelence already does not hold in Ocaml'. In Haskell the above identity phrased as it is, would hold, because we don't have side effects. Threading of the world through the IO Monad forces the same evaluation order for both expressions. > Also, I didn't know that such an ``important identity'' stands for > Caml expressions. Except in the trivial case where ``x'' just denotes > a variable in the statment. In this case, the statment still holds with > the new rule :) >>From what I can see yes it is broken because of side-effects, we cannot guarentee that the two phrases are equivalent in the standard denotational semantics. > > Of course we already have that: > > > > f x y <=/=> let x' = x in y' = y in f x' y' > > > > since the RHS guarrantees x is evaluated before y, > > whilst it happens by chance in the current Ocaml implementation > > the reverse is true for the LHS. > > So what? Is the ``important identity'' wrong after all, being wrong in > this case ? Or do you suggest to suppress currying in order to restore > the ``important identity' I'm a bit behind the discussion but I think the original poster was just pointing out that we can impose AOR reduction explicitly by using the let constructs. Cheers, Jason. ------------------- 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