Re: type-directed programming

From: Claus Reinke <claus.reinke_at_talk21.com>
Date: Sat, 16 Dec 2006 18:25:48 +0000

Thank you for your explanations, Wolfgang. I guess the details of how Curry
differs from ML's value restriction are in the Curry report. but the following
made me wonder

> It is simply because in Curry functions can return unbound variables,
> unknown :: a
> unknown = x where x free

why would this be considered unbound? in the sense "not bound to a value"?

also, what are the implications of the polymorphic type here? intuitively, I'd
expect it to be impossible ever to unify unknown/x with anything, because of
x's very restricted scope, so unknown might be polymorphic, but in a similar
way as undefined is polymorphic, ie, polymorphically unusable (we can only
pass it around).

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.

I'd have expected either an error telling me that unknown cannot be unified
(no scope extension), or a type error (scope extension of shared unknown).
Would the latter be consistent with a monomorphic unknown?

Claus


_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Sun Dec 17 2006 - 14:54:02 CET

This archive was generated by hypermail 2.3.0 : Thu Sep 19 2019 - 07:15:06 CEST