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

From: Wolfgang Lux <wlux_at_uni-muenster.de>

Date: Mon, 18 Dec 2006 09:47:39 +0100

Claus,

please keep in mind that Curry, though superficially similar to

Haskell, has a

different semantics. In particular, a Curry program is considered a

set of

(possibly) mutually recursive function equations. Therefore, a global

definition

like

unknown = x where x free

denotes a function with no arguments in Curry and not a global

variable (or

CAF) as in Haskell. All local definitions except declarations of free

variables

are lifted away (the details are explained in Appendix D.7 of the

Curry report).

Thus,

*> but when I play with PAKCS www interface, it seems that Curry does
*

*> some
*

*> form of scope extension? for instance, the following is accepted:
*

*>
*

*> f _ | (unknown =:= True) & (unknown =:= 0) = unknown
*

*>
*

*> Goal: f False :: a
*

*> Result: _1154 ?
*

*>
*

*> now this is curious, because it suggests that (a) the scope of x is
*

*> extended
*

*> to cover the (=:=) constraints, and that (b) unknown is expanded by
*

*> name,
*

*> rather than by need, so that instead of one shared free x, we get
*

*> three
*

*> independent free x.
*

unknown is expanded three times and you get three different logical

variables

(whose scope is extended into the enclosing expression) as you observed.

Also note that Curry's type system (cf. Sect. 4.2 of the Curry

report) is

defined on the lifted representation of the program. Thus, there are no

let-bound variables in Curry except for free variables, whose type

(necessarily) is monomorphic. Since there are no let-bound variables,

no generalization takes place for variables and hence Curry's typing

discipline is more restrictive than ML's value restriction.

Incidentally, I have been looking at extending Curry's type system

towards

adopting ML's value restriction. However, there are some technical

issues to

be solved. The most annoying of these is that ML's notion of a non-

expansive

expression (whose type can be generalized) is purely syntactic in ML,

but

not so in Curry because of the existence of functions with no

arguments. In

addition, I still have to prove that the extended type system is really

sound.

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Mo Dez 18 2006 - 11:28:31 CET

Date: Mon, 18 Dec 2006 09:47:39 +0100

Claus,

please keep in mind that Curry, though superficially similar to

Haskell, has a

different semantics. In particular, a Curry program is considered a

set of

(possibly) mutually recursive function equations. Therefore, a global

definition

like

unknown = x where x free

denotes a function with no arguments in Curry and not a global

variable (or

CAF) as in Haskell. All local definitions except declarations of free

variables

are lifted away (the details are explained in Appendix D.7 of the

Curry report).

Thus,

unknown is expanded three times and you get three different logical

variables

(whose scope is extended into the enclosing expression) as you observed.

Also note that Curry's type system (cf. Sect. 4.2 of the Curry

report) is

defined on the lifted representation of the program. Thus, there are no

let-bound variables in Curry except for free variables, whose type

(necessarily) is monomorphic. Since there are no let-bound variables,

no generalization takes place for variables and hence Curry's typing

discipline is more restrictive than ML's value restriction.

Incidentally, I have been looking at extending Curry's type system

towards

adopting ML's value restriction. However, there are some technical

issues to

be solved. The most annoying of these is that ML's notion of a non-

expansive

expression (whose type can be generalized) is purely syntactic in ML,

but

not so in Curry because of the existence of functions with no

arguments. In

addition, I still have to prove that the extended type system is really

sound.

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Mo Dez 18 2006 - 11:28:31 CET

*
This archive was generated by hypermail 2.3.0
: So Okt 24 2021 - 07:15:03 CEST
*