Higher-kinded Quantification
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?
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
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
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
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
participants (2)
-
Dan Doel -
Leon Smith