made universe hierarchy predicative except for lowest

README.org

@@ -1,7 +1,7 @@
 #+title: Perga
 #+options: toc:nil
 
-=perga= is a basic proof assistant based on a dependently typed lambda calculus (calculus of constructions). This implementation is based on the exposition in Nederpelt and Geuvers' /Type Theory and Formal Proof/. Right now it is a perfectly capable higher order logic proof checker, though there is lots of room for improved ergonomics and usability, which I intend to work on. At the moment, =perga= is comparable to Automath in terms of power and ease of use, being slightly more powerful than Automath, and a touch less ergonomic.
+=perga= is a basic proof assistant based on a dependently typed lambda calculus (calculus of constructions), but augmented with a simple universe hierarchy (Extended Calculus of Constructions but without Σ-types, though I intend to add them). This implementation is based on the exposition in Nederpelt and Geuvers' /Type Theory and Formal Proof/. Right now it is a perfectly capable higher order logic proof checker, though there is lots of room for improved ergonomics and usability, which I intend to work on. At the moment, =perga= is comparable to Automath in terms of power and ease of use, being slightly more powerful than Automath, and a touch less ergonomic.
 
 * Syntax
 The syntax is fairly flexible and should work as you expect. Identifiers can be Unicode as long as =megaparsec= calls them alphanumeric. =λ= and =Π= abstractions can be written in the usual ways that should be clear from the examples below. Additionally, arrows can be used as an abbreviation for a Π type where the parameter doesn't appear in the body as usual.
@@ -16,6 +16,8 @@ To be perfectly clear, =λ= abstractions can be written with either "λ" or "fun
 
 =Π= types can be written with either "Π", "∀", or "forall", and are separated from their bodies with a ",". Arrow types can be written "->" or "\to". Like with =λ= abstractions, binders with the same type can be grouped, and multiple binders can occur between the "Π" and the ",". Like with =λ= types, the "return" type can optionally be added after the binders and before the ",", however this is even more useless, as it is nearly always =*=, the type of types.
 
+The universe hierarchy is very similar to Coq, with =* : □ : □₁ : □₂ : ...=, where =*= is impredicative and the =□ᵢ= are predicative. There is no universe polymorphism, making this rather limited. A lack of inductive types (or even just built-in =Σ=-types and sum types) makes doing logic at any universe level other than =*= extremely limited. For ease of typing, =[]1=, =□1=, =[]₁=, and =□₁= are all the same.
+
 =Let= expressions have syntax shown below.
 #+begin_src
   let ( (<ident> (: <type>)? := <expr>) )+ in <expr> end
@@ -179,11 +181,14 @@ I was looking into bidirectional typing and came across a description of univers
 
 Also, everything ends up impredicative (no =* : *=, but quantifying over =*i= still leaves you in =*i=), and my implementation of impredicativity feels a little sketchy. There might be paradoxes lurking. It would be easy to switch it over to being predicative, but, without inductive types or at least more built-in types, logical connectives can only be defined impredicatively, so that will have to wait until we have inductive definitions.
 
-I may follow in Coq's footsteps and switch universe hierarchies to something like =* : □ : □₁ : □₂ : □₃ : ...=, where all the =□ᵢ= are predicative and =*= is impredicative (analogous to =Prop= and =Type i=). For now at least, we definitely need at least the lowest sort to be impredicative to allow for impredicative definitions of connectives.
+I have since followed in Coq's footsteps and switched universe hierarchies to =* : □ : □₁ : □₂ : □₃ : ...=, where all the =□ᵢ= are predicative and =*= is impredicative (analogous to =Prop= and =Type=). For now at least, we definitely need at least the lowest sort to be impredicative to allow for impredicative definitions of connectives.
 
 *** TODO Universe polymorphism
 I have [[Universes?][universes]], but without universe polymorphism, they're basically useless, or at least I am unable to find a practical use for them. (When would you want to quantify over e.g. kinds specifically?)
 
+*** TODO Sigma and sum types
+While not full [[Inductive Definitions][inductive definitions]], builtin sigma and sum types (and probably a unit type to complete the algebra) would make predicative universes actually possible to work in, and generally make working with conjunctions, disjunctions, and existentials much easier (especially with pattern matching). Record types could then likely follow as syntax sugar for a bunch of dependent pairs dealt with by the elaborator, making for easier definitions of e.g. algebraic structures.
+
 *** TODO Inductive Definitions
 This is definitely a stretch goal. It would be cool though, and would turn this proof checker into a much more competent programming language. It's not necessary for the math, but inductive definitions let you leverage computation in proofs, which is amazing. They also make certain definitions way easier, by avoiding needing to manually stipulate elimination rules, including induction principles, and let you keep more math constructive and understandable to the computer.
 
@@ -198,6 +203,8 @@ The repl is decent, probably the most fully-featured repl I've ever made, but im
 *** TODO Improve error messages
 Error messages are decent, but a little buggy. Syntax error messages are pretty ok, but could have better labeling. The type check error messages are decent, but could do with better location information. Right now, the location defaults to the end of the current definition, which is often good enough, but more detail can't hurt. The errors are generally very janky and hard to read. Having had quite a bit of practice reading them now, they actually provide very useful information, but could be made *a lot* more readable.
 
