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))
|
