Re: Linearity Requirement for Patterns
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" before). 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 functions. 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. Michael
Michael Hanus:
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 functions.
How does sharing work here? I assume the "let x = ..." is intended to mean sharing of "...". Does the same hold for function calls in Curry, so "aux x = g x x" implies sharing of x when evaluating g? In that case I suspect you might have problems if, for instance, you inline aux naively into g (f y) (f y) and f is nondeterministic. (Inlining should typically work for a referentially transparent language.) The problem can be fixed though: if you have this sharing, then "aux x = g x x" is really shorthand for "aux x = let y = x in g y y". If this definition is inlined and the let is kept (to preserve the sharing), then the transformation should work even if f is nondeterministic. If, on the other hand, Curry has a call-by-name semantics, then the direct inlining should work.
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.
Referential transparency is defined w.r.t. some notion of equality on terms, and cannot be precise unless this notion is made precise. If the language at hand has a denotational semantics, then equality on terms can be derived from their denotations. But referential transparency can also be defined w.r.t. other semantics. An interesting case is term rewrite semantics: a confluent term rewrite system defines a notion of equality through its convertibility relation (the transitive-reflexive-symmetric closure of the reduction relation). A notion of referential transparency can be based on this equivalence relation (which is an equality relation, due to closedness of the reduction relation under substitutions and taking of contexts). A restricted notion of referential transparency carries over to nonconfluent (and thus nondeterministic) rewrite systems. If the rewrite system can be partitioned into a confluent and a nonconfluent part, then the convertibility relation for the confluent part can be taken as an equality relation upon which the referential transparency can be defined. Under certain (not so strong) technical conditions, the set of possible normal forms will be the same for terms that are equal w.r.t. this convertibility relation. This holds also if the concept of normal form is extended to cover infinite and possibly diverging computations. I don't know how much of this applies directly to Curry, since the above is for pure term rewriting and I suspect Curry has unification in its evaluation mechanism (right?) which then makes the evaluation more complex. But maybe the above can provide some ideas how to formally define referential transparency for Curry? Björn Lisper PS. I have a paper on this. There is also a paper by Søndergaard and Sestoft that has an interesting discussion about referential transparency and nondeterminism. Bibtex entries are given below. @STRING{tcs = "Theoret.\ Comput.\ Sci."} @ARTICLE{Lisper-TCS, AUTHOR = {Bj{\"o}rn Lisper}, TITLE = {Computing in Unpredictable Environments: Semantics, Reduction Strategies, and Program Transformations}, JOURNAL = tcs, YEAR = {1998}, VOLUME = {190}, NUMBER = {1}, PAGES = {61--85}, MONTH = jan } @ARTICLE{SonSes-reftrans-unfold, AUTHOR = {Harald S{\o}ndergaard and Peter Sestoft}, TITLE = {Referential Transparency, Definiteness and Unfoldability}, JOURNAL = {Acta Informatica}, YEAR = {1990}, VOLUME = {27}, PAGES = {505--517} }
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. /Koen. -- Koen Claessen http://www.cs.chalmers.se/~koen phone:+46-31-772 5424 mailto:koen@cs.chalmers.se ----------------------------------------------------- Chalmers University of Technology, Gothenburg, Sweden
On 22-Mar-2001, Koen Claessen
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
participants (4)
-
Bjorn Lisper -
Fergus Henderson -
Koen Claessen -
Michael Hanus