Sebastian Hanowski wrote:
> _at_Wolfgang Lux
>> The Curry type checker *is* correct (I'm sure, since I wrote it :-).
>
> No, it's not.
The Curry type checker *is* correct in the sense that it faithfully
implements Curry's type system (see my answer to Claus Reinke from
today).
> Sebastian Fischer digged it out. Every call to the
> 'unknown' function will give you a fresh, free variable (I think
> it's
> like with IO References in Haskell). But since they can be
> bound -
> shared or not - to values, the context of their occurrence may fix
> their
> type.
>
> But
> bot :: a
> bot = bot
>
> will never compute to any value at all. And that's why /
> statically/ you
> can use it everywhere.
> Like I wrote earlier, it inhabits the /intersection of all types/.
> So it
> really has the type:
>
> bot :: forall a. a
>
> The Curry type-checker doesn't infer a most general type for it,
> when
> binding the type-variable due to context.
The Curry type-checker *does* infer the most general type for bot if you
define it at the top-level (i.e., as function with no arguments). It
simply
refuses to infer this type when bot is defined in a local declaration
group
(and hence considered a variable). I admit that this is not the most
general
type that could be inferred for bot, but it is the most general type
that
can safely be inferred for bot without using a groundness analysis (or
adding just a special case for local definitions of the form x = x).
> There's something like a 'polymorphism restriction' to it.
It is usually called a monomorphism restriction. You might also want to
google a bit for the dreaded monomorphism restriction for a related
issue
in Haskell, which regularly pops up on the Haskell related mailing lists
(or directly have a look at Sect. 4.5.5 of the Haskell report).
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