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

[Roberto Zunino]

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 .

For more tricks with type-lambdas, look up "System F".

Hope this helps,
Zun.