[Haskell-cafe] Higher-kinded Quantification

[Dan Doel]

On Tuesday 12 April 2011 11:27:31 AM Leon Smith wrote:
> I think impredicative polymorphism is actually needed here;  if I write
> ...
> Then I get a type error
> ...

I'm not going to worry about the type error, because that wasn't what I had in 
mind for the types. The type for loop I had in mind was:

  [i] -> Iterator i o m a -> Iterator i o m a

Then, feedPure cracks open the first (forall m. ...), instantiates it to the m 
for the result, and runs loop on it. If we had explicit type application, it'd 
look like:

  feedPure l it = /\m -> loop l (it at m)

but as it is it's just:

  feedPure l it = loop l it

Which cannot be eta reduced.

> But what I find rather befuddling is the kind error:
> > feedPure' :: [i] -> Iterator i o (forall (m :: * -> *) . m) a -> Iterator
> > i o (forall (m :: * -> *) . m) a feedPure' = undefined
> 
> Iterator.hs:193:58:
>     `m' is not applied to enough type arguments
>     Expected kind `*', but `m' has kind `* -> *'
>     In the type signature for `feedPure'':
>       feedPure' :: [i]
>                    -> Iterator i o (forall m :: (* -> *). m) a
>                       -> Iterator i o (forall m :: (* -> *). m) a
> 
> Is impredicative polymorphism restricted to the kind *?

The problem is that (forall (m :: * -> *). m) is not a valid type, and forall 
is not a valid way to construct things with kind * -> *. You have:

  m :: * -> * |- T[m] :: * ==> |- (forall (m :: * -> *). T[m]) :: *

but that is the only way forall works.

-- Dan