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