Linearity Requirement for Patterns

[Fergus Henderson]

On 22-Mar-2001, Koen Claessen <koen@cs.chalmers.se> wrote:
> Michael Hanus wrote:
> 
>  | For instance, the meaning of the definition
>  |
>  |   h = let x = f y in g x x
>  |
>  | is defined as an abbreviation for the rules
>  |
>  |   h = aux (f y)
>  |   aux x = g x x
>  |
>  | W.r.t. this semantics, there is no problem even with
>  | non-deterministic functions.
> 
> In ML, the meaning of the expression:
> 
>   let x = e1 in e2
> 
> is defined as an abbreviation for the expression
> 
>   mdo x <- e1; e2
> 
> W.r.t. this semantics, there is no problem even with
> side-effecting functions.

Referential transparency is a *syntactic* property of a language.  You can
define two languages with very similar semantics, and a well-defined
translation that maps one to the other (and vice versa), the only difference
being some syntactic sugar, and yet one can be referentially transparent and
the other not.

So I don't think it is reasonable to say that either of those languages are
referentially transparent by virtue of the existence of some transformation or
some rules for how to expand syntactic sugar for which the result of the
transformation is referentially transparent.  In general such transformations
don't necessarily preserve referential transparency.

On the other hand, another conclusion that you could draw from this is that
referential transparency is not such an important property; it's a means, not
an end.  Really what we care about is whether the languages that we use
are easy to understand, have a simple semantics, and are easy to transform.
Languages which are referentially transparent *tend* to have those properties,
but this is not necessarily the case.

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.