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.

On Tue, 2008-06-10 at 11:28 -0700, Ryan Ingram wrote:

On 6/10/08, Derek Elkins wrote:

...

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.

Although if I am reading the literature correctly, that definition will likely typecheck in the next GHC...

http://research.microsoft.com/~simonpj/papers/boxy/

Actually some support was hacked into the current version of GHC. http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extension...