- Haskell-Cafe - Haskell.org

Re: Linearity Requirement for Patterns
by Michael Hanus 22 Mar '01

22 Mar '01

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

4 3

Re: Linearity Requirement for Patterns
by Michael Hanus 22 Mar '01

22 Mar '01

Bjorn Lisper wrote: > >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 Yes. Since Curry is based on a lazy and (for a particular subclass, namely inductively sequential rules) also optimal evaluation strategy, sharing of function arguments is required and essential. > 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. In the presence of nondeterministic functions (i.e., nonconfluent rules), one has several options for the semantics. For parameter passing, one can use either the call-time choice or run-time choice semantics. Curry is based on the former since there is a well-defined semantical framework for this in the presence of non-strict functions (Gonzalez-Moreno et al., Journal of Logic Programming, Vol. 40, 1999). Semantically, the call-time choice means that rewrite rules can only be applied if the arguments are constructor terms, i.e., totally evaluated. This does not necessarily imply a strict semantics since it can be implemented by lazy reduction provided that function arguments are shared. Thus, this sharing must be somehow represented in an intermediate language for executing the programs and on this level inlining is preserved, as you have remarked. Naive inlining (i.e., without lets but possibly duplicating function calls) does only work for deterministic functions (which is no restriction from a Haskell point of view since Haskell allows only deterministic functions). > 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? The paper mentioned above defines a proof calculus, model theory and operational semantics for this language where the denotation of functions distinguish between deterministic and non-deterministic functions which seems to be conform to your remarks. Although it does not explicitly define referential transparancy, it shows the equivalence of all three notions which I think is enough for reasoning about Curry programs. Nevertheless, many thanks for your hints. Michael

1 0

Re: Linearity Requirement for Patterns
by Michael Hanus 22 Mar '01

22 Mar '01

Lennart Augustsson wrote: > Yes, your definition of non-linear patterns would give you extra > power. It would also destroy the nice semantics of Haskell! > By using this facility you can now observe intensional properties > of the term, and the clean denotational semantics crumbles. > > E.g., in Haskell you can always replace equals by equals without > changing the meaning of a program. In your example `g 0' is equal > to bottom so it should be possible to replace it by any other bottom > without any change in meaning. But if I define > h x = h x > and evaluate `f (g 0) (h 0)' I will no longer get 0. > > So this definitions of non-linear patterns is not an option for a > language that claims to be "referentially transparent" (whatever that means :). I agree and the question is about "whatever that means"... Term rewriting systems (TRS) are based on replacing equals by equals and that could be also considered as "referentially transparent". Nevertheless, TRSs usually allow non-linear left-hand sides (but often come with other restrictions like termination). BTW, (g 0) and (h 0) are not considered as equal since there are no rules/equations to transform one into the other. However, I agree that there are good reasons (mainly, operational simplicity) to allow only linear patterns and constructor-based rules in a real programming language, since non-linear patterns or non-constructor-based rules require other and more advanced operational principles. I only wanted to remark that there is no simple way to translate non-linear pattterns into linear patterns in the general case. Michael

4 3

Re: Linearity Requirement for Patterns
by Michael Hanus 22 Mar '01

22 Mar '01

