[Haskell-cafe] Writing functions over GADTs
dominic.p.mulligan at googlemail.com
Wed Mar 16 10:26:52 CET 2011
I'm working on a small proof assistant in Haskell. In the logic that
I'm implementing it's very important that I distinguish between `large'
and `small' types for consistency reasons. I have worked to get this
distinction reflected in my types with the use of GADTs, like so:
data Type :: * -> * where
SVariable :: Decoration -> Type Small
LVariable :: Decoration -> Type Large
Bound :: Index -> Type Small
Universal :: Decoration -> Type a -> Type Large
LFormer :: Decoration -> ArgList Large -> Variety -> Type Large
SFormer :: Decoration -> ArgList Small -> Variety -> Type Small
data ArgList :: * -> * where
Empty :: ArgList a
SmallCons :: Type Small -> ArgList a -> ArgList a
LargeCons :: Type Large -> ArgList a -> ArgList Large
Great, but one problem. How do you write functions over these data
types? Consider as an example the function `toList', which drops an
`ArgList a' down into a vanilla Haskell list `[a]'. Attempting a
straightforward implementation like so:
toList :: ArgList a -> [Type a]
toList Empty = 
toList (SmallCons h t) = h : toList t
toList (LargeCons h t) = h : toList t
Gives a type error, as the type variable `a' gets instantiated to Small
when typechecking the second clause of the function definition, and
Large when type checking the third clause. Perversely, it's much easier
to write a more complex function:
forget :: (forall a. Type a -> b) -> ArgList a -> [b]
forget f Empty = 
forget f (SmallCons h t) = f h : forget f t
forget f (LargeCons h t) = f h : forget f t
As we can use RankNTypes to make things `more polymorphic', and prevent
type variables being instantiated too soon. It seems plausible that
`toList' could be defined in terms of `forget', taking `f' to be the
identity function, but this does not work either as we then get type
errors about inferred types being less polymorphic than expected.
So, is there a standard way writing function like `toList' in Haskell?
Am I going about thinking of using GADTs in the wrong way? I've
searched everywhere and cannot seem to find the correct solution (and
I'm now at the very border of my Haskell knowledge).
My coworker showed me a way of doing this in O'Caml using polymorphic
variants. This allows us to form a subtype of both `Small' and `Large'.
I'm taken to believe that HList can simulate many of the properties that
polymorphic variants enjoy, so perhaps the answer lies there?
Any help gratefully received.
More information about the Haskell-Cafe