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 So Dez 17 2006 - 14:53:54 CET