summaryrefslogtreecommitdiff
path: root/testsuite/tests/gadt/tdpe.hs
blob: 58a4b85094f35fc6bd6faaa495dc647e93d5e670 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
{-# LANGUAGE GADTs #-}

module Tdpe where

data Type t where
    TBase :: Type Base
    TFun  :: Type a -> Type b -> Type (a -> b)

b :: Type Base
b = TBase

newtype Base = In { out :: Term Base }

data Term t where
    App :: Term (a->b) -> Term a -> Term b
    Fun :: (Term a -> Term b) -> Term (a->b)

reify :: Type t -> t -> Term t
reify (TBase) v    = out v
reify (TFun a b) v = Fun (\x -> reify b (v (reflect a x)))

reflect :: Type t -> Term t -> t
reflect (TBase) e    = In e
reflect (TFun a b) e = \x -> reflect b (App e (reify a x))