Re: type-directed programming

From: Wolfgang Lux <wlux_at_uni-muenster.de>
Date: Fri, 15 Dec 2006 15:59:56 +0100

Sebastian Fischer wrote:

> I forgot to post my definition of prec:
>
> prec :: a -> (Nat -> a -> a) -> Nat -> a
> prec mz _ Zero = mz
> prec mz ms (Suc n) = ms n (prec mz ms n)
>
> Currently, I think the Curry type checker infers a type that is not
> general enough. So maybe you spotted a bug again ;) In any case, I
> don't think that a free variable and undefined should type-check
> differently. So, maybe "cursor :: a" should be the correct type, even
> if mz was a free variable (?)

The Curry type checker *is* correct (I'm sure, since I wrote it :-).
Variables must have monomorphic types in Curry. Without this restriction
you could define an unsafe cast function

   cast :: a -> b
   case x | x =:= y = y where y free; y :: a

The point is that y's type would be instantiated to two different
types aat both occurrences. This is inconsistent with the fact that
the underlying logical variable is shared between both occurrences. No
such sharing occurs between the results of different uses of the
undefined
function so it can safely be given a polymorphic type. Of course, this
argument is no longer valid when the result of undefined is bound to a
variable.

In principle, it would be possible to assign a polymorphic type to
a variable that is bound to undefined or to a constant like the empty
list. However, in order to get this right in general, you have to
perform a groundness analysis. I do not think that it is worth
complicating the type checker in that way for the few places where
polymorphic variable might be useful.

Regards
Wolfgang


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

This archive was generated by hypermail 2.3.0 : Wed Sep 18 2019 - 07:15:06 CEST