implemented types ⊤, ⊥, and ℕ

README.md

@@ -1,19 +1,37 @@
 # pi
+
 A dependently typed system
 
+# Implemented
+
+* A Basic dependent lambda calculus
+  * lambda abstractions
+  * variables
+  * pi types
+  * type of types
+
+* Unit type
+
+* Empty type
+
+* Natural numbers
+
 # TODO
 
-* Some fun types
+* Fun types
-  * ⊤
-  * ⊥
-  * ℕ
   * Σ
   * Id
 
+* Parser
+
 * Implicit arguments
 
 * Universes
 
+* (indexed) inductive datatypes
+
+* Write down the rules (I'll not get this far)
+
 # References
 
 Some of the material I found helpful in groking dependent type checking:

src/Check.idr

@@ -41,16 +41,42 @@ mutual
 
   -- terms types term
   infer : Ctx n -> Ctx n -> Term n -> PI Value
-  infer trs tys (TVar i _) = pure (index (natToFinLT i) tys)
+  infer trs tys (TVar i)   = pure (index i tys)
   infer trs tys TType      = pure VType
   infer trs tys (TApp f x) = infer trs tys f >>= whnf >>=
                               \case
                                  VClos env (TPi a b) => do
-                                   if !(check trs tys (VClos env a) x)
+                                   guard =<< check trs tys (VClos env a) x
-                                      then pure (VClos (VClos trs x :: env) b)
+                                   pure (VClos (VClos trs x :: env) b)
-                                      else oops "application"
 
                                  _ => oops "expected infer pi"
+
+  infer trs tys TTop      = pure VType
+  infer trs tys TBot      = pure VType
+  infer trs tys TNat      = pure VType
+  infer trs tys TStar     = pure VTop
+  infer trs tys TZero     = pure VNat
+  infer trs tys (TSuc n)  = do 
+    guard =<< check trs tys VNat n
+    pure VNat
+
+  infer trs tys (TTopInd c st) = do
+    guard =<< check trs tys (VClos trs (TPi TTop TType)) c
+    guard =<< check trs tys (VApp (VClos trs c) VStar)   st
+    pure (VClos trs (TPi TTop (TApp (weakTr c) (TVar 0))))
+
+  infer trs tys (TBotInd c) = do
+    guard =<< check trs tys (VClos trs (TPi TBot TType)) c
+    pure (VClos trs (TPi TBot (TApp (weakTr c) (TVar 0))))
+
+  infer trs tys (TNatInd c z s) = do
+    guard =<< check trs tys (VClos trs (TPi TNat TType)) c
+    guard =<< check trs tys (VApp (VClos trs c) (VNatTr 0)) z
+    guard =<< check trs tys (VClos trs (TPi TNat 
+                                            (TPi (TApp (weakTr c) (TVar 0)) 
+                                                 (TApp (weakTr2 c) (TSuc (TVar (FS FZ))))))) s
+    pure (VClos trs (TPi TNat (TApp (weakTr c) (TVar 0))))
+
   infer trs tys _          = oops "cannot infer type"
 
 public export

src/Convert.idr

@@ -24,6 +24,13 @@ convert u1 u2 = do
   assert_total $ -- :(
     case (u1', u2') of
       (VType, VType) => pure True
+      (VTop, VTop)   => pure True
+      (VStar, VStar) => pure True
+      (VBot, VBot)   => pure True
+      (VNat, VNat)   => pure True
+
+      (VNatTr n, VNatTr m) => pure (n == m)
+
       (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 
                                        <*> delay <$> convert x1 x2
       (VGen k1, VGen k2) => pure (k1 == k2)
@@ -39,4 +46,29 @@ convert u1 u2 = do
                          (VClos env2 a2)
              <*> delay <$> convert (VClos (v :: env1) b1)
                                    (VClos (v :: env2) b2)
+
+      (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
+        c1' <- eval env1 c1
+        c2' <- eval env2 c2
+        st1' <- eval env1 st1
+        st2' <- eval env2 st2
+        (&&) <$> convert c1' c2' <*> delay <$> convert st1' st2'
+
+      (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => do
+        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
+        c2' <- eval env2 c2
+        z1' <- eval env1 z1
+        z2' <- eval env2 z2
+        s1' <- eval env1 s1
+        s2' <- eval env2 s2
+        b1  <- (&&) <$> convert c1' c2' <*> delay <$> convert z1' z2'
+        guard b1 
+        convert s1' s2'
+                                  
       _ => pure False

src/Normalize.idr

@@ -15,18 +15,52 @@ 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
+
+  app (VClos env (TTopInd c st))  VTop       = eval env st
+  app f@(VClos env (TTopInd c st))  x        = logS ("⊤-ind applied to " ++ show x)
+                                               >> pure (VApp f x)
+
+  app (VClos env (TNatInd _ z s)) (VNatTr n) = do
+    z'  <- eval env z
+    s'  <- eval env s
+    assert_total (nind z' s' n) -- :(
+    where
+      nind : Value -> Value -> Nat -> PI Value
+      nind z s 0     = pure z
+      nind z s (S n) = do
+        rec <- nind z s n
+        sn <- app s (VNatTr n)
+        app sn rec
+
+  app f@(VClos env (TNatInd _ z s)) x          = logS ("ℕ-ind applied to " ++ show x)
+                                                 >> pure (VApp f x)
+
   app f x = pure (VApp f x)
 
   public export
   eval : Ctx n -> Term n -> PI Value
-  eval env (TVar i _) = pure (index (natToFinLT i) env)
+  eval env (TVar i)   = pure (index i env)
   eval env (TApp f x) = do
     f' <- eval env f
     x' <- eval env x
     assert_total (app f' x') -- :(
   eval env TType      = pure VType
+  eval env TTop       = pure VTop
+  eval env TStar      = pure VStar
+  eval env TBot       = pure VBot
+  eval env TNat       = pure VNat
+  eval env TZero      = pure (VNatTr 0)
+
+  eval env (TSuc n)   = do
+    n' <- eval env n
+    case n' of
+         VNatTr n => pure (VNatTr (S n))
+         x        => logS ("suc applied to " ++ show x)
+                     >> pure (VClos env (TSuc n))
+
   eval env tr         = pure (VClos env tr)
 
 public export

src/Term.idr

@@ -1,6 +1,6 @@
 module Term
 
-import Data.Nat
+import Data.Fin
 
 import Misc
 
@@ -13,15 +13,79 @@ import Misc
 public export
 data Term : (_ : Index) -> Type where
   TType   : Term n                               -- Type of types
+
+  TTop    : Term n                               -- Unit type
+  TStar   : Term n                               -- Unit term
+  TTopInd : Term n -> Term n -> Term n           -- : (x : ⊤) → C x
+
+  TBot    : Term n                               -- Empty type
+  TBotInd : Term n -> Term n                     -- : (x : ⊥) → C x
+
+  TNat    : Term n                               -- ℕ
+  TZero   : Term n                               -- 0
+  TSuc    : Term n -> Term n                     -- successor
+  TNatInd : Term n -> Term n -> Term n -> Term n -- : (x : ℕ) → C x
+
   TLam    : Term (S n) -> Term n                 -- Lambda abstraction (λ _ . Scope)
   TPi     : Term n -> Term (S n) -> Term n       -- Pi type            (∏ _ : A . B _ )
+
   TApp    : Term n -> Term n -> Term n           -- Appliction
-  TVar    : (n : Nat) -> LT n m -> Term m -- Variable
+  TVar    : Fin n  -> Term n                      -- Variable
+
+infixl 2 `TApp`
 
 public export
 Show (Term n) where
   show TType           = "TType"
+
+  show TTop            = "⊤"
+  show TStar           = "★"
+  show (TTopInd c st)  = "⊤-ind (" ++ show c ++ ") (" ++ show st ++ ")"
+
+  show TBot            = "⊥"
+  show (TBotInd c)     = "⊥-ind (" ++ show c ++ ")"
+
+  show TNat            = "ℕ"
+  show TZero           = "0"
+  show (TSuc n)        = "suc (" ++ show n ++ ")"
+  show (TNatInd c z s) = "ℕ-ind (" ++ show c ++ ") (" ++ show z ++ ") (" ++ show s ++ ")"
+
   show (TLam sc)       = "TLam (" ++ show sc ++ ")"
   show (TPi  ty sc)    = "TPi (" ++ show ty ++ ") (" ++ show sc ++ ")"
+
   show (TApp f x)      = "TApp (" ++ show f ++ ") (" ++ show x ++ ")"
-  show (TVar i _) = "TVar " ++ show i
+  show (TVar i)        = "TVar " ++ show i
+
+public export
+weakTr : Term n -> Term (S n)
+weakTr = go 0
+  where
+    go : {0 n : Nat} -> Fin (S n) -> Term n -> Term (S n)
+    go n TType           = TType
+    go n TTop            = TTop
+    go n TStar           = TTop
+    go n (TTopInd c st)  = TTopInd (go n c) (go n st)
+    go n TBot            = TBot
+    go n (TBotInd c)     = TBotInd (go n c)
+    go n TNat            = TNat
+    go n TZero           = TZero
+    go n (TSuc m)        = TSuc (go n m)
+    go n (TNatInd c z s) = TNatInd (go n c) (go n z) (go n s)
+    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)
+    go n (TVar i)        = if weaken i < n
+                              then TVar (weaken i)
+                              else TVar (FS i)
+
+public export
+weakTr2 : Term n -> Term (2+n)
+weakTr2 = weakTr . weakTr
+
+public export
+weakTr3 : Term n -> Term (3+n)
+weakTr3 = weakTr . weakTr2
+
+public export
+weakTr4 : Term n -> Term (4+n)
+weakTr4 = weakTr2 . weakTr2

src/Tests.idr

@@ -11,25 +11,22 @@ import Control.Monad.RWS
 import Control.Monad.Identity
 import Control.Monad.Either
 
-import Data.Nat
+import Data.Fin
 
 %default total
 
-a : {p, q : Nat} -> lt p q = True -> LT p q
-a {p} {q} eq = ltReflectsLT p q eq
-
 {- λA. λx. x : ∏ (A : Type) → A → A -}
 test_id : Either String (Bool, List String)
-test_id = typecheck (TLam (TLam (TVar 0 (a Refl))))
+test_id = typecheck (TLam (TLam (TVar 0)))
-                    (TPi TType (TPi (TVar 0 (a Refl)) (TVar 1 (a Refl))))
+                    (TPi TType (TPi (TVar 0) (TVar 1)))
 
 {- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -}
 test_app : Either String (Bool, List String)
-test_app = typecheck (TLam (TLam (TLam (TLam (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))))))
+test_app = typecheck (TLam (TLam (TLam (TLam (TApp (TVar 1) (TVar 0))))))
                      (TPi TType 
-                          (TPi (TPi (TVar 0 (a Refl)) TType)
+                          (TPi (TPi (TVar 0) TType)
-                               (TPi (TPi (TVar 1 (a Refl)) (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))) 
+                               (TPi (TPi (TVar 1) (TApp (TVar 1) (TVar 0))) 
-                                    (TPi (TVar 2 (a Refl)) (TApp (TVar 2 (a Refl)) (TVar 0 (a Refl)))))))
+                                    (TPi (TVar 2) (TApp (TVar 2) (TVar 0))))))
 
 {- λf. λx. f x ≃ λf. λx. (λy. f y) x -}
 eta_test : Either String (Bool, List String)
@@ -37,6 +34,49 @@ eta_test = resolve action
   where
     action : PI Bool
     action = do
-      x <- eval ctx0 (TLam (TLam (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))))
+      x <- eval ctx0 (TLam (TLam (TApp (TVar 1) (TVar 0))))
-      y <- eval ctx0 (TLam (TLam (TApp (TLam (TApp (TVar 2 (a Refl)) (TVar 0 (a Refl)))) (TVar 0 (a Refl)))))
+      y <- eval ctx0 (TLam (TLam (TApp (TLam (TApp (TVar 2) (TVar 0))) (TVar 0))))
       convert x y
+
+addition : Term 0
+addition = TNatInd (TLam (TPi TNat TNat)) 
+                   (TLam (TVar 0)) 
+                   (TLam {-n-} (TLam {-n+-} (TLam {-m-} (TSuc (TApp (TVar 1) (TVar 0))))))
+
+addition_type : Either String (Bool, List String)
+addition_type = typecheck addition (TPi TNat (TPi TNat TNat))
+
+{- 2 + 1 = 3 -}
+add_test : Either String (Bool, List String)
+add_test = resolve action
+  where
+    action : PI Bool
+    action = do
+      x <- eval ctx0 (addition `TApp` TSuc (TSuc TZero) `TApp` TSuc TZero)
+      y <- eval ctx0 (TSuc (TSuc (TSuc TZero)))
+      convert x y
+
+multi : Term 0
+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)
+multi_type = typecheck multi (TPi TNat (TPi TNat TNat))
+
+{- 2 * 3 = 6 -}
+multi_test : Either String (Bool, List String)
+multi_test = resolve action
+  where
+    action : PI Bool
+    action = do
+      x <- eval ctx0 (multi `TApp` TSuc (TSuc TZero) `TApp` TSuc (TSuc (TSuc TZero)))
+      y <- eval ctx0 (TSuc (TSuc (TSuc (TSuc (TSuc (TSuc TZero))))))
+      convert x y
+
+-- no, not that kind
+unit_test : Either String (Bool, List String)
+unit_test = typecheck TStar TTop
+
+absurd_test : Either String (Bool, List String)
+absurd_test = typecheck (TLam (TBotInd (TLam (TVar 1)))) (TPi TType (TPi TBot (TVar 1)))

src/Value.idr

@@ -11,6 +11,15 @@ mutual
   public export
   data Value : Type where
     VType  : Value
+
+    VTop   : Value
+    VStar  : Value
+
+    VBot   : Value
+
+    VNat   : Value
+    VNatTr : Nat -> Value
+
     VGen   : Nat   -> Value
     VApp   : Value -> Value  -> Value
     VClos  : Ctx n -> Term n -> Value
@@ -26,6 +35,11 @@ ctx0 = []
 public export
 Show Value where
   show VType       = "VType"
+  show VTop        = "VTop"
+  show VStar       = "VStar"
+  show VBot        = "VBot"
+  show VNat        = "VNat"
+  show (VNatTr n)  = "V" ++ show n
   show (VGen i)    = "VGen " ++ show i
   show (VApp f x)  = "VApp (" ++ show f ++ ") (" ++ show x ++ ")"
   show (VClos e t) = "VClos (" ++ assert_total (show e) ++ ") (" ++ show t ++ ")"