Thanks! The issue with eta-reduction had been confusing me... Best, Leon
On Tue, Apr 12, 2011 at 3:35 PM, Dan Doel <dan.d...@gmail.com> wrote: > 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 > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
