working on adding full sigma types

This reverts commit 2c1f193d77.

examples/logic.pg

@@ -35,20 +35,17 @@ def double_neg_intro (A : ★) (a : A) : not (not A) :=
 
 -- Conjunction
 
-def ∧ (A B : ★) : ★ := forall (C : ★), (A → B → C) → C;
+def ∧ (A B : ★) : ★ := {A × B};
 infixl 10 ∧;
 
 -- introduction rule
-def and_intro (A B : ★) (a : A) (b : B) : A ∧ B :=
+def and_intro (A B : ★) (a : A) (b : B) : A ∧ B := <a, b>;
-    fun (C : ★) (H : A → B → C) => H a b;
 
 -- left elimination rule
-def and_elim_l (A B : ★) (ab : A ∧ B) : A :=
+def and_elim_l (A B : ★) (ab : A ∧ B) : A := π₁ ab;
-    ab A (fun (a : A) (b : B) => a);
 
 -- right elimination rule
-def and_elim_r (A B : ★) (ab : A ∧ B) : B :=
+def and_elim_r (A B : ★) (ab : A ∧ B) : B := π₂ ab;
-    ab B (fun (a : A) (b : B) => b);
 
 -- --------------------------------------------------------------------------------------------------------------
 
@@ -149,31 +146,25 @@ section Theorems
 
     -- ~(A ∨ B) => ~A ∧ ~B
     def de_morgan1 (h : not (A ∨ B)) : not A ∧ not B :=
-        and_intro (not A) (not B)
+        <[a : A] h (or_intro_l A B a)
-            ([a : A] h (or_intro_l A B a))
+        ,[b : B] h (or_intro_r A B b)>;
-            ([b : B] h (or_intro_r A B b));
 
     -- ~A ∧ ~B => ~(A ∨ B)
     def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) :=
         fun (contra : A ∨ B) => 
-            or_elim A B false contra
+            or_elim A B false contra (π₁ h) (π₂ h);
-                (and_elim_l (not A) (not B) h)
-                (and_elim_r (not A) (not B) h);
 
     -- ~A ∨ ~B => ~(A ∧ B)
     def de_morgan3 (h : not A ∨ not B) : not (A ∧ B) :=
         fun (contra : A ∧ B) =>
             or_elim (not A) (not B) false h
-                (fun (na : not A) => na (and_elim_l A B contra))
+                (fun (na : not A) => na (π₁ contra))
-                (fun (nb : not B) => nb (and_elim_r A B contra));
+                (fun (nb : not B) => nb (π₂ contra));
 
     -- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
 
     -- A ∧ B => B ∧ A
-    def and_comm (h : A ∧ B) : B ∧ A :=
+    def and_comm (h : A ∧ B) : B ∧ A := <π₂ h, π₁ h>;
-        and_intro B A
-            (and_elim_r A B h)
-            (and_elim_l A B h);
 
     -- A ∨ B => B ∨ A
     def or_comm (h : A ∨ B) : B ∨ A :=
@@ -183,23 +174,11 @@ section Theorems
 
     -- A ∧ (B ∧ C) => (A ∧ B) ∧ C
     def and_assoc_l (h : A ∧ (B ∧ C)) : (A ∧ B) ∧ C :=
-        let (a := (and_elim_l A (B ∧ C) h))
+        <<π₁ h, π₁ (π₂ h)>, π₂ (π₂ h)>;
-            (bc := (and_elim_r A (B ∧ C) h))
-            (b := (and_elim_l B C bc))
-            (c := (and_elim_r B C bc))
-        in
-            and_intro (A ∧ B) C (and_intro A B a b) c
-        end;
 
     -- (A ∧ B) ∧ C => A ∧ (B ∧ C)
     def and_assoc_r (h : (A ∧ B) ∧ C) : A ∧ (B ∧ C) :=
-        let (ab := and_elim_l (A ∧ B) C h)
+        <π₁ (π₁ h), <π₂ (π₁ h), π₂ h>>;
-            (a := and_elim_l A B ab)
-            (b := and_elim_r A B ab)
-            (c := and_elim_r (A ∧ B) C h)
-        in
-            and_intro A (B ∧ C) a (and_intro B C b c)
-        end;
 
     -- A ∨ (B ∨ C) => (A ∨ B) ∨ C
     def or_assoc_l (h : A ∨ (B ∨ C)) : (A ∨ B) ∨ C :=
@@ -221,21 +200,15 @@ section Theorems
 
     -- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
     def and_distrib_l_or (h : A ∧ (B ∨ C)) : A ∧ B ∨ A ∧ C :=
