[Haskell-cafe] handling rank 2 types
Andrew Pimlott
andrew at pimlott.net
Thu Nov 3 23:35:26 EST 2005
I am trying to use a rank 2 type to enforce a condition on a data
structure. For the purpose of this message, I am trying to ensure that
a list is empty (ignoring the possibility of bottom elements):
> {-# OPTIONS -fglasgow-exts #-}
> import Control.Monad
> newtype Empty = Empty (forall a. [a])
I want a function
> listToEmpty :: [v] -> IO Empty
> listToEmpty l = liftM Empty (mapM no l) where
> no :: a -> IO a'
> no x = fail "element found"
But this gives a "less polymorphic" error. I think the problem is that
ghc will not instantiate the "a'" in "IO a'" as a higher-rank type
because it occurs within a type contructor. I believe this is the
restriction referred to at the end of 7.4.9[1]. If I instead write
> uncheckedListToEmpty :: [v] -> Empty
> uncheckedListToEmpty l = Empty (map no l) where
> no :: a -> a'
> no x = error "element found"
it compiles, because "v'" can be instantiated as "forall v. Rule v", and
even pass through map with the higher-rank type.
Is there any way to make ghc accept the first definition? I found this
workaround:
> newtype Any = Any { unAny :: forall a. a }
> listToEmptyAny :: [v] -> IO Empty
> listToEmptyAny l = liftM (\l -> Empty (map unAny l)) (mapM no l) where
> no :: a -> IO Any
> no x = fail "element found"
But needing a newtype wrapper Empty was bad enough; do I really need one
for every intermediate result (that is inside another type constructor)
as well? I could probably define a generic family of wrappers
> newtype Forall = Forall (forall a. a)
> newtype Forall1 c1 = Forall1 (forall a. c1 a)
> newtype Forall2 c1 c2 = Forall2 (forall a. c1 c2 a)
...
But I would still have to use them everywhere. Any other tricks?
Andrew
[1] http://haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#universal-quantification
More information about the Haskell-Cafe
mailing list