added Σ types

README.md

@@ -19,7 +19,6 @@ A dependently typed system
 # TODO
 
 * Fun types
-  * Σ
   * Id
 
 * Parser

src/Check.idr

@@ -28,15 +28,27 @@ mutual
                            check (v :: trs) (VClos env a :: tys) (VClos (v :: env) b) sc
                          _ => oops "expected pi"
 
+      -- pi and sigma could be inferred /shrug
       TPi a b    => case xpt of
                          VType => do
                            v <- VGen <$> fresh
-                        (&&) <$> check trs tys VType a 
+                           guardS "Pi a" =<< check trs tys VType a 
-                             <*> delay <$> check (v :: trs) (VClos trs a :: tys) VType b
+                           check (v :: trs) (VClos trs a :: tys) VType b
-
-
                          _ => oops "expected type"
 
+      TSigma a b => case xpt of
+                         VType => do
+                           v <- VGen <$> fresh
+                           guardS "Σ a" =<< check trs tys VType a 
+                           check trs tys (VClos trs (TPi a TType)) b
+                         _ => oops "expected type"
+
+      TPair  x y => case xpt of
+                         (VClos env (TSigma a b)) => do
+                           guardS "Pair a" =<< check trs tys (VClos env a) x
+                           check trs tys (VClos env b `VApp` VClos trs x) y
+                         _ => oops "expected sigma"
+
       _       => convert xpt =<< infer trs tys tr
 
   -- terms types term
@@ -46,7 +58,7 @@ mutual
   infer trs tys (TApp f x) = infer trs tys f >>= whnf >>=
                               \case
                                  VClos env (TPi a b) => do
-                                   guard =<< check trs tys (VClos env a) x
+                                   guardS "app x" =<< check trs tys (VClos env a) x
                                    pure (VClos (VClos trs x :: env) b)
 
                                  _ => oops "expected infer pi"
@@ -57,27 +69,37 @@ mutual
   infer trs tys TStar     = pure VTop
   infer trs tys TZero     = pure VNat
   infer trs tys (TSuc n)  = do 
-    guard =<< check trs tys VNat n
+    guardS "suc n" =<< check trs tys VNat n
     pure VNat
 
   infer trs tys (TTopInd c st) = do