-        or_elim B C (A ∧ B ∨ A ∧ C) (and_elim_r A (B ∨ C) h)
+        or_elim B C (A ∧ B ∨ A ∧ C) (π₂ h)
-            (fun (b : B) => or_intro_l (A ∧ B) (A ∧ C)
+            (fun (b : B) => or_intro_l (A ∧ B) (A ∧ C) <π₁ h, b>)
-                (and_intro A B (and_elim_l A (B ∨ C) h) b))
+            (fun (c : C) => or_intro_r (A ∧ B) (A ∧ C) <π₁ h, c>);
-            (fun (c : C) => or_intro_r (A ∧ B) (A ∧ C)
-                (and_intro A C (and_elim_l A (B ∨ C) h) c));
 
     -- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
     def and_factor_l_or (h : A ∧ B ∨ A ∧ C) : A ∧ (B ∨ C) :=
         or_elim (A ∧ B) (A ∧ C) (A ∧ (B ∨ C)) h
-            (fun (ab : A ∧ B) => and_intro A (B ∨ C)
+            (fun (ab : A ∧ B) => <π₁ ab, or_intro_l B C (π₂ ab)>)
-                (and_elim_l A B ab)
+            (fun (ac : A ∧ C) => <π₁ ac, or_intro_r B C (π₂ ac)>);
-                (or_intro_l B C (and_elim_r A B ab)))
-            (fun (ac : A ∧ C) => and_intro A (B ∨ C)
-                (and_elim_l A C ac)
-                (or_intro_r B C (and_elim_r A C ac)));
 
     -- Thanks Quinn!
     -- A ∨ B => ~B => A

lib/Check.hs

@@ -16,6 +16,12 @@ matchPi x mt =
         (Pi _ a b) -> pure (a, b)
         t -> throwError $ ExpectedPiType x t
 
+matchSigma :: Expr -> Expr -> ReaderT Env Result (Expr, Expr)
+matchSigma x mt =
+    whnf mt >>= \case
+        (Sigma _ a b) -> pure (a, b)
+        t -> throwError $ ExpectedSigmaType x t
+
 findLevel :: Context -> Expr -> ReaderT Env Result Integer
 findLevel g a = do
     s <- findType g a
@@ -72,6 +78,17 @@ findType g e@(Let _ (Just t) v b) = do
     _ <- findType g t
     betaEquiv' e t res
     pure t
+findType g (Sigma _ a b) = do
+    aSort <- findType g a
+    bSort <- findType g b
+    liftEither $ compSort a b aSort bSort
+findType g (Pair a b) = do
+    aType <- findType g a
+    bType <- findType g b
+    validateType g $ Sigma "" aType bType
+    pure $ Sigma aType bType
+findType g (Pi1 x) = fst <$> (findType g x >>= matchSigma x)
+findType g (Pi2 x) = snd <$> (findType g x >>= matchSigma x)
 
 checkType :: Env -> Expr -> Result Expr
 checkType env t = runReaderT (findType [] t) env

lib/Elaborator.hs

@@ -116,6 +116,10 @@ usedVars (I.Let name ascr value body) = saveState $ do
     ascr' <- traverse usedVars ascr
     removeName name
     S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
+usedVars (I.Sigma m n) = S.union <$> usedVars m <*> usedVars n
+usedVars (I.Pair m n) = S.union <$> usedVars m <*> usedVars n
+usedVars (I.Pi1 x) = usedVars x
+usedVars (I.Pi2 x) = usedVars x
 
 -- traverse the body of a definition, adding the necessary section arguments to
 -- any definitions made within the section
@@ -142,6 +146,10 @@ traverseBody (I.Let name ascr value body) = saveState $ do
     value' <- traverseBody value
     removeName name
     I.Let name ascr' value' <$> traverseBody body
+traverseBody (I.Sigma m n) = I.Sigma <$> traverseBody m <*> traverseBody n
+traverseBody (I.Pair m n) = I.Pair <$> traverseBody m <*> traverseBody n
+traverseBody (I.Pi1 x) = I.Pi1 <$> traverseBody x
+traverseBody (I.Pi2 x) = I.Pi2 <$> traverseBody x
 
 mkPi :: (Text, IRExpr) -> IRExpr -> IRExpr
 mkPi (param, typ) = I.Pi param typ
