- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: German Vidal <gvidal_at_dsic.upv.es>

Date: Fri, 07 Jan 2011 01:53:27 +0100

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

Date: Fri, 07 Jan 2011 01:53:27 +0100

On 06/01/2011, at 21:41, Sergio Antoy wrote:

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.

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

*
This archive was generated by hypermail 2.3.0
: So Jan 26 2020 - 07:15:11 CET
*