Re: lazyness in ocaml (was : [Caml-list] kprintf with user formatters)

[Jason Smith <jns28@student.canterbury.ac.nz>]

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 == <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 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