Re: type-directed programming

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

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:08 CEST