Jerzy Karczmarczuk wrote: > Logic languages which allow for nonlinear patterns use unification, > which is usually much more costly than simple pattern compiling. > Now, I wonder whether in FP where there is no place for "logical > variable" concept one needs or doesn't need the classical unification, > with all the substitutions of variables. > "Read-only" patterns are manipulated more efficiently, but in presence > of laziness, of ~patterns etc., I feel - for the moment - rather > lost. > > What is the status of the referential transparency of Prolog or > Mercury? Prolog isn't referential transparent due to predefined predicates with side effects. However, logic programming ("pure Prolog") is referentially transparent if one considers a "non-deterministic" semantics where an expression is reduced to a disjunction of expressions (Prolog systems explore this disjunction in a left-to-right manner by backtracking). Actually, one can extend Haskell by "logical variables" in a conservative manner. This is the idea of the functional logic language Curry (http://www.informatik.uni-kiel.de/~curry/) where the pattern matching process is slightly extended so that the operational behavior is identical to Haskell (i.e., not more costly) for programs without occurrences of logical variables and, if a logical variable occurs during pattern matching, it is (non-deterministically) bound to some pattern. However, in order to support infinite data structures and laziness, linear patterns are also required. Non-linear patterns must be transformed into linear patterns by introducing a unification constraint in the condition part, i.e., all non-linearities must be made explicit in the program (so that pattern matching can be efficiently performed). Thus, I think that linearity is a natural requirement even for logic languages that support laziness. Michael

3 2

Re: ANNOUNCE: HasChorus - some modules for Haskore
by Robert Jeschofnik 20 Mar '01

20 Mar '01

On 20-Mar-2001, Martin Schwenke <martin(a)meltin.net> wrote: > HasChorus: > > A set of Haskell (http://haskell.org/) modules written on top of > Haskore (http://haskell.org/haskore/) to make it easier to sequence > simple, repetitive music. Even without having had a look at the code yet, I am led to wonder... > BubbleSort.lhs: An implementation of bubble sort. > Used by HasGroove.lhs. (I reformatted the quote so it wouldn't wrap over 80 chars) -Why- bubblesort? Rob

2 1

RE: Coroutines
by Simon Peyton-Jones 20 Mar '01

20 Mar '01

Lazy evaluation *is* coroutines, in a way. Or you may be interested in Concurrent Haskell See section 4 of "Tackling the awkward squad" http://research.microsoft.com/~simonpj/papers/marktoberdorf.htm Simon | -----Original Message----- | From: Andreas Gruenbacher [mailto:gruenbacher@geoinfo.tuwien.ac.at] | Sent: 19 March 2001 17:00 | To: haskell-cafe(a)haskell.org | Subject: Coroutines | | | Hello, | | has anybody thought about how to implement Simula style coroutines in | Haskell? What I have in mind is several "procedures" that | communicate via | message passing in a co-operative way. That would give clear | and intuitive | code for things like simulations... | | Thanks, | Andreas. | | -------------------------------------------------------------- | ---------- | Andreas Gruenbacher gruenbacher(a)geoinfo.tuwien.ac.at | Research Assistant Phone +43(1)58801-12723 | Institute for Geoinformation Fax +43(1)58801-12799 | Technical University of Vienna Cell phone +43(664)4064789 | | | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe(a)haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe |

6 6

RE: Coroutines
by Simon Peyton-Jones 20 Mar '01

20 Mar '01

| I see your point, and I must admit that this approach has its | charm. It's | not what I had in mind, though. Simon's MVars (in the Awkward Squad) | come pretty close, but they're still not the sort of (cooperative) | multitasking that I'm thinking of. I'm not looking for a | process or thread | model of concurrency. That's too expensive for simulations due to the | frequency of task switches. Could you try it and see? GHC's threads are implemented in GHC's runtime system; thread switching is much much much cheaper than switching between OS threads. It's designed to support thousands or hundreds of thousands of threads. Give it a whirl! Simon

1 0

RE: Coroutines
by Simon Peyton-Jones 19 Mar '01

19 Mar '01

1 0

Coroutines
by Andreas Gruenbacher 19 Mar '01

19 Mar '01

Hello, has anybody thought about how to implement Simula style coroutines in Haskell? What I have in mind is several "procedures" that communicate via message passing in a co-operative way. That would give clear and intuitive code for things like simulations... Thanks, Andreas. ------------------------------------------------------------------------ Andreas Gruenbacher gruenbacher(a)geoinfo.tuwien.ac.at Research Assistant Phone +43(1)58801-12723 Institute for Geoinformation Fax +43(1)58801-12799 Technical University of Vienna Cell phone +43(664)4064789

1 0

Re: Linearity Requirement for Patterns
by Michael Hanus 19 Mar '01

19 Mar '01

Brian Boutel wrote: > In any case, the same effect can be obtained using guards, where the > extra power of expression syntax solves the problem. Instead of > f x x = e1 > f (illegal pattern) = e2 > ... > > you can write the single equation > > f x y | x == y = e1 > | x /= y = e2 It depends on the meaning of pattern matching wrt. non-linear patterns. The standard notion (e.g., term rewriting) matches a pattern by finding a substitution for the pattern variables so that the instantiated pattern is identical to the function call. In this case, it can also match partially defined functions in contrast to your transformation. For instance, consider the definitions g z = 1 + g z f x x = 0 Then a call like (f (g 0) (g 0)) is reducible to 0 (wrt. standard notion of pattern matching using the instantiation {x |-> (g 0)}) whereas it is undefined if we transform this definition to f x y | x==y = 0 (which requires the evaluation of both arguments). Thus, I would say that non-linear patterns gives you extra power. Michael

3 2