[Camllist] kprintf with user formatters
[
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:  20040728 (10:18) 
From:  Jason Smith <jns28@s...> 
Subject:  Re: lazyness in ocaml (was : [Camllist] kprintf with user formatters) 
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 nonissue. 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 == <M>E{x > a} where a = <N>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 sideeffects this complicates the operational semantics (and invalidates equivalences in the denotational semantics), because sideeffects 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 sideeffects, 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 camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners