How to specify the type of heterogeneous collection in AST GADT recipe?

Question

I would like to print AST for a dynamic language. I am currently collecting collections. Here is a sample code example:

{-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ExistentialQuantification #-} data Box = forall s. B s data BinOp = Add | Sub | Mul | Div deriving (Eq, Show) data Flag = Empty | NonEmpty data List :: Flag -> * -> * where Nil :: List Empty a Cons :: a -> List fa -> List NonEmpty a data Expr ty where EInt :: Integer -> Expr Integer EDouble :: Double -> Expr Double -- EList :: List -> Expr List 

So far, I can build List instances quite well:

 *Main> :t (Cons (B (EInt 1)) (Cons (B (EDouble 2.0)) Nil)) (Cons (B (EInt 1)) (Cons (B (EDouble 2.0)) Nil)) :: List Box 'NonEmpty 

I am not sure how to encode this type in Expr for EList . Am I even on the right track here?

Answer 1

One way to solve this problem is to mark the values ​​using runtime type representatives. Here I am directing Stephanie Weirich. Let there be a small example. First introduce some types. This is usually done using a singleton design.

 data Type :: * -> * where Int :: Type Int Char :: Type Char List :: Type x -> Type [x] 

So Type Int contains a single value, which I also called Int , because it acts as a representative of the runtime of type Int . If you see color even in monochrome things, Int left of :: red, and Int after Type is blue.

Now we can make existential packaging while maintaining utility.

 data Cell :: * where (:::) :: x -> Type x -> Cell 

A Cell is a value labeled by the current representative of its type. You can restore the usefulness of a value by reading its type tag. Indeed, since types are first-order structures, we can test them for equality in a useful way.

 data EQ :: k -> k -> * where Refl :: EQ xx typeEQ :: Type x -> Type y -> Maybe (EQ xy) typeEQ Int Int = Just Refl typeEQ Char Char = Just Refl typeEQ (List s) (List t) = case typeEQ st of Just Refl -> Just Refl Nothing -> Nothing typeEQ _ _ = Nothing 

Boolean equality on type representatives is useless: we need an equality test to build evidence that the types presented can be unified. In evidence-based production, we can write

 gimme :: Type x -> Cell -> Maybe x gimme t (x ::: s) = case typeEQ st of Just Refl -> Just x Nothing -> Nothing 

Of course, writing type tags is a nuisance. But why keep the dog and bark yourself?

 class TypeMe x where myType :: Type x instance TypeMe Int where myType = Int instance TypeMe Char where myType = Char instance TypeMe x => TypeMe [x] where myType = List myType cell :: TypeMe x => x -> Cell cell x = x ::: myType 

And now we can do things like

 myCells :: [Cell] myCells = [cell (length "foo"), cell "foo"] 

and then we get

 > gimme Int (head myCells) Just 3 

Of course, everything would be much more neat if we did not have to build a singleton structure and could just match patterns with types that we could save at runtime. I expect that we will get there when the mythical quantifier pi becomes less mythical.