• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Sep 17th, 2019 100 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. data Tm = Var Int | Ann Tm Tm | Abs Tm | App Tm Tm | Pi Tm Tm | Fix Tm | Uni
2. data Clos = Clos Tm Env
3. data Dm = DVar Int | DAbs Clos | DNeutral Int [Dm] | DPi Dm Clos | DFix Clos | DUni
4. type Env = [Dm]
5.
6. capp :: Clos -> Dm -> Dm
7. capp (Clos b e) t = eval (t : e) b
8.
9. vapp :: Dm -> Dm -> Dm
10. vapp a b =
11.   case a of
12.     DAbs c -> capp c b
13.     DFix c -> vapp (capp c a) b
14.     DVar i -> DNeutral i [b]
15.     DNeutral i as -> DNeutral i (b : as)
16.     tm -> error \$ "impossible vapp"
17.
18. eval :: Env -> Tm -> Dm
19. eval env Uni = DUni
20. eval env (Var i) = env !! i
21. eval env (Ann t ty) = eval env t
22. eval env (Abs b) = DAbs (Clos b env)
23. eval env (Pi t b) = DPi (eval env t) (Clos b env)
24. eval env (Fix b) = DFix (Clos b env)
25. eval env (App a b) = vapp (eval env a) (eval env b)
26.
27. quote :: Int -> Dm -> Tm
28. quote k DUni = Uni
29. quote k (DVar i) = Var (k - (i + 1))
30. quote k (DAbs (Clos b e)) =
31.   Abs (quote (k + 1) (eval (DVar k : e) b))
32. quote k (DPi t (Clos b e)) =
33.   Pi (quote k t) (quote (k + 1) (eval (DVar k : e) b))
34. quote k (DFix (Clos b e)) =
35.   Fix (quote (k + 1) (eval (DVar k : e) b))
36. quote k (DNeutral i as) =
37.   foldr (flip App) (Var (k - (i + 1))) (map (quote k) as)
38.
39. nf :: Tm -> Tm
40. nf t = quote 0 (eval [] t)
41.
42. eqtype :: Int -> Dm -> Dm -> Bool
43. eqtype k DUni DUni = True
44. eqtype k (DVar i) (DVar j) = i == j
45. eqtype k (DFix c) (DFix c') =
46.   let v = DVar k in
47.   eqtype (k + 1) (capp c v) (capp c' v)
48. eqtype k (DAbs c) (DAbs c') =
49.   let v = DVar k in
50.   eqtype (k + 1) (capp c v) (capp c' v)
51. eqtype k (DAbs c) t' =
52.   let v = DVar k in
53.   eqtype (k + 1) (capp c v) (vapp t' v)
54. eqtype k t' (DAbs c) =
55.   let v = DVar k in
56.   eqtype (k + 1) (vapp t' v) (capp c v)
57. eqtype k v@(DFix c) t' =
58.   eqtype (k + 1) (capp c v) t'
59. eqtype k t' v@(DFix c) =
60.   eqtype (k + 1) t' (capp c v)
61. eqtype k (DNeutral i as) (DNeutral i' as') =
62.   i == i' && and (zipWith (eqtype k) as as')
63. eqtype k (DPi t c) (DPi t' c') =
64.   let v = DVar k in
65.   eqtype k t t' && eqtype (k + 1) (capp c v) (capp c' v)
66. eqtype _ _ _ = False
67.
68. type Err t = Either String t
69.
70. err :: String -> Err t
71. err = Left
72.
73. index :: Int -> [t] -> String -> Err t
74. index _ [] msg = err msg
75. index 0 (h : _) _ = return h
76. index i (_ : t) msg = index (i - 1) t msg
77.
78. assert :: Bool -> String -> Err ()
79. assert b msg = if b then return () else err msg
80.
81. check :: Env -> Env -> Int -> Tm -> Dm -> Err ()
82. check tenv venv k (Abs b) (DPi t b') =
83.   let v = DVar k in
84.   check (t : tenv) (v : venv) (k + 1) b (capp b' v)
85. check tenv venv k (Abs b) tm@(DFix b') =
86.   check tenv venv k (Abs b) (capp b' tm)
87. check tenv venv k tm@(Fix b) t =
88.   check (t : tenv) (eval venv tm : venv) (k + 1) b t
89. check tenv venv k t ty = do
90.   ty' <- synth tenv venv k t
91.   assert (eqtype k ty' ty) \$ "type are not equal " ++ (show \$ quote k ty') ++ " ~ " ++ (show \$ quote k ty)
92.
93. synthapp :: Env -> Env -> Int -> Tm -> Dm -> Tm -> Err Dm
94. synthapp tenv venv k tm ta b =
95.   case ta of
96.     DPi t c -> do
97.       check tenv venv k b t
98.       return \$ capp c (eval venv b)
99.     DFix c -> synthapp tenv venv k tm (capp c ta) b
100.     ty -> err \$ "not a pi type in " ++ (show tm) ++ ": " ++ (show \$ quote k ty)
101.
102. synth :: Env -> Env -> Int -> Tm -> Err Dm
103. synth tenv venv k Uni = return DUni
104. synth tenv venv k (Var i) = index i tenv \$ "var " ++ (show i) ++ " not found"
105. synth tenv venv k (Ann t ty) = do
106.   check tenv venv k ty DUni
107.   let ty' = eval venv ty
108.   check tenv venv k t ty'
109.   return ty'
110. synth tenv venv k (Pi t b) = do
111.   check tenv venv k t DUni
112.   check (eval venv t : tenv) (DVar k : venv) (k + 1) b DUni
113.   return DUni
114. synth tenv venv k tm@(App a b) = do
115.   ta <- synth tenv venv k a
116.   synthapp tenv venv k tm ta b
117. synth tenv venv k t = err \$ "cannot synth " ++ (show t)
118.
119. -- pretty
120. instance Show Tm where
121.   show (Var i) = show i
122.   show (Ann t ty) = "(" ++ (show t) ++ " : " ++ (show ty) ++ ")"
123.   show (Abs b) = "(\\" ++ (show b) ++ ")"
124.   show (App a b) = "(" ++ (show a) ++ " " ++ (show b) ++ ")"
125.   show (Pi t b) = "(" ++ (show t) ++ " -> " ++ (show b) ++ ")"
126.   show (Fix b) = "(fix " ++ (show b) ++ ")"
127.   show Uni = "*"
128.
129. -- testing
130. v :: Int -> Tm
131. v = Var
132.
133. a :: Tm -> [Tm] -> Tm
134. a f as = foldl App f as
135.
136. nat :: Tm -- fix r. (t:*) -> t -> (r -> t) -> t  :  *
137. nat = Ann (Fix (Pi Uni \$ Pi (v 0) \$ Pi (Pi (v 2) (v 2)) (v 2))) Uni
138.
139. z :: Tm -- \t z s. z : nat
140. z = Ann (Abs \$ Abs \$ Abs \$ v 1) nat
141.
142. s :: Tm -- \n t z s. s n : nat
143. s = Ann (Abs \$ Abs \$ Abs \$ Abs \$ App (v 0) (v 3)) (Pi nat nat)
144.
145. bool :: Tm -- (t:*) -> t -> t -> t
146. bool = Pi Uni \$ Pi (v 0) \$ Pi (v 1) (v 2)
147.
148. tru :: Tm -- \t a b. a : bool
149. tru = Ann (Abs \$ Abs \$ Abs \$ v 1) bool
150.
151. fls :: Tm -- \t a b. b : bool
152. fls = Ann (Abs \$ Abs \$ Abs \$ v 0) bool
153.
154. bnot :: Tm -- \b. b bool fls tru : bool -> bool
155. bnot = Ann (Abs \$ a (v 0) [bool, fls, tru]) (Pi bool bool)
156.
157. neven :: Tm -- fix r. \n. n bool tru (\m. not (r m)) : nat -> bool
158. neven = Ann (Fix \$ Abs \$ a (v 0) [bool, tru, Abs (App bnot (App (v 2) (v 0)))]) (Pi nat bool)
159.
160. term :: Tm -- even (s (s z)) ~> tru
161. term = App neven (App s (App s z))
162.
163. main :: IO ()
164. main = do
165.   putStrLn \$ show term
166.   putStrLn \$ show \$ fmap (quote 0) \$ synth [] [] 0 term
167.   putStrLn \$ show \$ nf term
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top