Dimitrios Vytiniotis dimitriv at cis.upenn.edu
Mon Oct 30 20:19:18 EST 2006

```Just noticed Joost Visser's message but since I
had (essentially a very similar) response I thought I might
send it off as well ... It includes the conditional cases.

Regards,
-d

{-# OPTIONS_GHC -fglasgow-exts #-}

module Main where

data Term a where
Lit  :: Int -> Term Int
Inc  :: Term Int -> Term Int
IsZ  :: Term Int -> Term Bool
If   :: Term Bool -> Term a -> Term a -> Term a
Pair :: Term a -> Term b -> Term (a,b)
Fst  :: Term (a,b) -> Term a
Snd  :: Term (a,b) -> Term b

data Expr = ELit Int
| EInc Expr
| EIsZ Expr
| EPair Expr Expr
| EIf Expr Expr Expr
| EFst Expr
| ESnd Expr

-- Give a GADT for representation types
data R a where
Rint :: R Int
Rbool :: R Bool
Rpair :: R a -> R b -> R (a,b)

-- Give an existential type with a type representation
data TermEx where
MkTerm :: R a -> Term a -> TermEx

-- we use Weirich's higher-order type-safe cast to avoid deep traversals
-- one can replace the type_cast with a more simple traversal-based
-- version.

data CL c a d = CL (c (d,a))
data CR c a d = CR (c (a,d))

type_cast :: forall a b c. R a -> R b -> c a -> c b
type_cast Rint Rint x = x
type_cast Rbool Rbool x = x
type_cast (Rpair (ra::(R a0)) (rb::(R b0)))
(Rpair (ra'::(R a0')) (rb'::(R b0'))) x =
let g = (type_cast ra ra' :: ( (CL c b0)  a0 -> (CL c b0) a0' ))
h = (type_cast rb rb' :: ( (CR c a0') b0 -> (CR c a0') b0'))
in case (g (CL x)) of
CL x' -> case (h (CR x')) of
CR y' -> y'
type_cast _ _ _  = error "cannot cast!"

-- give only the cases for Eif and Elit, the others are similar
my_read (ELit i) = MkTerm Rint (Lit i);
my_read (EIf p t e) =
MkTerm rb b ->
case rb of
Rbool ->