data Rep :: *0 ~> *0 where
   Rint  :: Rep Int
   Rbool :: Rep Bool
   Rpair :: Rep a -> Rep b -> Rep (a,b)
   Rarr  :: Rep a -> Rep b -> Rep (a -> b)







zero Rint = 0
zero Rbool = False
zero (Rpair t1 t2) = (zero t1, zero t2)
zero (Rarr t1 t2)  = \x -> zero t2

-- print type
pt :: Rep a -> String
pt Rint = "Int"
pt Rbool = "Bool"
pt (Rpair t1 t2) = "(" ++ pt t1 ++ "," ++ pt t2 ++ ")"
pt (Rarr t1 t2) = "(" ++ pt t1 ++ "->" ++ pt t2 ++ ")"

-- casting between two types

cast :: Rep a -> Rep b -> Maybe (a -> b)
cast Rint Rint = Just id
cast Rbool Rbool = Just id
cast (Rpair t1 t2) (Rpair s1 s2) = 
    case (cast t1 s1, cast t2 s2) of 
            (Just f, Just g) -> Just (\(x,y) -> (f x,g y))
            (_     , _)      -> Nothing
cast (Rtriple t1 t2 t3) (Rpair s1 s2) = 
cast (Rarr t1 t2) (Rarr s1 s2) = 
    case (cast s1 t1, cast t2 s2) of 
            (Just f, Just g) -> Just (\h -> g . h . f)
	     -- f :: s1 -> t1
	     -- h :: t1 -> t2  
             -- g :: t2 -> s2 
            (_     , _     ) -> Nothing
cast _ _ = Nothing

{karl Int} = Maybe Int 
{karl Bool} = Maybe Bool
{karl (a,b)} = Maybe ({karl a}, {karl b})
{karl (a -> b)} = Maybe ({karl a} -> {karl b})

karls_cast :: Rep a -> Rep b -> a -> {karl b}


-- more traditional dynamics

data Dyn = Int Int | Bool Bool | Pair Dyn Dyn | Fn (Dyn -> Dyn)

toDyn   :: Rep a -> a -> Dyn
toDyn Rint i = Int i
toDyn Rbool b = Bool b
toDyn (Rpair t1 t2) (x,y) = Pair (toDyn t1 x) (toDyn t2 y)
toDyn (Rarr t1 t2) f = Fn ((toDyn t2) . f . (fromDyn t1))

fromDyn :: Rep a -> Dyn -> a
fromDyn Rint (Int i) = i
fromDyn Rbool (Bool b) = b
fromDyn (Rpair t1 t2) (Pair x y) = (fromDyn t1 x, fromDyn t2 y)
fromDyn (Rarr t1 t2) (Fn f) = ((fromDyn t2). f . (toDyn t1))







-- optimized (?) data structure
my_list :: *0 ~> *0
{my_list (a,b)} = ([a],[b])
{my_list Int}   = [Int]
{my_list Bool}  = [Bool]
{my_list (a -> b)} = [a -> b]

my_cons :: Rep a -> a -> {my_list a} -> {my_list a}
my_cons (Rpair t1 t2) (x,y) (xs,ys) = (x:xs, y:ys)
my_cons Rint i is = i : is
my_cons Rbool b bs = b : bs
my_cons (Rarr _ _) f fs = f : fs

my_hd   :: Rep a -> {my_list a} -> a
my_hd (Rpair t1 t2) (x:xs,y:ys) = (x,y)
my_hd Rint  (i:is) = i
my_hd Rbool (b:bs) = b 
my_hd (Rarr _ _) (f:fs) = f

my_tl   :: Rep a -> {my_list a} -> {my_list a}
my_tl (Rpair t1 t2) (x:xs,y:ys) = (xs,ys)
my_tl Rint  (i:is) = is
my_tl Rbool (b:bs) = bs
my_tl (Rarr _ _) (f:fs) = fs





-- another one
swap_type :: *0 ~> *0 
{swap_type Int} = Int
{swap_type Bool} = Bool
{swap_type (a,b)} = ( {swap_type b},{swap_type a} )
{swap_type (a -> b)} = a -> b

swap_term :: Rep a -> a -> {swap_type a}
swap_term Rint i = i 
swap_term Rbool b = b
swap_term (Rpair t1 t2) (x,y) = (swap_term t2 y, swap_term t1 x)
swap_term (Rarr t1 t2) f = f 






-- marshalling
data Id t = ID Int

get_id :: (a -> b) -> Int
get_id f = 2

get_f  :: Int -> (a -> b)
get_f _ = f where f x = f x

tran :: *0 ~> *0
{tran Int} = Int
{tran Bool} = Bool
{tran (a -> b)} = Id (a -> b)
{tran (a,b)} = ({tran a},{tran b})

marshall :: Rep a -> a -> {tran a}
marshall Rint i = i
marshall Rbool b = b
marshall (Rarr r1 r2) f = ID (get_id f)
marshall (Rpair r1 r2) (x,y) = (marshall r1 x, marshall r2 y)