[Haskell-cafe] Predicativity?

[Thomas Davie]

On 17 Sep 2008, at 07:05, Wei Hu wrote:

> Hello,
>
> I only have a vague understanding of predicativity/impredicativity,  
> but cannot
> map this concept to practice.
>
> We know the type of id is forall a. a -> a. I thought id could not  
> be applied
> to itself under predicative polymorphism. But Haksell and OCaml both  
> type check
> (id id) with no problem. Is my understanding wrong? Can you show an  
> example
> that doesn't type check under predicative polymorphism, but would  
> type check
> under impredicative polymorphism?

In your application (id id) you create two instances of id, each of  
which has type forall a. a -> a, and each of which can be applied to a  
different type.  In this case, the left one gets applied to the type  
(a -> a) and the right one a, giving them types (a -> a) -> (a -> a)  
and (a -> a) respectively.

What will not type check on the other hand is:

main = g id

g h = h h 4

which needs something along the lines of rank-2 polymorphism.

Bob