-    guard =<< check trs tys (VClos trs (TPi TTop TType)) c
+    guardS "⊤ C" =<< check trs tys (VClos trs (TPi TTop TType)) c
-    guard =<< check trs tys (VApp (VClos trs c) VStar)   st
+    guardS "⊤ ★" =<< 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
+    guardS "⊥ C" =<< 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
+    guardS "ℕ C" =<< check trs tys (VClos trs (TPi TNat TType)) c
-    guard =<< check trs tys (VApp (VClos trs c) (VNatTr 0)) z
+    guardS "ℕ z" =<< check trs tys (VApp (VClos trs c) (VNatTr 0)) z
-    guard =<< check trs tys (VClos trs (TPi TNat 
+    guardS "ℕ s" =<< 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"
+  infer trs tys (TSigInd a b c f) = do
+    guardS "Σ A" =<< check trs tys VType a
+    guardS "Σ B" =<< check trs tys (VClos trs (TPi a TType)) b
+    guardS "Σ C" =<< check trs tys (VClos trs (TPi (TSigma a b) TType)) c
+    guardS "Σ f" =<< check trs tys (VClos trs (TPi a {-a:A-}
+                                              (TPi (weakTr b `TApp` TVar 0) {-b:Ba-}
+                                                   (weakTr2 c `TApp` TPair (TVar (FS FZ)) (TVar 0))))) f
+    pure (VClos trs (TPi (TSigma a b) (weakTr c `TApp` TVar 0)))
+                                      
+
+  infer trs tys x          = oops ("cannot infer type" ++ show x)
 
 public export
 typecheck : Term 0 -> Term 0 -> Either String (Bool, List String)

src/Convert.idr

@@ -14,6 +14,8 @@ 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
@@ -31,28 +33,28 @@ convert u1 u2 = do
 
       (VNatTr n, VNatTr m) => pure (n == m)
 
-      (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 
+      (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2
-                                       <*> delay <$> convert x1 x2
+
       (VGen k1, VGen k2) => pure (k1 == k2)
 
+      (VPair a1 b1, VPair a2 b2) => (&&) <$> convert a1 a2 <*> delay <$> convert b1 b2
+
       (VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do
         v <- VGen <$> fresh
-        convert (VClos (v :: env1) sc1)
+        convert (VClos (v :: env1) sc1) (VClos (v :: env2) sc2)
-                (VClos (v :: env2) sc2)
 
       (VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do
         v <- VGen <$> fresh
-        (&&) <$> convert (VClos env1 a1)
+        guard =<< convert (VClos env1 a1) (VClos env2 a2)
-                         (VClos env2 a2)
+        convert (VClos (v :: env1) b1) (VClos (v :: env2) b2)
-             <*> 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
+        guard =<< convert c1' c2'
         st1' <- eval env1 st1
         st2' <- eval env2 st2
-        (&&) <$> convert c1' c2' <*> delay <$> convert st1' st2'
+        convert st1' st2'
 
       (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => do
         c1' <- eval env1 c1
@@ -63,12 +65,34 @@ convert u1 u2 = do
       (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do
         c1' <- eval env1 c1
         c2' <- eval env2 c2
+        guard =<< convert c1' c2'
         z1' <- eval env1 z1
         z2' <- eval env2 z2
+        guard =<< convert z1' z2'
         s1' <- eval env1 s1
         s2' <- eval env2 s2
-        b1  <- (&&) <$> convert c1' c2' <*> delay <$> convert z1' z2'
-        guard b1 
         convert s1' s2'
 
+      (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do
+        a1' <- eval env1 a1
+        a2' <- eval env2 a2
+        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
+        a2' <- eval env2 a2
+        guard =<< convert a1' a2'
+        b1' <- eval env1 b1
+        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

src/Misc.idr

@@ -30,6 +30,12 @@ public export
 oops : String -> PI a
 oops = left
 
+public export
+guardS : String -> Bool -> PI ()
+guardS str True  = pure ()
+guardS str False = oops str
+
+
 public export
 fresh : PI Nat
 fresh = do

src/Normalize.idr

@@ -38,6 +38,14 @@ mutual
   app f@(VClos env (TNatInd _ z s)) x = logS ("ℕ-ind applied to " ++ show x)
                                         >> pure (VApp f x)
 
+  app (VClos env (TSigInd _ _ c f)) (VPair a b) = do
+    f' <- eval env f
+    fa <- app f' a
+    app fa b
+
+  app f@(VClos env (TSigInd _ _ c p)) x = logS ("Σ-ind applied to " ++ show x)
+                                          >> pure (VApp f x)
+
   app f x = pure (VApp f x)
 
   public export
@@ -61,6 +69,11 @@ mutual
          x        => logS ("suc applied to " ++ show x)
                      >> pure (VClos env (TSuc n))
 
+  eval env (TPair a b) = do
+    a' <- eval env a
+    b' <- eval env b
+    pure (VPair a' b')
+
   eval env tr          = pure (VClos env tr)
 
 public export

src/Term.idr

@@ -26,13 +26,17 @@ data Term : (_ : Index) -> Type where
   TSuc    : Term n -> Term n                     -- successor
   TNatInd : Term n -> Term n -> Term n -> Term n -- : (x : ℕ) → C x
 
+  TSigma  : Term n -> Term n -> Term n                     -- Sum type (Σ _ : A, B _)
+  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
+
   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    : Fin n  -> Term n                     -- Variable
 
-infixl 2 `TApp`
+infixl 3 `TApp`
 
 public export
 Show (Term n) where
@@ -50,6 +54,10 @@ 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 (TPair a b)     = "TPair (" ++ show a ++ ") (" ++ show b ++ ")"
+  show (TSigInd a b c f) = "Σ-ind (" ++ show a ++ ") (" ++ show b ++ ") (" ++ show c ++ ") (" ++ show f ++ ")"
+
   show (TLam sc)       = "TLam (" ++ show sc ++ ")"
   show (TPi  ty sc)    = "TPi (" ++ show ty ++ ") (" ++ show sc ++ ")"
 
@@ -71,6 +79,9 @@ weakTr = go 0
     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 (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 (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

@@ -22,11 +22,11 @@ test_id = typecheck (TLam (TLam (TVar 0)))
 
 {- λ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) (TVar 0))))))
+test_app = typecheck (TLam (TLam (TLam (TLam (TVar 1 `TApp` TVar 0)))))
                      (TPi TType 
                           (TPi (TPi (TVar 0) TType)
-                               (TPi (TPi (TVar 1) (TApp (TVar 1) (TVar 0))) 
+                               (TPi (TPi (TVar 1) (TVar 1 `TApp` TVar 0)) 
-                                    (TPi (TVar 2) (TApp (TVar 2) (TVar 0))))))
+                                    (TPi (TVar 2) (TVar 2 `TApp` TVar 0)))))
 
 {- λf. λx. f x ≃ λf. λx. (λy. f y) x -}
 eta_test : Either String (Bool, List String)
@@ -34,14 +34,14 @@ eta_test = resolve action
   where
     action : PI Bool
     action = do
-      x <- eval ctx0 (TLam (TLam (TApp (TVar 1) (TVar 0))))
+      x <- eval ctx0 (TLam (TLam (TVar 1 `TApp` TVar 0)))
-      y <- eval ctx0 (TLam (TLam (TApp (TLam (TApp (TVar 2) (TVar 0))) (TVar 0))))
+      y <- eval ctx0 (TLam (TLam (TLam (TVar 2 `TApp` TVar 0) `TApp` 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))))))
+                   (TLam {-n-} (TLam {-n+-} (TLam {-m-} (TSuc (TVar 1 `TApp` TVar 0)))))
 
 addition_type : Either String (Bool, List String)
 addition_type = typecheck addition (TPi TNat (TPi TNat TNat))
@@ -80,3 +80,38 @@ 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)))
+
+pr1ty : Term 0
+pr1ty = TPi TType {- A : Type -}
+            (TPi (TPi (TVar 0) TType) {- B : A → Type -}
+                 (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
+                      (TVar 2)))
+
+pr1 : Term 0
+pr1 = TLam {- A : Type -} 
+           (TLam {- B : A → Type -}
+                 (TSigInd (TVar 1) (TVar 0) (TLam {-ΣAB-} (TVar 2)) (TLam (TLam (TVar 1)))))
+
+pr1_test : Either String (Bool, List String)
+pr1_test = typecheck pr1 pr1ty
+
+pr2ty : Term 0
+pr2ty = TPi TType {- A : Type -}
+            (TPi (TPi (TVar 0) TType) {- B : A → Type -}
+                 (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
+                      (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0))))
+
+pr2 : Term 0
+pr2 = TLam {- A : Type -} 
+           (TLam {- B : A → Type -}
+                 (TSigInd (TVar 1)
+                          (TVar 0)
+                          (TLam {-ΣAB-}
+                                (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0)))
+                          (TLam (TLam (TVar 0)))))
+
+pr2ty_test : Either String (Bool, List String)
+pr2ty_test = typecheck pr2ty TType
+
+pr2_test : Either String (Bool, List String)
+pr2_test = typecheck pr2 pr2ty

src/Value.idr

@@ -20,10 +20,14 @@ mutual
     VNat   : Value
     VNatTr : Nat -> Value
 
+    VPair  : Value -> Value -> Value
+
     VGen   : Nat   -> Value
     VApp   : Value -> Value  -> Value
     VClos  : Ctx n -> Term n -> Value
 
+  infixl 2 `VApp`
+
   public export
   Ctx : Index -> Type
   Ctx i = Vect i Value
@@ -39,6 +43,7 @@ Show Value where
   show VStar       = "VStar"
   show VBot        = "VBot"
   show VNat        = "VNat"
+  show (VPair a b) = "VPair (" ++ show a ++ ") (" ++ show b ++ ")"
   show (VNatTr n)  = "V" ++ show n
   show (VGen i)    = "VGen " ++ show i
   show (VApp f x)  = "VApp (" ++ show f ++ ") (" ++ show x ++ ")"