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.
> 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.
Best regards,
Michael
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Jan 06 2011 - 18:10:54 CET