From 2c1f193d777c474acc2c261ce53db84c528464b2 Mon Sep 17 00:00:00 2001 From: William Ball Date: Fri, 24 Jan 2025 00:57:13 -0800 Subject: [PATCH] starting progress on (non-dependent) products --- examples/logic.pg | 61 +++++++++++++---------------------------------- lib/Check.hs | 17 +++++++++++++ lib/Elaborator.hs | 12 ++++++++++ lib/Errors.hs | 2 ++ lib/Eval.hs | 26 ++++++++++++++++++++ lib/Expr.hs | 20 ++++++++++++++++ lib/IR.hs | 10 ++++++++ lib/Parser.hs | 20 +++++++++++++++- 8 files changed, 123 insertions(+), 45 deletions(-) diff --git a/examples/logic.pg b/examples/logic.pg index d28ee0c..c1da0c2 100644 --- a/examples/logic.pg +++ b/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 := - fun (C : ★) (H : A → B → C) => H a b; +def and_intro (A B : ★) (a : A) (b : B) : A ∧ B := ; -- left elimination rule -def and_elim_l (A B : ★) (ab : A ∧ B) : A := - ab A (fun (a : A) (b : B) => a); +def and_elim_l (A B : ★) (ab : A ∧ B) : A := π₁ ab; -- right elimination rule -def and_elim_r (A B : ★) (ab : A ∧ B) : B := - ab B (fun (a : A) (b : B) => b); +def and_elim_r (A B : ★) (ab : A ∧ B) : B := π₂ ab; -- -------------------------------------------------------------------------------------------------------------- @@ -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)) - ([b : B] h (or_intro_r A B b)); + <[a : A] h (or_intro_l A B a) + ,[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 - (and_elim_l (not A) (not B) h) - (and_elim_r (not A) (not B) h); + or_elim A B false contra (π₁ h) (π₂ 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 (nb : not B) => nb (and_elim_r A B contra)); + (fun (na : not A) => na (π₁ 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 := - and_intro B A - (and_elim_r A B h) - (and_elim_l A B h); + def and_comm (h : A ∧ B) : B ∧ A := <π₂ h, π₁ 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)) - (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; + <<π₁ h, π₁ (π₂ h)>, π₂ (π₂ h)>; -- (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) - (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; + <π₁ (π₁ h), <π₂ (π₁ h), π₂ h>>; -- 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) - (fun (b : B) => or_intro_l (A ∧ B) (A ∧ C) - (and_intro A B (and_elim_l A (B ∨ C) h) b)) - (fun (c : C) => or_intro_r (A ∧ B) (A ∧ C) - (and_intro A C (and_elim_l A (B ∨ C) h) c)); + or_elim B C (A ∧ B ∨ A ∧ C) (π₂ h) + (fun (b : B) => or_intro_l (A ∧ B) (A ∧ C) <π₁ h, b>) + (fun (c : C) => or_intro_r (A ∧ B) (A ∧ 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) - (and_elim_l A B ab) - (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))); + (fun (ab : A ∧ B) => <π₁ ab, or_intro_l B C (π₂ ab)>) + (fun (ac : A ∧ C) => <π₁ ac, or_intro_r B C (π₂ ac)>); -- Thanks Quinn! -- A ∨ B => ~B => A diff --git a/lib/Check.hs b/lib/Check.hs index c790bfe..55ecce0 100644 --- a/lib/Check.hs +++ b/lib/Check.hs @@ -16,6 +16,12 @@ matchPi x mt = (Pi _ a b) -> pure (a, b) t -> throwError $ ExpectedPiType x t +matchProd :: Expr -> Expr -> ReaderT Env Result (Expr, Expr) +matchProd x mt = + whnf mt >>= \case + (Prod a b) -> pure (a, b) + t -> throwError $ ExpectedProdType 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 (Prod 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 $ Prod aType bType + pure $ Prod aType bType +findType g (Pi1 x) = fst <$> (findType g x >>= matchProd x) +findType g (Pi2 x) = snd <$> (findType g x >>= matchProd x) checkType :: Env -> Expr -> Result Expr checkType env t = runReaderT (findType [] t) env diff --git a/lib/Elaborator.hs b/lib/Elaborator.hs index 9d2492f..b0cc77d 100644 --- a/lib/Elaborator.hs +++ b/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.Prod 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.Prod m n) = I.Prod <$> 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.Prod m n) = E.Prod <$> 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 diff --git a/lib/Errors.hs b/lib/Errors.hs index a4a91a2..298f4d5 100644 --- a/lib/Errors.hs +++ b/lib/Errors.hs @@ -9,6 +9,7 @@ data Error = UnboundVariable Text | NotASort Expr | ExpectedPiType Expr Expr + | ExpectedProdType 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 (ExpectedProdType 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) diff --git a/lib/Eval.hs b/lib/Eval.hs index bc32fa4..51d4060 100644 --- a/lib/Eval.hs +++ b/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 (Prod m n) = Prod (subst k s m) (subst k 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 (Prod a b) = Prod <$> 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 + (Prod a b, Prod 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 () diff --git a/lib/Expr.hs b/lib/Expr.hs index 2bb721b..5fce231 100644 --- a/lib/Expr.hs +++ b/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 + Prod :: 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 + (Prod x1 y1) == (Prod 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 (Prod 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 (Prod m n) = Prod (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,10 @@ prettyExpr k expr = case expr of where (binds, body) = collectLets expr bindings = sep $ map pretty binds + (Prod x y) -> parens $ parens (pretty x) <+> "×" <+> parens (pretty y) + (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 diff --git a/lib/IR.hs b/lib/IR.hs index ae654a0..c0c45e2 100644 --- a/lib/IR.hs +++ b/lib/IR.hs @@ -27,6 +27,16 @@ data IRExpr , letValue :: IRExpr , letBody :: IRExpr } + | Prod + { prodLeft :: IRExpr + , prodRight :: IRExpr + } + | Pair + { pairLeft :: IRExpr + , pairRight :: IRExpr + } + | Pi1 IRExpr + | Pi2 IRExpr deriving (Show, Eq, Ord) data IRSectionDef diff --git a/lib/Parser.hs b/lib/Parser.hs index a8eb2f4..e0605ef 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -174,8 +174,26 @@ pSort = lexeme $ pStar <|> pSquare pOpSection :: Parser IRExpr pOpSection = lexeme $ parens $ Var <$> pSymbol +pProd :: Parser IRExpr +pProd = lexeme $ between (char '{') (char '}') $ do + left <- pIRExpr + _ <- symbol "×" + Prod 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, pProd, pPair, try pOpSection, parens pIRExpr] pInfix :: Parser IRExpr pInfix = parseWithPrec 0