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

[skaller <skaller@users.sourceforge.net>]

On Fri, 2004-07-23 at 02:28, Pierre Weis wrote:

> In my mind, this idea would be a type-based transformation of the
> source code. The typing rule for lazy function application would be:
> 
> |~ -: (f : 'a lazy -> 'b) (e : 'a)
> ----------------------------------  (lazy app)
>            |~ -: (f e : 'b)
> 
> and the transformation rule on the type annotated abstract syntax
> trees would be:
> 
> (f : 'a lazy -> b) (e : 'a) => (f : 'a lazy -> b) (lazy e : 'a lazy)
> 
> Interestingly enough, the typing rule implies that you not only can
> omit the lazy keyword at application time: it would be mandatory to
> omit it! Weel, not so bad, after all ...
> 
> This has to be precisely ruled out and the necessary proofs have to be
> made, but I think it could work (including for higher-order
> functional, map, fold, and so on). I mean, I don't see any trivial
> counter-example that would ruin this scheme. Wao! If this rule
> turned out to be usable, it would be a major improvement for lazy
> evaluation in our favorite language.

But this looks very dangerous!

Its kind of like reference parameters in C++, which make
it impossible to tell if  f(expr) can modifiy expr or not
[without finding which 'f' it is and examining it]

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. 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 even if your rule is sound, it might not be a good idea
because it breaks 'the substitution principle'.

How about sugar:

\(expr) <==> lazy expr

Since arguments to be lazily evaluated are never variables,
they're often going to be surrounded in brackets already, 
and so this is only a single character .. 
a lazy way to spell lazy  .. and a very easy implementation :)

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net



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