Linearity Requirement for Patterns

Michael Hanus
Thu, 22 Mar 2001 09:46:26 +0100 (MET)

Fergus Henderson wrote:
> My understanding, from talking with Michael Hanus a few years ago, is
> that Curry is not referentially transparent, in the sense that you can't
> replace equals with equals, because it permits nondeterministic functions.
> In particular, `let x = f y in g x x' is not the same as `g (f y) (f y)'
> in Curry.

Of course, as you already mentioned, one has te be very precise
when talking about referential transparency. In particular, one
has to say what "equals" mean. Otherwise, one could also argue
that Haskell is not referential transparent: if a Haskell program
has a defining equation "f 1 = 1", the expressions "(f 1)" and "1"
might not be identical (if there is another equation like "f x = 0"

In Curry, each defining equation contributes to the semantics
of a function independently of the other equations for the same
function, and the overall goal is to compute all values of
an expression (plus possible substitutions for free variables)
which can be derived from this equational reading of all rules.
In this sense, Curry is refentially transparent (although I have
no formal definition of this notion but only soundness, completeness
and optimality results). Your "counter example" comes from a
misunderstanding of the "let" in Curry. Since the kernel language
is based lazy evaluation w.r.t. a set of constructor-based rewrite
rules, the "let" is considered as syntactic sugar for abbreviating
some function argument. 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

If you have a precise definition of "referentially transparent"
at hand so that you can make your statement more precise, I would
be very interested to read it. As you have seen, the slogan
"replacing equals by equals" is still to fuzzy since just looking
for equality symbols in a language is not sufficient.