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?
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
data Iterator i o m a
= NeedInput (i -> Iterator i o m a)
| HasOutput o (Iterator i o m a)
| NeedAction (m (Iterator i o m a))
| IsDone a
feedPure :: [i] -> Iterator i o (forall m . m) a -> Iterator i o (forall m . m) a
feedPure = loop
where
loop [] iter = iter
loop (i:is) (NeedInput k) = loop is (k i)
loop is (HasOutput o k0) = HasOutput o (loop is k0)
loop _ (NeedAction _) = undefined -- shouldn't happen, due to type
loop _ (IsDone a) = IsDone a
{-
impredicative.hs:10:34:
Kind mis-match
The third argument of `Iterator' should have 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) -}
feedPure' :: [i] -> Iterator i o (forall m . (m :: * -> *)) a -> Iterator i o (forall m . (m :: * -> *)) a
feedPure' = loop
where
loop [] iter = iter
loop (i:is) (NeedInput k) = loop is (k i)
loop is (HasOutput o k0) = HasOutput o (loop is k0)
loop _ (NeedAction _) = undefined
loop _ (IsDone a) = IsDone a
{-
impredicative.hs:28:46:
`(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
-}
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
