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

From: Michael Hanus <mh_at_informatik.uni-kiel.de>

Date: Tue, 02 Nov 2004 12:11:57 +0100

Dear Colleagues,

I'd like to propose to relax two restrictions in the definition

of Curry which seem to me unnecessarily strong.

The first one is related to the introduction of free variables.

The current language definition (Curry Report, C.3) requires

that in an expression of the form

let x free in e

e must be of type "Success" (1).

On the one hand, this seems justified by the fact that existential

quantification is reasonable for constraints only. On the other hand,

this demands for some nasty transformations if one needs local

variables in a non-constraint scope. For instance, the (currently

illegal) definition

f x = \y -> let z free in g x y z -- (2)

(where (g x y z) is not of type Success) can be transformed

in the valid Curry program

f x = g' x

g' x y = g x y z where z free

The transformation can be avoided by introducing a

"generate-free-variable" function (actually, this is the

solution which I often use):

f x = \y -> g x y any

any = z where z free

Both solutions are less readable than (2). Furthermore,

the alternatives demonstrate that restriction (1) is not

really necessary. In particular, if one defines a type

isomorphic to Success, the restriction becomes questionable.

Thus, I propose to drop the restriction (2).

This would also make the application of let and where

"more equivalent".

The second restriction concerns the sequential conjunction

of constraints, which is currently defined as

(&>) :: Success -> Success -> Success

c &> x | c = x

in the prelude.

We have a number of applications where we want to put constraints

during a functional evaluation. Until now, we have defined for this

purpose a "guard" function that takes a constraint and an expression as

input and is the identity on the second argument provided that the

constraint is satisfied. Thus, it is defined as

guard :: Success -> a -> a

guard c x | c = x

so that you can use it as in (guard (x=:=1) (2+x)).

Now, you see that the definition of the guard function is

identical to (&>) apart from the different types.

Since such a guard function is quite useful, I propose

to generalize the type of (&>) to

(&>) :: Success -> a -> a

so that it is a general function to establish new constraints

during arbitrary computations.

Since both proposals have no influence on existing programs but

allow more valid Curry programs, I see no problem in them.

However, maybe somebody sees some problem?

Best regards,

Michael

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Di Nov 02 2004 - 14:14:47 CET

Date: Tue, 02 Nov 2004 12:11:57 +0100

Dear Colleagues,

I'd like to propose to relax two restrictions in the definition

of Curry which seem to me unnecessarily strong.

The first one is related to the introduction of free variables.

The current language definition (Curry Report, C.3) requires

that in an expression of the form

let x free in e

e must be of type "Success" (1).

On the one hand, this seems justified by the fact that existential

quantification is reasonable for constraints only. On the other hand,

this demands for some nasty transformations if one needs local

variables in a non-constraint scope. For instance, the (currently

illegal) definition

f x = \y -> let z free in g x y z -- (2)

(where (g x y z) is not of type Success) can be transformed

in the valid Curry program

f x = g' x

g' x y = g x y z where z free

The transformation can be avoided by introducing a

"generate-free-variable" function (actually, this is the

solution which I often use):

f x = \y -> g x y any

any = z where z free

Both solutions are less readable than (2). Furthermore,

the alternatives demonstrate that restriction (1) is not

really necessary. In particular, if one defines a type

isomorphic to Success, the restriction becomes questionable.

Thus, I propose to drop the restriction (2).

This would also make the application of let and where

"more equivalent".

The second restriction concerns the sequential conjunction

of constraints, which is currently defined as

(&>) :: Success -> Success -> Success

c &> x | c = x

in the prelude.

We have a number of applications where we want to put constraints

during a functional evaluation. Until now, we have defined for this

purpose a "guard" function that takes a constraint and an expression as

input and is the identity on the second argument provided that the

constraint is satisfied. Thus, it is defined as

guard :: Success -> a -> a

guard c x | c = x

so that you can use it as in (guard (x=:=1) (2+x)).

Now, you see that the definition of the guard function is

identical to (&>) apart from the different types.

Since such a guard function is quite useful, I propose

to generalize the type of (&>) to

(&>) :: Success -> a -> a

so that it is a general function to establish new constraints

during arbitrary computations.

Since both proposals have no influence on existing programs but

allow more valid Curry programs, I see no problem in them.

However, maybe somebody sees some problem?

Best regards,

Michael

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Di Nov 02 2004 - 14:14:47 CET

*
This archive was generated by hypermail 2.3.0
: Fr Jan 24 2020 - 07:15:05 CET
*