Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[Caml-list] kprintf with user formatters
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2004-07-28 (09:13)
From: Pierre Weis <pierre.weis@i...>
Subject: Re: lazyness in ocaml (was : [Caml-list] kprintf with user formatters)
> 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


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

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

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: