Path: utzoo!attcan!uunet!mcsun!ukc!sys.uea!jrk
From: jrk@sys.uea.ac.uk (Richard Kennaway CMP RA)
Newsgroups: comp.lang.functional
Subject: Re: Purity and Laziness
Message-ID: <1555@sys.uea.ac.uk>
Date: 7 Jun 90 10:53:13 GMT
References: <8691@cs.utexas.edu> <1990May25.024023.10616@comp.vuw.ac.nz> <1535@sys.uea.ac.uk> <3417@rex.cs.tulane.edu>
Organization: UEA, Norwich, UK
Lines: 70

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