+Since adding [[Multiple levels of AST][an intermediate AST]], the error messages have gotten much worse. This is pretty urgent now.
+
 *** TODO Document library code
 Low priority, as I'm the only one working on this, I'm working on it very actively, and things will continue rapidly changing, but I'll want to get around to it once things stabilize, before I forget how everything works.
 

lib/Check.hs

@@ -2,7 +2,7 @@
 
 module Check (checkType, findType) where
 
-import Control.Monad.Except (MonadError (throwError))
+import Control.Monad.Except (MonadError (throwError), liftEither)
 import Data.List ((!?))
 import Errors
 import Eval (Env, betaEquiv', envLookupTy, subst, whnf)
@@ -21,12 +21,30 @@ findLevel g a = do
     s <- findType g a
     whnf s >>= \case
         Level i -> pure i
+        Star -> pure $ -1 -- HACK: but works, so...
         _ -> throwError $ NotASort a s
 
 validateType :: Context -> Expr -> ReaderT Env Result ()
 validateType g a = void $ findLevel g a
 
+isSort :: Expr -> Bool
+isSort Star = True
+isSort (Level _) = True
+isSort _ = False
+
+compSort :: Expr -> Expr -> Expr -> Expr -> Result Expr
+compSort _ _ Star Star = pure Star
+compSort _ _ Star r@(Level _) = pure r
+compSort _ _ (Level i) Star
+    | i == 0 = pure Star
+    | otherwise = pure $ Level i
+compSort _ _ (Level i) (Level j) = pure $ Level $ max i j
+compSort a b left right
+    | isSort left = throwError $ NotASort b right
+    | otherwise = throwError $ NotASort a left
+
 findType :: Context -> Expr -> ReaderT Env Result Expr
+findType _ Star = pure $ Level 0
 findType _ (Level i) = pure $ Level (i + 1)
 findType g (Var x n) = do
     t <- g !? fromInteger n `whenNothing` throwError (UnboundVariable x)
@@ -46,10 +64,10 @@ findType g f@(Abs x a asc m) = do
     validateType g (Pi x a Nothing b)
     pure $ if occursFree 0 b then Pi x a Nothing b else Pi "" a Nothing b
 findType g f@(Pi _ a asc b) = do
-    i <- findLevel g a
+    aSort <- findType g a
-    j <- findLevel (incIndices a : map incIndices g) b
+    bSort <- findType (incIndices a : map incIndices g) b
-    whenJust asc (betaEquiv' f $ Level j)
+    whenJust asc $ betaEquiv' f bSort
-    pure $ Level $ max (i - 1) j -- This feels very sketchy, but certainly adds impredicativity
+    liftEither $ compSort a b aSort bSort
 findType g (Let _ Nothing v b) = findType g (subst 0 v b)
 findType g e@(Let _ (Just t) v b) = do
     res <- findType g (subst 0 v b)

lib/Elaborator.hs

@@ -26,6 +26,7 @@ elaborate ir = evalState (elaborate' ir) []
     elaborate' (I.Var n) = do
         binders <- get
         pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
+    elaborate' I.Star = pure E.Star
     elaborate' (I.Level level) = pure $ E.Level level
     elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
     elaborate' (I.Abs x t a b) = saveBinders $ do

lib/Eval.hs

@@ -39,6 +39,7 @@ subst k s (Var x n)
     | otherwise = Var x n
 subst _ _ (Free s) = Free s
 subst _ _ (Axiom s) = Axiom s
+subst _ _ Star = Star
 subst _ _ (Level i) = Level i
 subst k s (App m n) = App (subst k s m) (subst k s n)
 subst k s (Abs x m a n) = Abs x (subst k s m) a (subst (k + 1) (incIndices s) n)
@@ -86,18 +87,14 @@ betaEquiv e1 e2
         e1' <- whnf e1
         e2' <- whnf e2
         case (e1', e2') of
-            (Var k1 _, Var k2 _) -> pure $ k1 == k2
-            (Free n, Free m) -> pure $ n == m
             (Free n, e) -> envLookupVal n >>= betaEquiv e
             (e, Free n) -> envLookupVal n >>= betaEquiv e
-            (Axiom n, Axiom m) -> pure $ n == m
-            (Level i, Level j) -> pure $ i == j
             (Abs _ t1 _ v1, Abs _ t2 _ v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
             (Pi _ t1 _ v1, Pi _ t2 _ v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
             (App m1 n1, App m2 n2) -> (&&) <$> betaEquiv m1 m2 <*> betaEquiv n1 n2
             (Let _ _ v b, e) -> betaEquiv (subst 0 v b) e
             (e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
-            _ -> pure False -- remaining cases impossible or false
+            _ -> pure False -- remaining cases impossible, false, or redundant
 
 betaEquiv' :: Expr -> Expr -> Expr -> ReaderT Env Result ()
 betaEquiv' ctxt e1 e2 = unlessM (betaEquiv e1 e2) $ throwError $ NotEquivalent e1 e2 ctxt

lib/Expr.hs

@@ -4,6 +4,7 @@ data Expr where
     Var :: Text -> Integer -> Expr
     Free :: Text -> Expr
     Axiom :: Text -> Expr
+    Star :: Expr
     Level :: Integer -> Expr
     App :: Expr -> Expr -> Expr
     Abs :: Text -> Expr -> Maybe Expr -> Expr -> Expr
@@ -15,6 +16,7 @@ instance Eq Expr where
     (Var _ n) == (Var _ m) = n == m
     (Free s) == (Free t) = s == t
     (Axiom s) == (Axiom t) = s == t
+    Star == Star = True
     (Level i) == (Level j) = i == j
     (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2
     (Abs _ _ t1 b1) == (Abs _ _ t2 b2) = t1 == t2 && b1 == b2
@@ -26,6 +28,7 @@ occursFree :: Integer -> Expr -> Bool
 occursFree n (Var _ k) = n == k
 occursFree _ (Free _) = False
 occursFree _ (Axiom _) = False
+occursFree _ Star = False
 occursFree _ (Level _) = False
 occursFree n (App a b) = on (||) (occursFree n) a b
 occursFree n (Abs _ a _ b) = occursFree n a || occursFree (n + 1) b
@@ -38,6 +41,7 @@ shiftIndices d c (Var x k)
     | otherwise = Var x k
 shiftIndices _ _ (Free s) = Free s
 shiftIndices _ _ (Axiom s) = Axiom s
+shiftIndices _ _ Star = Star
 shiftIndices _ _ (Level i) = Level i
 shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
 shiftIndices d c (Abs x m a n) = Abs x (shiftIndices d c m) a (shiftIndices d (c + 1) n)
@@ -106,13 +110,29 @@ showBinding (ident, params, val) =
             <> " := "
             <> pretty val
 
+printLevel :: Integer -> Text
+printLevel k
+    | k == 0 = "₀"
+    | k == 1 = "₁"
+    | k == 2 = "₂"
+    | k == 3 = "₃"
+    | k == 4 = "₄"
+    | k == 5 = "₅"
+    | k == 6 = "₆"
+    | k == 7 = "₇"
+    | k == 8 = "₈"
+    | k == 9 = "₉"
+    | k < 0 = show k
+    | otherwise = printLevel (k `div` 10) <> printLevel (k `mod` 10)
+
 helper :: Integer -> Expr -> Text
 helper _ (Var s _) = s
 helper _ (Free s) = s
 helper _ (Axiom s) = s
+helper _ Star = "*"
 helper _ (Level i)
-    | i == 0 = "*"
+    | i == 0 = "□"
-    | otherwise = "*" <> show i
+    | otherwise = "□" <> printLevel i
 helper k (App e1 e2) = if k > 3 then parenthesize res else res
   where
     res = helper 3 e1 <> " " <> helper 4 e2

lib/IR.hs

@@ -4,6 +4,7 @@ type Param = (Text, IRExpr)
 
 data IRExpr
     = Var {varName :: Text}
+    | Star
     | Level {level :: Integer}
     | App
         { appFunc :: IRExpr

lib/Parser.hs

@@ -3,7 +3,7 @@
 module Parser where
 
 import Control.Monad.Except
-import Data.List (foldl1)
+import Data.List (foldl, foldl1)
 import qualified Data.Text as T
 import Errors (Error (..))
 import IR
@@ -129,13 +129,34 @@ pApp :: Parser IRExpr
 pApp = lexeme $ foldl1 App <$> some pTerm
 
 pStar :: Parser IRExpr
-pStar = lexeme $ Level 0 <$ eat "*"
+pStar = lexeme $ Star <$ eat "*"
+
+pSquare :: Parser IRExpr
+pSquare = lexeme $ Level 0 <$ defChoice ("□" :| ["[]"])
+
+subscriptDigit :: Parser Integer
+subscriptDigit =
+    choice
+        [ chunk "₀" >> pure 0
+        , chunk "₁" >> pure 1
+        , chunk "₂" >> pure 2
+        , chunk "₃" >> pure 3
+        , chunk "₄" >> pure 4
+        , chunk "₅" >> pure 5
+        , chunk "₆" >> pure 6
+        , chunk "₇" >> pure 7
+        , chunk "₈" >> pure 8
+        , chunk "₉" >> pure 9
+        ]
+
+subscriptInt :: Parser Integer
+subscriptInt = foldl (\acc d -> acc * 10 + d) 0 <$> some subscriptDigit
 
 pNumSort :: Parser IRExpr
-pNumSort = lexeme $ label "sort" $ eat "*" >> Level <$> L.decimal
+pNumSort = lexeme $ pSquare >> Level <$> (L.decimal <|> subscriptInt)
 
 pSort :: Parser IRExpr
-pSort = lexeme $ try pNumSort <|> pStar
+pSort = lexeme $ pStar <|> try pNumSort <|> pSquare
 
 pAxiom :: Parser IRDef
 pAxiom = lexeme $ label "axiom" $ do