[Haskell] Impredicative Types?

[Daan Leijen]

On Tue, 17 Feb 2004 14:40:18 -0800, Ashley Yakeley <ashley at semantic.org> wrote:
>  Ben Rudiak-Gould <benrg at dark.darkweb.com> wrote:
>
>> > Bear in mind you can't even write IO (forall t. whatever) in Haskell.
>>
>> True, but why is this? Is there a deep reason why we can use nested
>> foralls as the arguments to (->), but not as the arguments to any other
>> type constructor?
>
> Apparently it makes type-checking Very Very Hard. Simon PJ may have
> explained it to me ("impredicative", he called it), but I don't remember
> offhand.

Whenever you instantiate type variables with type schemes, you are impredicative.
Impredicative instantiation makes type checking (much) harder -- without extra
constraints, you don't even have principal types. i.e.

choose :: a -> a -> a
choose x y = x

What is the type of "choose id" if your system is impredicative?
Either "forall a. (a -> a) -> (a -> a)"  or "(forall a. a->a) -> (forall a. a->a)"
Note that neither of these types subsumes the other.
This is why MLF adds extra constraints which enables them to give a principle
type to this expression. (namely: forall a. (a >= forall a. a -> a) => a -> a)

Anyway, Ben Rudiak's particular case, namely instantiating arguments of a
type with type schemes, is difficult due to another problem. It is very
hard to know whether an argument to a type is used contra-variantly or co-variantly
(or both, or not at all). This means that we can't do a proper subsumption
check on type schemes. i.e.

data Contra a  = Contra (a -> Int)
data Co a      = Co (Int -> a)
data None a    = None
data Both a    = Contra (a -> Int) | Co a

In this case it may seem trivial to infer the contra/co variance of the argument
but try this with some type constructors as arguments :-) In a particular case
one can give type rules of course, for example for tuples or the IO monad.

All the best,
  Daan.