testsuite/tests/gadt/tdpe.hs

   1 {-# LANGUAGE GADTs #-}
   2
   3 module Tdpe where
   4
   5 data Type t where
   6     TBase :: Type Base
   7     TFun  :: Type a -> Type b -> Type (a -> b)
   8
   9 b :: Type Base
  10 b = TBase
  11
  12 newtype Base = In { out :: Term Base }
  13
  14 data Term t where
  15     App :: Term (a->b) -> Term a -> Term b
  16     Fun :: (Term a -> Term b) -> Term (a->b)
  17
  18 reify :: Type t -> t -> Term t
  19 reify (TBase) v    = out v
  20 reify (TFun a b) v = Fun (\x -> reify b (v (reflect a x)))
  21
  22 reflect :: Type t -> Term t -> t
  23 reflect (TBase) e    = In e
  24 reflect (TFun a b) e = \x -> reflect b (App e (reify a x))