added universes; documentation and examples forthcoming

lib/Check.hs

@@ -5,7 +5,7 @@ module Check (checkType, findType) where
 import Control.Monad.Except (MonadError (throwError))
 import Data.List ((!?))
 import Errors
-import Eval (Env, betaEquiv, envLookupTy, isSort, subst, whnf)
+import Eval (Env, betaEquiv, envLookupTy, subst, whnf)
 import Expr (Expr (..), incIndices, occursFree)
 
 type Context = [Expr]
@@ -16,24 +16,23 @@ matchPi x mt =
         (Pi _ a b) -> pure (a, b)
         t -> throwError $ ExpectedPiType x t
 
-validateType :: Context -> Expr -> ReaderT Env Result Expr
+findLevel :: Context -> Expr -> ReaderT Env Result Integer
-validateType g a = do
+findLevel g a = do
     s <- findType g a
-    isSort s >>= flip unless (throwError $ NotASort a s)
+    whnf s >>= \case
-    pure s
+        Level i -> pure i
+        _ -> throwError $ NotASort a s
 
-validateType_ :: Context -> Expr -> ReaderT Env Result ()
+validateType :: Context -> Expr -> ReaderT Env Result ()
-validateType_ g a = void $ validateType g a
+validateType g a = void $ findLevel g a
 
 findType :: Context -> Expr -> ReaderT Env Result Expr
-findType _ Star = pure Square
+findType _ (Level i) = pure $ Level (i + 1)
-findType _ Square = throwError SquareUntyped
 findType g (Var x n) = do
     t <- g !? fromInteger n `whenNothing` throwError (UnboundVariable x)
-    validateType_ g t
+    validateType g t
     pure t
-findType _ (Free n) = do
+findType _ (Free n) = envLookupTy n
-    envLookupTy n
 findType _ (Axiom n) = envLookupTy n
 findType g e@(App m n) = do
     (a, b) <- findType g m >>= matchPi m
@@ -42,23 +41,15 @@ findType g e@(App m n) = do
     unless equiv $ throwError $ NotEquivalent a a' e
     pure $ subst 0 n b
 findType g (Abs x a m) = do
-    validateType_ g a
+    validateType g a
     b <- findType (incIndices a : map incIndices g) m
-    validateType_ g (Pi x a b)
+    validateType g (Pi x a b)
     pure $ if occursFree 0 b then Pi x a b else Pi "" a b
 findType g (Pi _ a b) = do
-    validateType_ g a
+    i <- findLevel g a
-    validateType (incIndices a : map incIndices g) b
+    j <- findLevel (incIndices a : map incIndices g) b
+    pure $ Level $ max (i - 1) j -- This feels very sketchy, but otherwise `forall (A : *), A` has type *1
 findType g (Let _ v b) = findType g (subst 0 v b)
-    -- a <- findType g v
-    -- validateType_ g a
-    -- res <- findType (incIndices a : map incIndices g) b
-    -- pure $ subst 0 a res
-
--- this is kinda goofy, it's just like a function, except the resulting type
--- of the body doesn't need to result in a valid function type
--- this means things like `let x := * in ...` would be allowed, even though
--- you couldn't write a function that takes something of type `□` as an argument
 
 checkType :: Env -> Expr -> Result Expr
 checkType env t = runReaderT (findType [] t) env

lib/Eval.hs

@@ -42,8 +42,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 _ _ Square = Square
 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)
@@ -95,7 +94,7 @@ betaEquiv e1 e2
             (Axiom n, Axiom m) -> pure $ n == m
             (Free n, e) -> envLookupVal n >>= betaEquiv e
             (e, Free n) -> envLookupVal n >>= betaEquiv e
-            (Star, Star) -> pure True
+            (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
@@ -107,8 +106,7 @@ checkBeta :: Env -> Expr -> Expr -> Result Bool
 checkBeta env e1 e2 = runReaderT (betaEquiv e1 e2) env
 
 isSortPure :: Expr -> Bool
-isSortPure Star = True
+isSortPure (Level _) = True
-isSortPure Square = True
 isSortPure _ = False
 
 isSort :: Expr -> ReaderT Env Result Bool

lib/Expr.hs

@@ -4,8 +4,7 @@ data Expr where
     Var :: Text -> Integer -> Expr
     Free :: Text -> Expr
     Axiom :: Text -> Expr
-    Star :: Expr
+    Level :: Integer -> Expr
-    Square :: Expr
     App :: Expr -> Expr -> Expr
     Abs :: Text -> Expr -> Expr -> Expr
     Pi :: Text -> Expr -> Expr -> Expr
@@ -16,8 +15,7 @@ instance Eq Expr where
     (Var _ n) == (Var _ m) = n == m
     (Free s) == (Free t) = s == t
     (Axiom a) == (Axiom b) = a == b
-    Star == Star = True
+    (Level i) == (Level j) = i == j
-    Square == Square = True
     (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2
     (Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2
     (Pi _ t1 b1) == (Pi _ t2 b2) = t1 == t2 && b1 == b2
@@ -28,8 +26,7 @@ occursFree :: Integer -> Expr -> Bool
 occursFree n (Var _ k) = n == k
 occursFree _ (Free _) = False
 occursFree _ (Axiom _) = False
-occursFree _ Star = False
+occursFree _ (Level _) = False
-occursFree _ Square = False
 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
@@ -41,8 +38,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 _ _ Square = Square
 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)
@@ -114,8 +110,9 @@ helper :: Integer -> Expr -> Text
 helper _ (Var s _) = s
 helper _ (Free s) = s
 helper _ (Axiom s) = s
-helper _ Star = "*"
+helper _ (Level i)
-helper _ Square = "□"
+    | i == 0 = "*"
+    | otherwise = "*" <> show i
 helper k (App e1 e2) = if k > 3 then parenthesize res else res
   where
     res = helper 3 e1 <> " " <> helper 4 e2

lib/Parser.hs

@@ -140,10 +140,13 @@ pApp :: Parser Expr
 pApp = lexeme $ foldl1 App <$> some pTerm
 
 pStar :: Parser Expr
-pStar = lexeme $ Star <$ eat "*"
+pStar = lexeme $ Level 0 <$ eat "*"
 
-pSquare :: Parser Expr
+pNumSort :: Parser Expr
-pSquare = lexeme $ Square <$ defChoice ("□" :| ["[]"])
+pNumSort = lexeme $ label "sort" $ eat "*" >> Level <$> L.decimal
+
+pSort :: Parser Expr
+pSort = try pNumSort <|> pStar
 
 checkAscription :: Text -> Expr -> Maybe Expr -> Parser ()
 checkAscription ident value massert = do
@@ -190,8 +193,7 @@ pTerm =
         label "term" $
             choice
                 [ between (char '(') (char ')') pExpr
-                , pStar
+                , pSort
-                , pSquare
                 , pVar
                 ]