working on type checking

app/Check.hs

@@ -1,32 +1,43 @@
+{-# LANGUAGE BangPatterns #-}
 module Check where
 
-import Expr ( Expr(..), betaEquiv, isSort, subst )
-import Data.List ((!?))
 import Control.Monad (guard)
+import Data.List ((!?))
+import Debug.Trace (trace)
+import Expr
 
 type Context = [Expr]
 
+-- λ S : * . λ P : ∏ x : S . * . ∏ x : S . P x
+-- lambda S : * . lambda P : Pi x : S . * . lambda Q : Pi x : S . * . lambda H : (Pi x : S . Pi h : P x . Q x) . lambda G : (Pi x : S . P x) . lambda x : S . H x (G x)
+-- lambda S : * . lambda P : (Pi x : S . *). lambda H : (Pi x : S . P x) . lambda x : S . H x
 findType :: Context -> Expr -> Maybe Expr
 findType g (Var k) = do
-  t <- g !? fromInteger k
+    t <- g !? fromInteger k
-  kind <- findType g t
+    kind <- findType g t
-  guard $ isSort kind
+    guard $ isSort kind
-  Just t
+    pure t
 findType _ Star = Just Square
 findType _ Square = Nothing
 findType g (App m n) = do
-  Pi a b <- findType g m
+    let !_ = trace ("app: " ++ show m ++ "\t" ++ show n) False
-  a' <- findType g n
+    Pi a b <- findType g m
-  guard $ betaEquiv a a'
+    let !_ = trace ("Pi: " ++ show a ++ " . " ++ show b) False
-  Just $ subst 0 n b
+    a' <- findType g n
+    let !_ = trace ("a': " ++ show a' ++ "\n") False
+    guard $ betaEquiv a a'
+    pure $ subst n b
 findType g (Abs t v) = do
-  _argTypeValid <- findType g t
+    argType <- findType g t
-  bodyType <- findType (t : g) v
+    guard $ isSort argType
-  _resTypeValid <- findType g (Pi t bodyType)
+    bodyType <- findType (incIndices t : map incIndices g) v
-  Just $ Pi t bodyType
+    resType <- findType g (Pi t bodyType)
+    guard $ isSort resType
+    pure $ Pi t bodyType
 findType g (Pi t v) = do
-  argType <- findType g t
+    let !_ = trace ("Pi rule: " ++ show t ++ "\t" ++ show v ++ "\n") False
-  guard $ isSort argType
+    argType <- findType g t
-  bodyType <- findType g v
+    guard $ isSort argType
-  guard $ isSort bodyType
+    bodyType <- findType (incIndices t : map incIndices g) v
-  Just bodyType
+    guard $ isSort bodyType
+    pure bodyType

app/Expr.hs

@@ -56,19 +56,29 @@ incIndices = mapIndices (Var . (+ 1))
 decIndices :: Expr -> Expr
 decIndices = mapIndices (Var . subtract 1)
 
-subst :: Integer -> Expr -> Expr -> Expr
+-- substitute 0 for s *AND* decrement indices; only use after reducing a redex.
-subst k s (Var n) = if k == n then s else Var n
+subst :: Expr -> Expr -> Expr
-subst _ _ Star = Star
+subst s (Var 0) = s
-subst _ _ Square = Square
+subst _ (Var n) = Var $ n - 1
-subst k s (App m n) = App (subst k s m) (subst k s n)
+subst _ Star = Star
-subst k s (Abs m n) = Abs (subst k s m) (subst k (incIndices s) n)
+subst _ Square = Square
-subst k s (Pi m n) = Pi (subst k s m) (subst k (incIndices s) n)
+subst s (App m n) = App (subst s m) (subst s n)
+subst s (Abs m n) = Abs (subst s m) (subst s n)
+subst s (Pi m n) = Pi (subst s m) (subst s n)
+
+substnd :: Expr -> Expr -> Expr
+substnd s (Var n) = if n == 0 then s else Var n
+substnd _ Star = Star
+substnd _ Square = Square
+substnd s (App m n) = App (substnd s m) (substnd s n)
+substnd s (Abs m n) = Abs (substnd s m) (substnd s n)
+substnd s (Pi m n) = Pi (substnd s m) (substnd s n)
 
 betaReduce :: Expr -> Expr
 betaReduce (Var k) = Var k
 betaReduce Star = Star
 betaReduce Square = Square
-betaReduce (App (Abs _ v) n) = subst 0 n v
+betaReduce (App (Abs _ v) n) = subst n v
 betaReduce (App m n) = App (betaReduce m) (betaReduce n)
 betaReduce (Abs t v) = Abs (betaReduce t) (betaReduce v)
 betaReduce (Pi t v) = Pi (betaReduce t) (betaReduce v)

app/Main.hs

@@ -3,6 +3,7 @@ module Main where
 import Expr
 import Parser
 import System.IO
+import Check
 
 main :: IO ()
 main = do
@@ -11,4 +12,7 @@ main = do
     input <- getLine
     case pAll input of
         Left err -> putStrLn err
-        Right expr -> putStrLn $ pretty expr
+        Right expr -> case findType [] expr of
+            Just ty -> putStrLn $ pretty expr ++ " : " ++ pretty ty
+            Nothing -> putStrLn $ "Unable to find type for " ++ pretty expr ++ "!"
+    main

app/Parser.hs

@@ -58,7 +58,9 @@ pLAbs = lexeme $ label "λ-abstraction" $ do
   ty <- pExpr
   _ <- defChoice $ "." :| []
   modify (ident :)
-  Abs ty <$> pExpr
+  body <- pExpr
+  modify $ drop 1
+  pure $ Abs ty body
 
 pPAbs :: Parser Expr
 pPAbs = lexeme $ label "Π-abstraction" $ do
@@ -68,7 +70,9 @@ pPAbs = lexeme $ label "Π-abstraction" $ do
   ty <- pExpr
   _ <- defChoice $ "." :| []
   modify (ident :)
-  Pi ty <$> pExpr
+  body <- pExpr
+  modify $ drop 1
+  pure $ Pi ty body
 
 pApp :: Parser Expr
 pApp = foldl1 App <$> some pTerm