[Haskell-cafe] Moving "forall" over type constructors

[Derek Elkins]

On Tue, 2008-06-10 at 18:12 +0200, Roberto Zunino wrote:
> Sean Leather wrote:
> > inside :: ((forall a. W (t a))-> W (forall a. (t a)))
> > --inside (W x) = W x -- (a) FAILS
> > --inside = W . unW -- (b) FAILS
> > inside x = W (unW x) -- (c) WORKS
> >
> > Are there any pointers for developing a better understanding or
> > intuition of this?
> 
> Usually, making type arguments explicit helps: that is, assume that each
> polymorphic value is actually a function expecting a type (the a in
> forall a. ...) and returning the value related to that type. The last
> 'inside' definition becomes:
> 
>   inside x = W (\type -> unW (x type))
> 
> Note that we do not know at this time what will be the actual "type"
> above. But that's OK, since we can return a type-lambda.
> 
> Instead, pattern matching desugars to:
> 
>   inside x = case x of ...
> 
> But wait! x is a function (because it's polymorphic) and we can not
> pattern match on that! And, at this time, we do not know the
> type-argument for x. So we are stuck.
> 
> Also, type-lambdas and type-arguments are hard to insert in W . unW .

This is the lack of impredicativity.

W :: a -> W a
To get the result type W (forall a. t a), W must instantiate the a in
W's type to (forall a. t a).  Further we then pass it to (.) which has
type (b -> c) -> (a -> b) -> a -> c and thus require instantiating both
a and b to higher-rank types.  A predicative type system does not allow
instantiating type variables to quantified types.