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 <dan.d...@gmail.com> wrote: > 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 > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe