jrk@sys.uea.ac.uk (Richard Kennaway) (05/25/90)
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
geoffb@butcombe.inmos.co.uk (Geoff Barrett) (05/25/90)
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. If you apply a printing function to the second you might get a "(" on the screen and then the program will hang, but that is to do with the strictness of the printing function. It's the printing function which has defined an evaluation order, in effect. However, if I were to pattern match fun last (reverse_cons(x,a)) = a a call of "last (f x)" should return "1" (BTW, what's that "x" for?). I believe there is an Oxford DPhil thesis by a man called David Turner which pointed out that strict languages are not referentially transparent because of the fact that conditionals are not strict, so that the equality symbol in the definition fun iiff (b,x,y) = if b then x else y is not equality. Lazy evaluation languages are referentially transparent. I think this is what the original poster meant by "purer". > Nick. >-- >Nick Rothwell, Laboratory for Foundations of Computer Science, Edinburgh. > nick@lfcs.ed.ac.uk <Atlantic Ocean>!mcsun!ukc!lfcs!nick >~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ > Ich weiss jetzt was kein Engel weiss Geoff Barrett vvv| |vvv------------------------------------- \ o o / \ / Wot! No Queen's Award logo?
fs@rex.cs.tulane.edu (Frank Silbermann) (05/25/90)
In article <1535@sys.uea.ac.uk> jrk@sys.uea.ac.uk (Richard Kennaway) writes: > > Functional languages are supposed to be readable as mathematics. > For languages such as Miranda, ML, Haskell, etc. this means > that one should be able to read a program such as that below > as a set of equational axioms. > > list ::= Nil | Cons num list > > f Nil Nil = 1 g Nil Nil = 1 > f Nil (Cons x y) = 2 g (Cons x y) Nil = 2 > f (Cons x y) z = 3 g z (Cons x y) = 3 > > loop = loop You are suggesting that the Miranda's semantics should reflect the equational notation. Actually, the logic is not equational; Miranda permits contradictory program clauses, which are resolved by the evaluation order. The clausal notation, which incorporates pattern-matching, is only a syntactic sugar. I find pattern-matching a convenient shortcut when hacking, but when thinking about denotational semantics, I first compile such syntactic sugars out of my examples. > Notice that f and g are nearly the same function, > but they take their arguments in the opposite order. > (The results differ in some cases, therefore Miranda's > evaluation strategy is not quite correct.) Only if you take the syntactic sugars literally. > ... the basic algorithm for dealing _properly_ > with systems like the above ...(can be found in)... Huet & Levy > "Call by need computations in non-ambiguous linear > term rewriting systems", INRIA report 359, 1979. You are advocating a different kind of language. If you want to interpret a Miranda program as a non-ambiguous linear term rewriting system, you will need a way to prevent contradictions in the equations (which Miranda permits). Also, I doubt that the paper you cite takes higher-order functions into consideration. Frank Silbermann fs@rex.cs.tulane.edu Tulane University, New Orleans, Louisianna, U.S.A.
brian@comp.vuw.ac.nz (Brian Boutel) (05/28/90)
In article <1535@sys.uea.ac.uk>, jrk@sys.uea.ac.uk (Richard Kennaway) writes: > 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: [...] > > 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 > > [....] > 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. > [....] > > 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". > I think jrk has done a large issue switch here, but, taking up his point: Every language of this class has to specify the semantics of pattern/equation matching, and do do in a way that will permit efficient implementation. Otherwise, we will all continue to play with functional languages and do our real work in C. It would be highly desirable for Miranda and Haskell to be sufficiently lazy to guarantee that they would never loop/die/bottom while matching equations if there is just one equation which matches the actual arguments. Unfortunately, examples like f x false true = 1 f true x false = 2 f false true x = 3 show that there is no sequential algorithm which will always work. For example, f bot false true matches the first equation and no other, but if, in matching, the first argument is matched first, this will bottom. Similarly for f true bot false if the second argument is matched first, etc. Whatever you try to match first, there is an argument value that will cause non-termination. The only ways to avoid this are a) to outlaw programs like the example, which seem to be otherwise reasonable, or b) to go to parallel evaluation, which is expensive to simulate on a sequential machine. So, if the goal is to define a useful language for real computation, and to have lazy evaluation, it seems that some compromise is necessary. --brian Internet: brian@comp.vuw.ac.nz Postal: Brian Boutel, Computer Science Dept, Victoria University of Wellington, PO Box 600, Wellington, New Zealand Phone: +64 4 721000 Fax: +64 4 712070
smart@ditmela.oz (Robert Smart) (05/28/90)
In article <1990May28.020325.18011@comp.vuw.ac.nz> brian@comp.vuw.ac.nz (Brian Boutel) writes: > b) to go to parallel evaluation, which is expensive to simulate on a > sequential machine. > I'm a complete amateur at this, but I can't believe that parallel evaluation would be as bad as all that in practise. It's not like an operating system where the processes have unknown behaviour and you have to be very fair about sharing time. All you need is for both processes to call a scheduler every now and then. You might start with calling the scheduler every 16th time through a particular calculation point, then move that up to every 32nd, etc. In that way the scheduling cost would always be low in large calculations. Also I really doubt whether there are a lot of cases where a procedure has multiple parameters which might not terminate. Most commonly there will only be one and the compiler should be able to figure out a reasonable heuristic for deciding which patterns to try to match for a given function call. To be popular a language needs to behave in a surprise free fashion. For lazy functional languages that has to mean parallel parameter evaluation when truly necessary. Bob Smart
geoffb@butcombe.inmos.co.uk (Geoff Barrett) (05/29/90)
In article <BJORNL.90Jul26211631@tarpon.tds.kth.se> bjornl@tds.kth.se (Bj|rn Lisper) writes: ]In article <7044@ganymede.inmos.co.uk> geoffb@butcombe.inmos.co.uk (Geoff ]Barrett) writes: ]%I believe there is an Oxford DPhil thesis by a man called David Turner ]%which pointed out that strict languages are not referentially ]%transparent because of the fact that conditionals are not strict, so ]%that the equality symbol in the definition ] ]% fun iiff (b,x,y) = if b then x else y ] ]%is not equality. Lazy evaluation languages are referentially ]%transparent. ] ]Hmmm. How would a lazy language treat a call ] ]if(b,x,x) ] ]where the evaluation of b is non-terminating but the evaluation of x ]terminates? If "naive" left-to-right evaluation order is assumed, the ]computation will not terminate. On the other hand, it is reasonable to ]define the semantics of the if-function so that such a call returns the ]value of x. (After all, the value of x will be the answer regardless of what ]b evaluates to). What about "referential transparency" here? I think I need a good deal of convincing that it would be "reasonable" to define the semantics of "if(b,x,x)" to be "x". But, even so, so long as "iiff (b,x,x)" and "if b then x else x" evaluate to the same thing then the language is still referentially transparent. All I want to be able to do is to substitute equals. ]This problem is akin to left-to-right evaluation sensitivity of goals in ]Prolog; the order of goals that are ANDed together in a Horn clause can ]affect termination even though AND, considered as a "mathematical" binary ]operation, is commutative. One would hope that it is commutative on proper values and obeys the same rules as the "mathematical" operator there. The functions f x = 2*x; g x = x/2 satisfy the rule "f.g = id = g.f" if their domains are restricted to the non-zero real numbers, but not on the whole of the real numbers. Sometimes different functions do satisfy different laws. I think this is what the French might call a "hering rouge". ]Bjorn Lisper Geoff Barrett Newsgroups: comp.lang.functional Subject: Re: Purity and Laziness Summary: Expires: References: <14531@dime.cs.umass.edu> <2535@skye.ed.ac.uk> <8691@cs.utexas.edu> <4170@castle.ed.ac.uk> <7044@ganymede.inmos.co.uk> <BJORNL.90Jul26211631@tarpon.tds.kth.se> Sender: Reply-To: geoffb@inmos.co.uk (Geoff Barrett) Followup-To: Distribution: Organization: INMOS Limited, Bristol, UK. Keywords: In article <BJORNL.90Jul26211631@tarpon.tds.kth.se> bjornl@tds.kth.se (Bj|rn Lisper) writes: ]In article <7044@ganymede.inmos.co.uk> geoffb@butcombe.inmos.co.uk (Geoff ]Barrett) writes: ]%I believe there is an Oxford DPhil thesis by a man called David Turner ]%which pointed out that strict languages are not referentially ]%transparent because of the fact that conditionals are not strict, so ]%that the equality symbol in the definition ] ]% fun iiff (b,x,y) = if b then x else y ] ]%is not equality. Lazy evaluation languages are referentially ]%transparent. ] ]Hmmm. How would a lazy language treat a call ] ]if(b,x,x) ] ]where the evaluation of b is non-terminating but the evaluation of x ]terminates? If "naive" left-to-right evaluation order is assumed, the ]computation will not terminate. On the other hand, it is reasonable to ]define the semantics of the if-function so that such a call returns the ]value of x. (After all, the value of x will be the answer regardless of what ]b evaluates to). What about "referential transparency" here? I think I need a good deal of convincing that it would be "reasonable" to define the semantics of "if(b,x,x)" to be "x". But, even so, so long as "iiff (b,x,x)" and "if b then x else x" evaluate to the same thing then the language is still referentially transparent. All I want to be able to do is to substitute equals. ]This problem is akin to left-to-right evaluation sensitivity of goals in ]Prolog; the order of goals that are ANDed together in a Horn clause can ]affect termination even though AND, considered as a "mathematical" binary ]operation, is commutative. One would hope that it is commutative on proper values and obeys the same rules as the "mathematical" operator there. The functions f x = 2*x; g x = x/2 satisfy the rule "f.g = id = g.f" if their domains are restricted to the non-zero real numbers, but not on the whole of the real numbers. Sometimes different functions do satisfy different laws. I think this is what the French might call a "hering rouge". ]Bjorn Lisper Geoff Barrett vvv| |vvv------------------------------------- \ o o / \ / Wot! No Queen's Award logo? \_/
news@usc.edu (05/30/90)
In article <1990May28.020325.18011@comp.vuw.ac.nz> brian@comp.vuw.ac.nz (Brian Boutel) writes:
It would be highly desirable for Miranda and Haskell to be sufficiently
lazy to guarantee that they would never loop/die/bottom while matching
equations if there is just one equation which matches the actual
arguments. Unfortunately, examples like
. . .
The only ways to avoid this are
a) to outlaw programs like the example, which seem to be otherwise
reasonable, or
b) to go to parallel evaluation, which is expensive to simulate on a
sequential machine.
So, if the goal is to define a useful language for real computation, and
to have lazy evaluation, it seems that some compromise is necessary.
um... I may be way off base here, but I seem to recall some discussion
of this at a recent APL conference (don't remember the ACM SIGAPL
volume, but it was the one in New York). Essentially, they were using
the parallel boolean functions of the language... there is a class of
problems that serial unification does not handle correctly.. this
parallel algorithm dependended on all information being available up
front (self referent problems, such as paradoxes could not be
represented).
A big question was whether there were useful self-referent problems.
The answer to this isn't clear.
Sorry I don't remember the specific reference.. I'll try to find it
and post it.
raulmill@usc.edujrk@sys.uea.ac.uk (Richard Kennaway CMP RA) (06/07/90)
In article <3417@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes: >The clausal notation, which incorporates pattern-matching, >is only a syntactic sugar. I find pattern-matching >a convenient shortcut when hacking, but when thinking about >denotational semantics, I first compile such syntactic sugars >out of my examples. Well, I prefer not to think of them as syntactic sugar. If you define pattern-matching by compilation to lambda calculus, why is that better than taking pattern-matching seriously in its own right? Especially since what the implementation does usually looks more like pattern-matching than lambda calculus. In another message, someone said that lambda calculus has a denotational semantics, and term rewriting doesnt, but surely e.g. the initial algebra stuff of the ADJ group contradicts the latter claim. [quoting and paraphrasing me] >> Notice that f and g are nearly the same function, >> but they take their arguments in the opposite order. >> (The results differ in some cases, therefore Miranda's >> evaluation strategy is not quite correct.) > >Only if you take the syntactic sugars literally. > >> ... the basic algorithm for dealing _properly_ >> with systems like the above ...(can be found in)... Huet & Levy >> "Call by need computations in non-ambiguous linear >> term rewriting systems", INRIA report 359, 1979. > >You are advocating a different kind of language. Agreed. >If you want to interpret a Miranda program as a >non-ambiguous linear term rewriting system, >you will need a way to prevent contradictions in the equations >(which Miranda permits). Also, I doubt that the paper you cite >takes higher-order functions into consideration. Another way of interpreting Miranda-style pattern-matching, studied by Alain Laville, is to compile the ordered pattern-matching of Miranda into a set of disjoint rules, in which the order of pattern matching does not matter. (He actually considered ML, but the same problems arise.) In other words, ordered pattern-matching is taken to be syntactic sugar, to be defined by translating to unordered pattern-matching of conflict-free rule-systems, which is considered meaningful in its own right. (I admit that this is open to the same criticism that I levelled above against translation to lambda calculus: one is explaining ordered p-m by translation to unordered consistent p-m, but then just implementing ordered p-m...) I'm not sure what you meant above by "higher order functions". In my f/g example: >> f Nil Nil = 1 g Nil Nil = 1 >> f Nil (Cons x y) = 2 g (Cons x y) Nil = 2 >> f (Cons x y) z = 3 g z (Cons x y) = 3 if I apply f to Nil, I get a function which maps Nil to 1 and (Cons ? ?) to 2. I can also define the argument-switching combinator: c x y z = x z y (with which one might express one's expectation about the relation between f and g as "c f = g") and the whole system still falls within the ambit of the Huet-Levy paper. Is this higher-order enough for you? -- Richard Kennaway SYS, University of East Anglia, Norwich, U.K. Internet: jrk@sys.uea.ac.uk uucp: ...mcvax!ukc!uea-sys!jrk
bjornl@tds.kth.se (Bj|rn Lisper) (07/27/90)
In article <7044@ganymede.inmos.co.uk> geoffb@butcombe.inmos.co.uk (Geoff Barrett) writes: %I believe there is an Oxford DPhil thesis by a man called David Turner %which pointed out that strict languages are not referentially %transparent because of the fact that conditionals are not strict, so %that the equality symbol in the definition % fun iiff (b,x,y) = if b then x else y %is not equality. Lazy evaluation languages are referentially %transparent. I think this is what the original poster meant by %"purer". Hmmm. How would a lazy language treat a call if(b,x,x) where the evaluation of b is non-terminating but the evaluation of x terminates? If "naive" left-to-right evaluation order is assumed, the computation will not terminate. On the other hand, it is reasonable to define the semantics of the if-function so that such a call returns the value of x. (After all, the value of x will be the answer regardless of what b evaluates to). What about "referential transparency" here? This problem is akin to left-to-right evaluation sensitivity of goals in Prolog; the order of goals that are ANDed together in a Horn clause can affect termination even though AND, considered as a "mathematical" binary operation, is commutative. Bjorn Lisper