I think impredicative polymorphism is actually needed here; if I write
{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-}
feedPure :: forall i o a. [i] -> (forall m. Iterator i o m a) -> (forall m. Iterator i o m a) feedPure = loop where loop :: [i] -> (forall m. Iterator i o m a) -> (forall m. Iterator i o m a) loop [] iter = iter loop (i:is) (NeedInput k) = loop is (k i)
Then I get a type error: Iterator.hs:185:36: Couldn't match type `m0' with `m1' because type variable `m1' would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: Iterator i o m1 a The following variables have types that mention m0 k :: i -> Iterator i o m0 a (bound at Iterator.hs:185:28) Which I think I vaguely understand, as the type of NeedInput is (i -> Iterator i o m a) -> Iterator i o m a, meaning the type of m is equal. So it seems the polymorphism must be carried on m. 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 *?
Best,
Leon
Then I get a tp
On Tue, Apr 12, 2011 at 5:37 AM, 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe