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. OK, I Understand
 
Top