🚀 go-pugleaf

In article <1990May25.024023.10616@comp.vuw.ac.nz> brian@comp.vuw.ac.nz (Brian Boutel) writes:
>In article <4170@castle.ed.ac.uk>, nick@lfcs.ed.ac.uk (Nick Rothwell) writes:
>> Correct me if I'm wrong (more than likely...) but in a lazy language
>> I can write things like
>> 
>> 	fun f x = cons(1, f x)
>> 
>> to build an infinite list, but not
>> 
>> 	fun f x = reverse_cons(f x, 1)
>> 
>> because of the reduction order.
>> 
>> So it strikes me that lazy evaluation has this implicit evaluation
>> order (with different termination characteristics) which is left
>> to right. Eager evaluation is purer because it doesn't; if you have
>> an infinite computation it hangs regardless.

It's not lazy evaluation which has this evaluation order, but the
so-called lazy languages.  I regard this as a defect, precisely because
it fails to be lazy.  An eager language, in contrast, is uniformly bad
in this respect.  I find the absence of laziness in a functional
language as irksome as the absence of recursion would be in imperative
languages.

>Lazy evaluation *will* allow your reverse_cons example. All the
>arguments of functions and constructors are passed unevaluated.
...
> --brian


> || It's not quite as simple as that.

(This is jrk speaking, from here on the ">" doesnt indicate quoting.
The reason will eventually become clear.)

Although the reverse_cons example doesnt cause problems, other examples do.
Consider the following definitions:

>    list  ::=  Nil  |  Cons num list

>    f Nil Nil           =   1 
>    f Nil (Cons x y)    =   2
>    f (Cons x y) z      =   3

>    g Nil Nil           =   1
>    g (Cons x y) Nil    =   2
>    g z (Cons x y)      =   3

>    loop                =   loop

This is Miranda, but the point can be made in any of the supposedly lazy
functional languages I know.  

Notice that f and g are nearly the same function, but they take their
arguments in the opposite order.  Now consider the two expressions

>   test1   =   f (Cons 1 Nil) loop

and

>   test2   =   g loop (Cons 1 Nil)

test1 evaluates to 3.  Therefore so should test2, right?  But it gives a
non-terminating computation instead.

Functional languages are supposed to have the advantage that a functional
program can be read as a piece of mathematics, to which ordinary
mathematical reasoning can be applied to prove properties of a program.  No
separate proof-theoretic apparatus should be required.  For languages such
as Miranda, ML, Haskell, etc. this means that one should be able to read a
program such as the above as a set of equational axioms.  "Evaluating" a
term is done by using those axioms to prove the term equal to some term
which has a printable representation.

With the above axioms, it is easy to prove test1 and test2 both equal to 3
(and perhaps less obviously, it is impossible to prove either equal to any
other printable value).  Miranda does this with test1, but fails with
test2.  Therefore Miranda is not fully lazy.

Every other functional language I have seen would do at least as badly
(some might fail to compute test1 as well).

The reason for this behaviour is that Miranda adopts a specific evaluation
strategy for any program, which may be summed up as "left to right, top to
bottom".  The evaluation of test 2 first applies the only rule for test2,
replacing it by g loop (Cons 1 Nil).  It then tries the first rule for g. 
If it tried to match the second argument of the rule (which is Nil) with
the second argument of the term (which is (Cons 1 Nil)), the match would
fail and the pattern-matcher could go on to try the second rule, which
would also fail, and then the third, which would succeed and give the final
result 3.  However, pattern-matching in Miranda always goes from left to
right.  In trying to match the first rule for g against (g loop (Cons 1
Nil)), it tries to match Nil against loop.  Seeing that there is a rule for
loop, it applies it, getting the same term again, and goes into an infinite
loop.

I discuss all this at even greater length in a paper presented at the ESOP
conference last week (Springer LNCS 432), but the basic algorithm for
dealing properly with systems like the above has been known for eleven
years (see Huet & Levy "Call by need computations in non-ambiguous linear
term rewriting systems", INRIA report 359, 1979).

BTW, if you have a Miranda implementation, you can give it the whole of
this message, starting at the line which begins "> ||", and see the example
behave as described.

--
Richard Kennaway          SYS, University of East Anglia, Norwich, U.K.
Internet:  jrk@sys.uea.ac.uk            uucp:  ...mcvax!ukc!uea-sys!jrk