[Haskell-cafe] Higher-kinded Quantification

[Dan Doel]

On Monday 11 April 2011 8:31:54 PM Leon Smith wrote:
> I have a type constructor (Iterator i o m a) of kind (* -> * -> (* ->
> *) -> *),  which is a monad transformer,  and I'd like to use the type
> system to express the fact that some computations must be "pure",  by
> writing the impredicative type (Iterator i o (forall m. m) a).
> However I've run into a bit of difficulty expressing this,  due to the
> kind of m.   I've attached a minimal-ish example.   Is there a way to
> express this in GHC?

I think the simplest way is 'Iterator i o Id a'. Then there's a function:

  embed :: Iterator i o Id a -> Iterator i o m a

with the obvious implementation. This means your NeedAction case is no longer 
undefined, too. You can either peel off NeedActions (since they're just 
delays) or leave them in place.

However, another option is probably:

    [i] -> (forall m. Iterator i o m a) -> (forall m. Iterator i o m a)

which will still have the 'this is impossible' case. You know that the 
incoming iterator can't take advantage of what m is, though, so it will be 
impossible.

-- Dan