[Haskell-cafe] Writing functions over GADTs

[Benedikt Huber]

On 16.03.11 10:26, Dominic Mulligan wrote:
> Dear all,
>
> 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
 >    [...]
 >
 > 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]
 > [...]
Hi Dominic,
As you noticed, this type signature is not correct.
Consider for example

toList (SmallCons t Empty :: ArgList Large)

t is of type 'Type Small', but the result needs to be a list with 
elements of type 'Type Large', i.e., of type [Type Large].

Also note that this instance would also need to typecheck:

toList (Empty :: ArgList Cookie) :: [Type Cookie]

> 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?

There are many solutions to this problem in Haskell as well, but HList 
is probably not what you want.

Here is one variant, which is polymorphic in the type constructor 
parametrized over Small or Large:

-- For each t, Ex t is either (t Small) or (t Large)
data Ex :: (* -> *) -> * where
   ExS :: t Small -> Ex t
   ExL :: t Large -> Ex t
toList :: ArgList a -> [Ex Type]
toList Empty           = []
toList (SmallCons h t) = ExS h : toList t
toList (LargeCons h t) = ExL h : toList t

As in your case, the datatype constructor tells you whether you are 
dealing with a small or large type, a more generic encoding of 
existentials would be fine too I guess:

data Ex :: (* -> *) -> * where
   Ex :: t a -> Ex t

Kind Regards,
Benedikt