Thanks! The issue with eta-reduction had been confusing me...
Best,
Leon
On Tue, Apr 12, 2011 at 3:35 PM, Dan Doel
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