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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
