On 06/01/2011, at 21:41, Sergio Antoy wrote:
> On Thu, 06 Jan 2011, Michael Hanus wrote:
>
>> Wolfgang Lux wrote:
>>> Thinking a bit more about it, I finally see a reason for keeping the
>>> linearity restriction: Pattern matching in Curry (as in any other lazy
>>> language) causes evaluation to head normal form, i.e., arguments are
>>> evaluated just as far as necessary to make their shape equivalent to
>>> the pattern. This is no longer the case with non-linear patterns. Each
>>
>> This is true but it is questionable whether one really
>> reasons about a program in such individual steps
>> like hnf computations. For instance, the work on the
>> rewriting logic CRWL shows that a programmer might better
>> reason in terms of call-by-value evaluations
>> to understand the effect of nondeterministic computations.
>> Laziness is a good vehicle to ensure completeness of computations,
>> but it is not easy to think in this evaluation order.
>>
>> As a solution to this difficulty, I can imagine that
>> a compiler issues warnings on demand for non-linear patterns,
>> like it issue warnings for variables with a single occurrence.
>
> I like the idea of a warning.
Yes, warnings might be useful. Nevertheless, I don't really see a
problem with laziness here. If one clarifies that non-linear patterns
are just syntactic sugar for an equality constraint between arguments,
it should be clear that evaluation to normal form is required; actually,
I think that no confusion can arise since non-linear patterns are not
allowed in lazy functional languages like Haskell.
>>> There is also one point in your proposal that needs further
>>> clarification: What about function rules with (constraint) guards? f x
>>> x | g = e seems to have at least two possible translations: Either
>>> sequential
>>> f x y | x=:=y &> g = e
>>> or concurrent
>>> f x y | x=:=y & g = e
>>
>> Good point, but I have no preference or good arguments for
>> one of them. Intuitively, I'd prefer the sequential interpretation
>> since the non-linearity condition belongs to the matching,
>> i.e., it should be checked before any other guard or right-hand
>> side computations takes place.
>
> Are there some plausible examples where there is a difference
> which might help choosing either one of the options?
I also prefer the sequential one. E.g., given a function like
f x x | g Zero = Foo
g Zero = g Zero
g One = success
and the first translation
f x y | x =:= y & g Zero = Foo
a call like (f Zero One) might enter an infinite loop if the considered
selection strategy is not fair and always selects the second constraint
in (Zero =:= One & g Zero). This is not what one would expect here but
an immediate failure of unification between Zero and One.
Similarly, given a call like (f (g Zero) (g Zero)), one would expect an
infinite failure but a fair selection strategy will give rise to a
finite failure.
So I think that &> is more reasonable.
Best wishes,
German
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Jan 07 2011 - 10:34:30 CET