Re: 'polymorphism restriction' anyone?

From: Wolfgang Lux <>
Date: Mon, 18 Dec 2006 10:17:09 +0100

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

> 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
refuses to infer this type when bot is defined in a local declaration
(and hence considered a variable). I admit that this is not the most
type that could be inferred for bot, but it is the most general type
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
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).


curry mailing list
Received on Mo Dez 18 2006 - 11:28:31 CET

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