[Haskell] Re: Impredicative Types?

[Ben Rudiak-Gould]

On Wed, 18 Feb 2004, Daan Leijen wrote:

> 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 bad, but it doesn't seem any worse than what we've got already in
GHC and Hugs. In fact, what we've got is much worse: not only can't we
infer most general types, we can't even determine the meaning of a correct
program without looking at explicit type signatures.

> 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).

I noticed that problem but didn't think about the difficulties of type
constructor parameters. It seems like you could make this work by
extending the kind system, but maybe it's not worth it.

-- Ben