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