@@ -206,3 +214,7 @@ elaborate ir = evalState (elaborate' ir) []
         ty' <- elaborate' ty
         modify (name :)
         E.Let name (Just ty') val' <$> elaborate' body
+    elaborate' (I.Sigma m n) = E.Sigma <$> elaborate' m <*> elaborate' n
+    elaborate' (I.Pair m n) = E.Pair <$> elaborate' m <*> elaborate' n
+    elaborate' (I.Pi1 x) = E.Pi1 <$> elaborate' x
+    elaborate' (I.Pi2 x) = E.Pi2 <$> elaborate' x

lib/Errors.hs

@@ -9,6 +9,7 @@ data Error
     = UnboundVariable Text
     | NotASort Expr
     | ExpectedPiType Expr Expr
+    | ExpectedSigmaType Expr Expr
     | NotEquivalent Expr Expr Expr
     | PNMissingType Text
     | DuplicateDefinition Text
@@ -18,6 +19,7 @@ instance Pretty Error where
     pretty (UnboundVariable x) = "Unbound variable: '" <> pretty x <> "'"
     pretty (NotASort x) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> "is not a type"
     pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a function, instead is type" <> line <> pretty t)
+    pretty (ExpectedSigmaType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a pair, instead is type" <> line <> pretty t)
     pretty (NotEquivalent a a' e) =
         group $
             hang 4 ("Cannot unify" <> line <> pretty a)

lib/Eval.hs

@@ -45,6 +45,10 @@ subst k s (App m n) = App (subst k s m) (subst k s n)
 subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Let x t v b) = Let x t (subst k s v) (subst (k + 1) (incIndices s) b)
+subst k s (Sigma x m n) = Sigma x (subst k s m) (subst (k + 1) (incIndices s) n)
+subst k s (Pair m n) = Pair (subst k s m) (subst k s n)
+subst k s (Pi1 x) = Pi1 (subst k s x)
+subst k s (Pi2 x) = Pi2 (subst k s x)
 
 envLookupVal :: Text -> ReaderT Env Result Expr
 envLookupVal n = asks ((_val <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
@@ -59,6 +63,12 @@ reduce (Abs x t v) = Abs x <$> reduce t <*> reduce v
 reduce (Pi x t v) = Pi x <$> reduce t <*> reduce v
 reduce (Free n) = envLookupVal n
 reduce (Let _ _ v b) = pure $ subst 0 v b
+reduce (Sigma x a b) = Sigma x <$> reduce a <*> reduce b
+reduce (Pair a b) = Pair <$> reduce a <*> reduce b
+reduce (Pi1 (Pair a _)) = pure a
+reduce (Pi2 (Pair _ b)) = pure b
+reduce (Pi1 x) = Pi1 <$> reduce x
+reduce (Pi2 x) = Pi2 <$> reduce x
 reduce e = pure e
 
 normalize :: Expr -> ReaderT Env Result Expr
@@ -78,6 +88,18 @@ whnf (App m n) = do
         else whnf $ App m' n
 whnf (Free n) = envLookupVal n >>= whnf
 whnf (Let _ _ v b) = whnf $ subst 0 v b
+whnf (Pi1 (Pair a _)) = pure a
+whnf (Pi2 (Pair _ b)) = pure b
+whnf (Pi1 x) = do
+    x' <- whnf x
+    if x == x'
+        then pure $ Pi1 x
+        else whnf $ Pi1 x'
+whnf (Pi2 x) = do
+    x' <- whnf x
+    if x == x'
+        then pure $ Pi2 x
+        else whnf $ Pi2 x'
 whnf e = pure e
 
 betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
@@ -99,6 +121,10 @@ betaEquiv e1 e2
             (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
             (Let _ _ v b, e) -> betaEquiv (subst 0 v b) e
             (e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
+            (Sigma _ a b, Sigma _ a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b'
+            (Pair a b, Pair a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b'
+            (Pi1 x, Pi1 x') -> betaEquiv x x'
+            (Pi2 x, Pi2 x') -> betaEquiv x x'
             _ -> pure False -- remaining cases impossible, false, or redundant
 
 betaEquiv' :: Expr -> Expr -> Expr -> ReaderT Env Result ()

lib/Expr.hs

@@ -15,6 +15,10 @@ data Expr where
     Abs :: Text -> Expr -> Expr -> Expr
     Pi :: Text -> Expr -> Expr -> Expr
     Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr
+    Sigma :: Text -> Expr -> Expr -> Expr
+    Pair :: Expr -> Expr -> Expr
+    Pi1 :: Expr -> Expr
+    Pi2 :: Expr -> Expr
     deriving (Show, Ord)
 
 instance Pretty Expr where
@@ -30,6 +34,10 @@ instance Eq Expr where
     (Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2
     (Pi _ t1 b1) == (Pi _ t2 b2) = t1 == t2 && b1 == b2
     (Let _ _ v1 b1) == (Let _ _ v2 b2) = v1 == v2 && b1 == b2
+    (Sigma _ x1 y1) == (Sigma _ x2 y2) = x1 == x2 && y1 == y2
+    (Pair x1 y1) == (Pair x2 y2) = x1 == x2 && y1 == y2
+    (Pi1 x) == (Pi1 y) = x == y
+    (Pi2 x) == (Pi2 y) = x == y
     _ == _ = False
 
 occursFree :: Integer -> Expr -> Bool
@@ -42,6 +50,10 @@ occursFree n (App a b) = on (||) (occursFree n) a b
 occursFree n (Abs _ a b) = occursFree n a || occursFree (n + 1) b
 occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b
 occursFree n (Let _ _ v b) = occursFree n v || occursFree (n + 1) b
+occursFree n (Sigma _ x y) = occursFree n x || occursFree n y
+occursFree n (Pair x y) = occursFree n x || occursFree n y
+occursFree n (Pi1 x) = occursFree n x
+occursFree n (Pi2 x) = occursFree n x
 
 shiftIndices :: Integer -> Integer -> Expr -> Expr
 shiftIndices d c (Var x k)
@@ -55,6 +67,10 @@ shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
 shiftIndices d c (Abs x m n) = Abs x (shiftIndices d c m) (shiftIndices d (c + 1) n)
 shiftIndices d c (Pi x m n) = Pi x (shiftIndices d c m) (shiftIndices d (c + 1) n)
 shiftIndices d c (Let x t v b) = Let x t (shiftIndices d c v) (shiftIndices d (c + 1) b)
+shiftIndices d c (Sigma x m n) = Sigma x (shiftIndices d c m) (shiftIndices d c n)
+shiftIndices d c (Pair m n) = Pair (shiftIndices d c m) (shiftIndices d c n)
+shiftIndices d c (Pi1 x) = Pi1 (shiftIndices d c x)
+shiftIndices d c (Pi2 x) = Pi2 (shiftIndices d c x)
 
 incIndices :: Expr -> Expr
 incIndices = shiftIndices 1 0
@@ -206,6 +222,11 @@ prettyExpr k expr = case expr of
       where
         (binds, body) = collectLets expr
         bindings = sep $ map pretty binds
+    (Sigma "" x y) -> parens $ parens (pretty x) <+> "×" <+> parens (pretty y)
+    (Sigma x t m) -> parens $ "Σ" <+> pretty x <+> ":" <+> pretty t <> "," <+> pretty m
+    (Pair x y) -> parens $ pretty x <> "," <+> pretty y
+    (Pi1 x) -> parens $ "π₁" <+> parens (pretty x)
+    (Pi2 x) -> parens $ "π₂" <+> parens (pretty x)
 
 prettyT :: Expr -> Text
 prettyT = renderStrict . layoutSmart defaultLayoutOptions . pretty

lib/IR.hs

@@ -27,6 +27,16 @@ data IRExpr
         , letValue :: IRExpr
         , letBody :: IRExpr
         }
+    | Sigma
+        { prodLeft :: IRExpr
+        , prodRight :: IRExpr
+        }
+    | Pair
+        { pairLeft :: IRExpr
+        , pairRight :: IRExpr
+        }
+    | Pi1 IRExpr
+    | Pi2 IRExpr
     deriving (Show, Eq, Ord)
 
 data IRSectionDef

lib/Parser.hs

@@ -174,8 +174,26 @@ pSort = lexeme $ pStar <|> pSquare
 pOpSection :: Parser IRExpr
 pOpSection = lexeme $ parens $ Var <$> pSymbol
 
+pSigma :: Parser IRExpr
+pSigma = lexeme $ between (char '{') (char '}') $ do
+    left <- pIRExpr
+    _ <- symbol "×"
+    Sigma left <$> pIRExpr
+
+pPair :: Parser IRExpr
+pPair = lexeme $ between (char '<') (char '>') $ do
+    left <- pIRExpr
+    _ <- symbol ","
+    Pair left <$> pIRExpr
+
+pPi1 :: Parser IRExpr
+pPi1 = lexeme $ symbol "π₁" >> Pi1 <$> pIRExpr
+
+pPi2 :: Parser IRExpr
+pPi2 = lexeme $ symbol "π₂" >> Pi2 <$> pIRExpr
+
 pTerm :: Parser IRExpr
-pTerm = lexeme $ label "term" $ choice [pSort, pPureVar, pVar, try pOpSection, parens pIRExpr]
+pTerm = lexeme $ label "term" $ choice [pSort, pPi1, pPi2, pPureVar, pVar, pSigma, pPair, try pOpSection, parens pIRExpr]
 
 pInfix :: Parser IRExpr
 pInfix = parseWithPrec 0