added let ... in ...

README.md

@@ -10,6 +10,8 @@ A dependently typed system
   * pi types
   * type of types
 
+* let ... in ...
+
 * Unit type
 
 * Empty type
@@ -20,21 +22,26 @@ A dependently typed system
 
 # TODO
 
-* Let ... in ...
-
 * Parser
 
 * Fun types
   * Id
 
+* Repl
+
 * Universes
 
+* Performence optimisation
+  * Memoize normalisation and conversion somehow?
+
 * Implicit arguments
 
 * (indexed) inductive datatypes
 
 * Write down the rules (I'll not get this far)
 
+* Compile to scheme
+
 # References
 
 Some of the material I found helpful in groking dependent type checking:

src/Check.idr

@@ -15,6 +15,14 @@ import Convert
 
 %default total
 
+-- extend environment, used to ensure environment is always in normal form
+extV : Ctx n -> Value -> PI (Ctx (S n))
+extV ctx val = whnf val >>= pure . (`Data.Vect.(::)` ctx)
+
+-- to extend, closure env, term
+extT : Ctx m -> Ctx n -> Term n -> PI (Ctx (S m))
+extT ctx env = extV ctx . VClos env
+
 mutual
   public export
   -- terms types expected term
@@ -25,7 +33,7 @@ mutual
       TLam sc    => case xpt of
                          VClos env (TPi a b) => do
                            v <- VGen <$> fresh
-                           check (v :: trs) (VClos env a :: tys) (VClos (v :: env) b) sc
+                           check (v :: trs) !(extT tys env a) (VClos (v :: env) b) sc
                          _ => oops "expected pi"
 
       -- pi and sigma could be inferred /shrug
@@ -33,7 +41,7 @@ mutual
                          VType => do
                            v <- VGen <$> fresh
                            guardS "Pi a" =<< check trs tys VType a 
-                           check (v :: trs) (VClos trs a :: tys) VType b
+                           check (v :: trs) !(extT tys trs a) VType b
                          _ => oops "expected type"
 
       TSigma a b => case xpt of
@@ -49,6 +57,10 @@ mutual
                            check trs tys (VClos env b `VApp` VClos trs x) y
                          _ => oops "expected sigma"
 
+      TLet ty tr tri => do
+        guardS "let" =<< check trs tys (VClos trs ty) tr
+        check !(extT trs trs tr) !(extT tys trs ty) xpt tri
+
       _       => convert xpt =<< infer trs tys tr
 
   -- terms types term
@@ -59,7 +71,8 @@ mutual
                               \case
                                  VClos env (TPi a b) => do
                                    guardS "app x" =<< check trs tys (VClos env a) x
-                                   pure (VClos (VClos trs x :: env) b)
+                                   tr <- whnf (VClos trs x)
+                                   pure (VClos (tr :: env) b)
 
                                  _ => oops "expected infer pi"
 
@@ -99,6 +112,10 @@ mutual
     pure (VClos trs (TPi (TSigma a b) (weakTr c `TApp` TVar 0)))
                                       
 
+  infer trs tys (TLet ty tr tri) = do
+        guardS "let infer" =<< check trs tys (VClos trs ty) tr
+        infer !(extT trs trs tr) !(extT tys trs ty) tri
+
   infer trs tys x          = oops ("cannot infer type" ++ show x)
 
 public export

src/Convert.idr

@@ -14,8 +14,6 @@ import Data.Vect
 
 %default total
 
-{- TODO: I should throw eval, eval, convert into a helper sometime -}
-
 public export
 convert : Value -> Value -> PI Bool
 convert u1 u2 = do
@@ -45,54 +43,45 @@ convert u1 u2 = do
 
       (VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do
         v <- VGen <$> fresh
-        guard =<< convert (VClos env1 a1) (VClos env2 a2)
+
+        s1 <- case headM env1 of
+                   Nothing => pure ""
+                   Just x  => pure (show x)
+
+        s2 <- case headM env2 of
+                   Nothing => pure ""
+                   Just x  => pure (show x)
+
+        guardS (s1 ++ " | " ++ s2) =<< convert (VClos env1 a1) (VClos env2 a2)
         convert (VClos (v :: env1) b1) (VClos (v :: env2) b2)
 
       (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
-        c1' <- eval env1 c1
+        termGuard env1 env2 c1 c2
-        c2' <- eval env2 c2
+        termConv  env1 env2 st1 st2
-        guard =<< convert c1' c2'
-        st1' <- eval env1 st1
-        st2' <- eval env2 st2
-        convert st1' st2'
 
-      (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => do
+      (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2
-        c1' <- eval env1 c1
-        c2' <- eval env2 c2
-        convert c1' c2'
 
-      -- lmao
       (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do
-        c1' <- eval env1 c1
+        termGuard env1 env2 c1 c2
-        c2' <- eval env2 c2
+        termGuard env1 env2 z1 z2
-        guard =<< convert c1' c2'
+        termConv  env1 env2 s1 s2
-        z1' <- eval env1 z1
-        z2' <- eval env2 z2
-        guard =<< convert z1' z2'
-        s1' <- eval env1 s1
-        s2' <- eval env2 s2
-        convert s1' s2'
 
       (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do
-        a1' <- eval env1 a1
+        termGuard env1 env2 a1 a2
-        a2' <- eval env2 a2
+        termConv  env1 env2 b1 b2
-        guard =<< convert a1' a2'
-        b1' <- eval env1 b1
-        b2' <- eval env2 b2
-        convert b1' b2'
 
       (VClos env1 (TSigInd a1 b1 c1 f1), VClos env2 (TSigInd a2 b2 c2 f2)) => do
-        a1' <- eval env1 a1
+        termGuard env1 env2 a1 a2
-        a2' <- eval env2 a2
+        termGuard env1 env2 b1 b2
-        guard =<< convert a1' a2'
+        termGuard env1 env2 c1 c2
-        b1' <- eval env1 b1
+        termConv  env1 env2 f1 f2
-        b2' <- eval env2 b2
-        guard =<< convert b1' b2'
-        c1' <- eval env1 c1
-        c2' <- eval env2 c2
-        guard =<< convert c1' c2'
-        f1' <- eval env1 f1
-        f2' <- eval env2 f2
-        convert f1' f2'
                                   
       _ => pure False
+  where
+    termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool
+    termConv env1 env2 a1 a2 = do
+      a1' <- eval env1 a1
+      a2' <- eval env2 a2
+      convert a1' a2'
+    termGuard : Ctx n -> Ctx m -> Term n -> Term m -> PI ()
+    termGuard env1 env2 a1 a2 = guardS "termGuard" =<< termConv env1 env2 a1 a2

src/Misc.idr

@@ -5,6 +5,7 @@ import Control.Monad.Identity
 import Control.Monad.Either
 
 import Data.Nat
+import Data.Vect
 
 %default total
 
@@ -45,41 +46,9 @@ fresh = do
 
 public export
 logS : String -> PI ()
-logS = tell . (:: [])
+logS = tell . (`Prelude.(::)` [])
 
 public export
-lteTransp : LTE a b -> a = c -> b = d -> LTE c d
+headM : Vect n a -> Maybe a
-lteTransp p Refl Refl = p
+headM [] = Nothing
-
+headM (x :: _) = Just x
-public export
-lteS : {n : _} -> LTE n (S n)
-lteS {n = Z}   = LTEZero
-lteS {n = S n} = LTESucc lteS
-
-public export
-lteSplit : {m : _} -> LTE n m -> Either (n = m) (LT n m)
-lteSplit {m = Z} LTEZero = Left Refl
-lteSplit {m = S m} LTEZero = Right (LTESucc LTEZero)
-lteSplit {m = S m} (LTESucc p) = case lteSplit p of
-                                      Left p2 => Left (cong S p2)
-                                      Right p2 => Right (LTESucc p2)
-
-public export
-minusLte : {m,n : _} -> LTE (minus n (S m)) n
-minusLte {n = Z} = LTEZero
-minusLte {n = S n} {m = Z} = rewrite minusZeroRight n in lteSuccRight reflexive
-minusLte {n = S n} {m = S m} = lteSuccRight (minusLte {n = n} {m = m})
-
-public export
-prevEq : (i, j : Nat) -> S i = S j -> i = j
-prevEq Z Z Refl = Refl
-prevEq (S i) (S _) Refl = Refl
-
-public export
-natEqDecid : (n, m : Nat) -> Either (Not (n = m)) (n = m) 
-natEqDecid Z Z        = Right Refl
-natEqDecid (S _) Z    = Left absurd
-natEqDecid Z (S _)    = Left absurd
-natEqDecid (S n) (S m) = case natEqDecid n m of
-                              Right p => Right (cong S p)
-                              Left  p => Left  (p . prevEq n m)

src/Normalize.idr

@@ -15,7 +15,6 @@ import Data.Vect
 
 mutual
   public export
-  -- no computational rule for ⊥
   app : Value -> Value -> PI Value
   app (VClos env (TLam sc))       x = eval (x :: env) sc
 
@@ -74,6 +73,10 @@ mutual
     b' <- eval env b
     pure (VPair a' b')
 
+  eval env (TLet ty tr tri) = do
+    tr' <- eval env tr
+    eval (tr' :: env) tri
+
   eval env tr          = pure (VClos env tr)
 
 public export
@@ -82,5 +85,9 @@ whnf (VApp f x) = do
   f' <- whnf f
   x' <- whnf x
   app f' x'
+whnf (VPair a b) = do
+  a' <- whnf a
+  b' <- whnf b
+  pure (VPair a' b')
 whnf (VClos env tr) = eval env tr
 whnf v              = pure v

src/Term.idr

@@ -30,6 +30,8 @@ data Term : (_ : Index) -> Type where
   TPair   : Term n -> Term n -> Term n                     -- Sum constructor _,_
   TSigInd : Term n -> Term n -> Term n -> Term n -> Term n -- A B C f : (x : Σ _ : A , B _) → C x
 
+  TLet    : Term n -> Term n -> Term (S n) -> Term n       -- let _ : #0 := #1 in #2
+
   TLam    : Term (S n) -> Term n                 -- Lambda abstraction (λ _ . Scope)
   TPi     : Term n -> Term (S n) -> Term n       -- Pi type            (∏ _ : A . B _ )
 
@@ -54,15 +56,16 @@ Show (Term n) where
   show (TSuc n)        = "suc (" ++ show n ++ ")"
   show (TNatInd c z s) = "ℕ-ind (" ++ show c ++ ") (" ++ show z ++ ") (" ++ show s ++ ")"
 
-  show (TSigma a b)    = "TSigma (" ++ show a ++ ") (" ++ show b ++ ")"
+  show (TSigma a b)    = "Σ (" ++ show a ++ ") (" ++ show b ++ ")"
-  show (TPair a b)     = "TPair (" ++ show a ++ ") (" ++ show b ++ ")"
+  show (TPair a b)     = "Pair (" ++ show a ++ ") (" ++ show b ++ ")"
   show (TSigInd a b c f) = "Σ-ind (" ++ show a ++ ") (" ++ show b ++ ") (" ++ show c ++ ") (" ++ show f ++ ")"
+  show (TLet ty tr itr) = "let : (" ++ show ty ++ ") := (" ++ show tr ++ ") in (" ++ show itr ++ ")"
 
-  show (TLam sc)       = "TLam (" ++ show sc ++ ")"
+  show (TLam sc)       = "λ (" ++ show sc ++ ")"
-  show (TPi  ty sc)    = "TPi (" ++ show ty ++ ") (" ++ show sc ++ ")"
+  show (TPi  ty sc)    = "Π (" ++ show ty ++ ") (" ++ show sc ++ ")"
 
-  show (TApp f x)      = "TApp (" ++ show f ++ ") (" ++ show x ++ ")"
+  show (TApp f x)      = "(" ++ show f ++ ") TApp (" ++ show x ++ ")"
-  show (TVar i)        = "TVar " ++ show i
+  show (TVar i)        = "Var " ++ show i
 
 public export
 weakTr : Term n -> Term (S n)
@@ -82,6 +85,7 @@ weakTr = go 0
     go n (TSigma a b)      = TSigma (go n a) (go n b)
     go n (TPair a b)       = TPair (go n a) (go n b)
     go n (TSigInd a b c f) = TSigInd (go n a) (go n b) (go n c) (go n f)
+    go n (TLet ty tr itr)  = TLet (go n ty) (go n tr) (go (FS n) itr)
     go n (TLam sc)         = TLam (go (FS n) sc)
     go n (TPi  ty sc)      = TPi (go n ty) (go (FS n) sc)
     go n (TApp f x)        = TApp (go n f) (go n x)

src/Tests.idr

@@ -43,12 +43,18 @@ addition = TNatInd (TLam (TPi TNat TNat))
                    (TLam (TVar 0)) 
                    (TLam {-n-} (TLam {-n+-} (TLam {-m-} (TSuc (TVar 1 `TApp` TVar 0)))))
 
-addition_type : Either String (Bool, List String)
+additionty : Term 0
-addition_type = typecheck addition (TPi TNat (TPi TNat TNat))
+additionty = TPi TNat (TPi TNat TNat)
+
+additionty_test : Either String (Bool, List String)
+additionty_test = typecheck additionty TType
+
+addition_test : Either String (Bool, List String)
+addition_test = typecheck addition additionty
 
 {- 2 + 1 = 3 -}
-add_test : Either String (Bool, List String)
+addition_compute_test : Either String (Bool, List String)
-add_test = resolve action
+addition_compute_test = resolve action
   where
     action : PI Bool
     action = do
@@ -61,12 +67,18 @@ multi = TNatInd (TLam (TPi TNat TNat))
                 (TLam TZero)
                 (TLam {-n-} (TLam {-n*-} (TLam {-m-} (weakTr3 addition `TApp` TVar 0 `TApp` (TVar 1 `TApp` TVar 0)))))
 
-multi_type : Either String (Bool, List String)
+multity : Term 0
-multi_type = typecheck multi (TPi TNat (TPi TNat TNat))
+multity = TPi TNat (TPi TNat TNat)
+
+multity_test : Either String (Bool, List String)
+multity_test = typecheck multity TType
+
+multi_test : Either String (Bool, List String)
+multi_test = typecheck multi multity
 
 {- 2 * 3 = 6 -}
-multi_test : Either String (Bool, List String)
+multi_compute_test : Either String (Bool, List String)
-multi_test = resolve action
+multi_compute_test = resolve action
   where
     action : PI Bool
     action = do
@@ -92,6 +104,9 @@ pr1 = TLam {- A : Type -}
            (TLam {- B : A → Type -}
                  (TSigInd (TVar 1) (TVar 0) (TLam {-ΣAB-} (TVar 2)) (TLam (TLam (TVar 1)))))
 
+pr1ty_test : Either String (Bool, List String)
+pr1ty_test = typecheck pr1ty TType
+
 pr1_test : Either String (Bool, List String)
 pr1_test = typecheck pr1 pr1ty
 
@@ -115,3 +130,26 @@ pr2ty_test = typecheck pr2ty TType
 
 pr2_test : Either String (Bool, List String)
 pr2_test = typecheck pr2 pr2ty
+
+pr2ty_let : Term 0
+pr2ty_let = TLet pr1ty pr1 {- pr1 : pr1ty -}
+                 (TPi TType {- A : Type -}
+                      (TPi (TPi (TVar 0) TType) {- B : A → Type -}
+                           (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
+                                (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0)))))
+
+pr2_let : Term 0
+pr2_let = TLet pr1ty pr1 {- pr1 : pr1ty -}
+               (TLam {- A : Type -} 
+                     (TLam {- B : A → Type -}
+                           (TSigInd (TVar 1)
+                                    (TVar 0)
+                                    (TLam {-ΣAB-}
+                                          (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0)))
+                                    (TLam (TLam (TVar 0))))))
+
+pr2ty_let_test : Either String (Bool, List String)
+pr2ty_let_test = typecheck pr2ty_let TType
+
+pr2_let_test : Either String (Bool, List String)
+pr2_let_test = typecheck pr2_let pr2ty_let