added README

README.org

@@ -0,0 +1,83 @@
+#+title: Dependent Lambda
+
+A basic implementation of a dependently typed lambda calculus (calculus of constructions) based on the exposition in Nederpelt and Geuvers /Type Theory and Formal Proof/. Right now it is /technically/ 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.
+
+* Syntax
+The syntax is fairly flexible and should work as you expect. Identifiers can be Unicode as long as =megaparsec= calls them alphanumeric. Lambda and Pi abstractions can be written in many obvious 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.
+
+All of the following examples correctly parse, and should look familiar if you are used to standard lambda calculus notation or Coq syntax.
+#+begin_src
+  λ (α : *) . λ (β : *) . λ (x : α) . λ (y : β) . x
+  fun (A B C : *) (g : → C) (f : A → B) (x : A) ⇒ g (f x)
+  fun (S : *) (P Q : S -> *) (H : Π (x : S) . P x -> Q x) (HP : forall (x : S), P x) => fun (x : S) => H x (HP x)
+#+end_src
+
+* Basic Usage
+For the moment, running the program drops you into a repl where you can enter terms in the calculus of construction, which the system will then type check and report the type of the entered term, or any errors if present.
+
+** Sample Session
+Here's a sample session. Suppose your goal is to prove that for every set $S$ and pair of propositions $P$ and $Q$ on $S$, if $\forall x \in S, P x$ holds, and $\forall x \in S, P x \Rightarrow Q x$, then $\forall x \in S, Q x$. A set $S$ corresponds to a type =S=, so our term will begin
+#+begin_src
+  > fun (S : *)
+#+end_src
+Likewise propositions are functions from =S → *=, so we can continue
+#+begin_src
+  > fun (S : *) (P Q : S → *)
+#+end_src
+Since $\forall$ corresponds with =Π=, the hypothesis $\forall x \in S, P x$ would correspond to the type =Π (x : S) . P x= and the hypothesis $\forall x \in S, P x \Rightarrow Q x$ would correspond with =Π (x : S) . P x → Q x=. Thus we can continue
+#+begin_src
+  > fun (S : *) (P Q : S → *) (HP : forall (x : S), P x) (H : forall (x : S), P x → Q x)
+#+end_src
+Since we are trying to prove a universally quantified proposition, we need to introduce an =x : S=, so
+#+begin_src
+  > fun (S : *) (P Q : S → *) (HP : forall (x : S), P x) (H : forall (x : S), P x → Q x) (x : S)
+#+end_src
+Finally, all we have left to do is find something of type =Q x=. We can get to =Q x= using =H x= if we can find something of type =P x=. Fortunately, =HP x= is type =P x=, so our final term is
+#+begin_src
+  > fun (S : *) (P Q : S → *) (HP : forall (x : S), P x) (H : forall (x : S), P x → Q x) (x : S) ⇒ H x (HP x)
+#+end_src
+Pressing enter to send this term to the system, it responds with
+#+begin_src
+  λ (S : *) (P Q : S -> *) (HP : ∏ (x : S) . P x) (H : ∏ (x : S) . P x -> Q x) (x : S) . H x (HP x) : ∏ (S : *) (P Q : S -> *) . (∏ (x : S) . P x) -> (∏ (x : S) . P x -> Q x) -> ∏ (x : S) . Q x
+#+end_src
+This output is a bit hard to read, but it is ultimately in the form =term : type=. The =term= is, up to minor syntactic differences, the term we entered, and the =type= is the type of the term inferred by the system. As a nice sanity check, we can verify that the =type= indeed corresponds to the theorem we wanted to prove.
+
+More complex and interesting proofs and theorems are technically possible (in fact, /all/ interesting theorems and proofs are possible, for a certain definition of /interesting/, /theorem/, and /proof/), though practically infeasible without definitions.
+
+* Goals
+
+** Substantive
+
+*** TODO DEFINITIONS
+Some kind of definition system would be a difficult and substantial addition, but man is it necessary to do anything. Likewise, I'd probably want a way to define primitive notions/axioms, but that should be an easy extension of the definition system. Further following /Type Theory and Formal Proof/ would additionally yield a nice context system, which would be handy, though I disagree with the choice to differentiate between parameterized definitions and functions. That distinction doesn't really make sense in full calculus of constructions.
+
+Sidenote: With a definition system, I would greatly prefer Haskell-style type annotations to ML-style type annotations, though the latter are likely way easier to implement. It serves as a nice bit of documentation, de-clutters the function definition, and follows the familiar mathematical statement-proof structure.
+
+*** TODO Inference
+Obviously not fully decidable, but I might be able to implement some basic unification algorithm. This isn't super necessary though, I find leaving off the types of arguments to generally be a bad idea, but in some cases it can be worth it.
+
+*** TODO Implicits
+Much, much more useful than [[Inference][inference]], implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none.
+
+*** TODO Universes?
+Not really necessary without [[Inductive Definitions][inductive definitions]], but could be fun.
+
+*** 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 easier, by avoiding needing to manually stipulate elimination rules, including induction principles.
+
+** Cosmetic/usage/technical
+
+*** TODO Prettier pretty printing
+Right now, everything defaults to one line, which can be a problem with how large the proof terms get. Probably want to use [[https://hackage.haskell.org/package/prettyprinter][prettyprinter]] to be able to nicely handle indentation and line breaks.
+
+*** TODO Better usage
+Read input from a file if a filename is given, otherwise drop into a repl. Perhaps use something like [[https://hackage.haskell.org/package/haskeline][haskeline]] to improve the repl (though =rlwrap= is fine, so not a huge priority).
+
+*** TODO Improve error messages
+The error messages currently aren't terrible, but it would be nice to have, e.g. line numbers. =megaparsec= allows for semantic errors, so somehow hook into that like what I'm doing for unbound variables?
+
+*** TODO Improve β-equivalence check
+The check for β-equivalence could certainly be a lot smarter. This is much less of an issue without [[Inductive Definitions][inductive definitions]]/recursion, as far less computation gets done in general, let alone at the type level. That being said, it's certainly not a bad idea.
+
+*** TODO Better testing
+Using some kind of testing framework, like [[https://hackage.haskell.org/package/QuickCheck][QuickCheck]] and/or [[https://hackage.haskell.org/package/HUnit][HUnit]] seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable.

app/Check.hs

@@ -1,43 +1,54 @@
-{-# LANGUAGE BangPatterns #-}
 module Check where
 
-import Control.Monad (guard)
+import Control.Monad.Except
-import Data.List ((!?))
+import Data.List (intercalate, (!?))
-import Debug.Trace (trace)
+
+import Control.Monad (unless)
 import Expr
 
 type Context = [Expr]
 
--- λ S : * . λ P : ∏ x : S . * . ∏ x : S . P x
+data TypeCheckError = SquareUntyped | UnboundVariable String | NotASort Expr Expr | ExpectedPiType Expr Expr | NotEquivalent Expr Expr Expr
--- 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
+instance Show TypeCheckError where
-findType :: Context -> Expr -> Maybe Expr
+    show SquareUntyped = "□ does not have a type"
-findType g (Var k) = do
+    show (UnboundVariable x) = "Unbound variable: " ++ x
-    t <- g !? fromInteger k
+    show (NotASort x t) = "Expected " ++ pretty x ++ " to have type * or □, instead found " ++ pretty t
-    kind <- findType g t
+    show (ExpectedPiType m a) = pretty m ++ " : " ++ pretty a ++ " is not a function"
-    guard $ isSort kind
+    show (NotEquivalent a a' e) = "Cannot unify " ++ pretty a ++ " with " ++ pretty a' ++ " when evaluating " ++ pretty e
+
+type CheckResult = Either TypeCheckError
+
+matchPi :: Expr -> Expr -> CheckResult (Expr, Expr)
+matchPi _ (Pi _ a b) = Right (a, b)
+matchPi m e = Left $ ExpectedPiType m e
+
+showContext :: Context -> String
+showContext g = "[" ++ intercalate ", " (map show g) ++ "]"
+
+findType :: Context -> Expr -> CheckResult Expr
+findType _ Star = Right Square
+findType _ Square = Left SquareUntyped
+findType g (Var n x) = do
+    t <- maybe (Left $ UnboundVariable x) Right $ g !? fromInteger n
+    s <- findType g t
+    unless (isSort s) $ throwError $ NotASort t s
     pure t
-findType _ Star = Just Square
+findType g e@(App m n) = do
-findType _ Square = Nothing
+    (a, b) <- findType g m >>= matchPi m
-findType g (App m n) = do
-    let !_ = trace ("app: " ++ show m ++ "\t" ++ show n) False
-    Pi a b <- findType g m
-    let !_ = trace ("Pi: " ++ show a ++ " . " ++ show b) False
     a' <- findType g n
-    let !_ = trace ("a': " ++ show a' ++ "\n") False
+    unless (betaEquiv a a') $ throwError $ NotEquivalent a a' e
-    guard $ betaEquiv a a'
+    pure $ subst 0 n b
-    pure $ subst n b
+findType g (Abs x a m) = do
-findType g (Abs t v) = do
+    s1 <- findType g a
-    argType <- findType g t
+    unless (isSort s1) $ throwError $ NotASort a s1
-    guard $ isSort argType
+    b <- findType (incIndices a : map incIndices g) m
-    bodyType <- findType (incIndices t : map incIndices g) v
+    s2 <- findType g (Pi x a b)
-    resType <- findType g (Pi t bodyType)
+    unless (isSort s2) $ throwError $ NotASort (Pi x a b) s2
-    guard $ isSort resType
+    pure $ if occursFree 0 b then Pi x a b else Pi "" a b
-    pure $ Pi t bodyType
+findType g (Pi _ a b) = do
-findType g (Pi t v) = do
+    s1 <- findType g a
-    let !_ = trace ("Pi rule: " ++ show t ++ "\t" ++ show v ++ "\n") False
+    unless (isSort s1) $ throwError $ NotASort a s1
-    argType <- findType g t
+    s2 <- findType (incIndices a : map incIndices g) b
-    guard $ isSort argType
+    unless (isSort s2) $ throwError $ NotASort b s2
-    bodyType <- findType (incIndices t : map incIndices g) v
+    pure s2
-    guard $ isSort bodyType
-    pure bodyType

app/Expr.hs

@@ -3,48 +3,96 @@
 module Expr where
 
 import Data.Function (on)
-import Data.List (genericDrop)
 
 data Expr where
-    Var :: Integer -> Expr
+    Var :: Integer -> String -> Expr
     Star :: Expr
     Square :: Expr
     App :: Expr -> Expr -> Expr
-    Abs :: Expr -> Expr -> Expr
+    Abs :: String -> Expr -> Expr -> Expr
-    Pi :: Expr -> Expr -> Expr
+    Pi :: String -> Expr -> Expr -> Expr
-    deriving (Show, Eq)
+    deriving (Show)
+
+instance Eq Expr where
+    (Var n _) == (Var m _) = n == m
+    Star == Star = True
+    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
+    _ == _ = False
+
+infixl 4 <.>
+
+(<.>) :: Expr -> Expr -> Expr
+(<.>) = App
+
+infixr 2 .->
+
+(.->) :: Expr -> Expr -> Expr
+a .-> b = Pi "" a (incIndices b)
 
 occursFree :: Integer -> Expr -> Bool
-occursFree n (Var k) = n == k
+occursFree n (Var k _) = n == k
 occursFree _ Star = False
 occursFree _ Square = False
-occursFree n (App a b) = occursFree n a || occursFree n b
+occursFree n (App a b) = on (||) (occursFree n) a b
-occursFree n (Abs a b) = occursFree n a || occursFree (n + 1) 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 (Pi _ a b) = occursFree n a || occursFree (n + 1) b
 
 {- --------------------- PRETTY PRINTING ----------------------------- -}
 
--- TODO : store parsed identifiers for better printing
+parenthesize :: String -> String
-genName :: Integer -> String
+parenthesize s = "(" ++ s ++ ")"
-genName k = case genericDrop k ["x", "y", "z", "w", "u", "v"] of
+
-    [] -> 'x' : show (k - 6)
+collectLambdas :: Expr -> ([(String, Expr)], Expr)
-    (v : _) -> v
+collectLambdas (Abs x ty body) = ((x, ty) : params, final)
+  where
+    (params, final) = collectLambdas body
+collectLambdas e = ([], e)
+
+collectPis :: Expr -> ([(String, Expr)], Expr)
+collectPis p@(Pi "" _ _) = ([], p)
+collectPis (Pi x ty body) = ((x, ty) : params, final)
+  where
+    (params, final) = collectPis body
+collectPis e = ([], e)
+
+groupParams :: [(String, Expr)] -> [([String], Expr)]
+groupParams = foldr addParam []
+  where
+    addParam :: (String, Expr) -> [([String], Expr)] -> [([String], Expr)]
+    addParam (x, t) [] = [([x], t)]
+    addParam (x, t) l@((xs, s) : rest)
+        | incIndices t == s = (x : xs, t) : rest
+        | otherwise = ([x], t) : l
+
+showParamGroup :: ([String], Expr) -> String
+showParamGroup (ids, ty) = parenthesize $ unwords ids ++ " : " ++ pretty ty
+
+helper :: Integer -> Expr -> String
+helper _ (Var _ s) = s
+helper _ Star = "*"
+helper _ Square = "□"
+helper k (App e1 e2) = if k > 3 then parenthesize res else res
+  where
+    res = helper 3 e1 ++ " " ++ helper 4 e2
+helper k (Pi "" t1 t2) = if k > 2 then parenthesize res else res
+  where
+    res = helper 3 t1 ++ " -> " ++ helper 2 t2
+helper k e@(Pi{}) = if k > 2 then parenthesize res else res
+  where
+    (params, body) = collectPis e
+    grouped = showParamGroup <$> groupParams params
+    res = "∏ " ++ unwords grouped ++ " . " ++ pretty body
+helper k e@(Abs{}) = if k >= 1 then parenthesize res else res
+  where
+    (params, body) = collectLambdas e
+    grouped = showParamGroup <$> groupParams params
+    res = "λ " ++ unwords grouped ++ " . " ++ pretty body
 
 pretty :: Expr -> String
 pretty = helper 0
-  where
-    helper :: Integer -> Expr -> String
-    helper k (Var n) = genName $ k - n - 1
-    helper _ Star = "*"
-    helper _ Square = "□"
-    helper k (App e1 e2) = "(" ++ helper k e1 ++ " " ++ helper k e2 ++ ")"
-    helper k (Abs ty b) =
-        "(λ" ++ genName k ++ " : " ++ helper k ty ++ " . " ++ helper (k + 1) b ++ ")"
-    helper k (Pi ty b) =
-        if occursFree 0 b
-            then
-                "(∏" ++ genName k ++ " : " ++ helper k ty ++ " . " ++ helper (k + 1) b ++ ")"
-            else "(" ++ helper k ty ++ " -> " ++ helper (k + 1) b ++ ")"
 
 {- --------------- ACTUAL MATH STUFF ---------------- -}
 
@@ -53,46 +101,38 @@ isSort Star = True
 isSort Square = True
 isSort _ = False
 
-mapIndices :: (Integer -> Expr) -> Expr -> Expr
+shiftIndices :: Integer -> Integer -> Expr -> Expr
-mapIndices f (Var n) = f n
+shiftIndices d c (Var k x)
-mapIndices _ Star = Star
+    | k >= c = Var (k + d) x
-mapIndices _ Square = Square
+    | otherwise = Var k x
-mapIndices f (App m n) = App (mapIndices f m) (mapIndices f n)
+shiftIndices _ _ Star = Star
-mapIndices f (Abs m n) = Abs (mapIndices f m) (mapIndices f n)
+shiftIndices _ _ Square = Square
-mapIndices f (Pi m n) = Pi (mapIndices f m) (mapIndices f n)
+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)
 
 incIndices :: Expr -> Expr
-incIndices = mapIndices (Var . (+ 1))
+incIndices = shiftIndices 1 0
 
-decIndices :: Expr -> Expr
+-- substitute s for k *AND* decrement indices; only use after reducing a redex.
-decIndices = mapIndices (Var . subtract 1)
+subst :: Integer -> Expr -> Expr -> Expr
-
+subst k s (Var n x)
--- substitute 0 for s *AND* decrement indices; only use after reducing a redex.
+    | k == n = s
-subst :: Expr -> Expr -> Expr
+    | otherwise = Var (n - 1) x
-subst s (Var 0) = s
+subst _ _ Star = Star
-subst _ (Var n) = Var $ n - 1
+subst _ _ Square = Square
-subst _ Star = Star
+subst k s (App m n) = App (subst k s m) (subst k s n)
-subst _ Square = Square
+subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
-subst s (App m n) = App (subst s m) (subst s n)
+subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices 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 (Var k s) = Var k s
 betaReduce Star = Star
 betaReduce Square = Square
-betaReduce (App (Abs _ v) n) = subst n v
+betaReduce (App (Abs _ _ v) n) = subst 0 n v
 betaReduce (App m n) = App (betaReduce m) (betaReduce n)
-betaReduce (Abs t v) = Abs (betaReduce t) (betaReduce v)
+betaReduce (Abs x t v) = Abs x (betaReduce t) (betaReduce v)
-betaReduce (Pi t v) = Pi (betaReduce t) (betaReduce v)
+betaReduce (Pi x t v) = Pi x (betaReduce t) (betaReduce v)
 
 betaNF :: Expr -> Expr
 betaNF e = if e == e' then e else betaNF e'

app/Main.hs

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

app/Parser.hs

@@ -2,77 +2,90 @@ module Parser where
 
 import Control.Monad
 import Control.Monad.State.Strict
+import Data.Bifunctor (first)
 import Data.Functor.Identity
 import Data.List (elemIndex)
-import Data.List.NonEmpty (NonEmpty((:|)))
+import Data.List.NonEmpty (NonEmpty ((:|)))
 import qualified Data.List.NonEmpty as NE
-import Expr (Expr (..))
+import Expr (Expr (..), incIndices, (.->))
 import Text.Megaparsec hiding (State)
 import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
-import Data.Bifunctor (first)
 
 type InnerState = [String]
 
 data CustomErrors = UnboundVariable String [String] deriving (Eq, Ord, Show)
 
 instance ShowErrorComponent CustomErrors where
-  showErrorComponent (UnboundVariable var bound) =
+    showErrorComponent (UnboundVariable var bound) =
-    "Unbound variable: " ++ var ++ ". Did you mean one of: " ++ unwords bound ++ "?"
+        "Unbound variable: " ++ var ++ ". Did you mean one of: " ++ unwords bound ++ "?"
 
 type Parser = ParsecT CustomErrors String (State InnerState)
 
 skipSpace :: Parser ()
 skipSpace =
-  L.space
+    L.space
-    space1
+        space1
-    (L.skipLineComment "--")
+        (L.skipLineComment "--")
-    (L.skipBlockCommentNested "(*" "*)")
+        (L.skipBlockCommentNested "(*" "*)")
 
 lexeme :: Parser a -> Parser a
 lexeme = L.lexeme skipSpace
 
 pIdentifier :: Parser String
 pIdentifier = label "identifier" $ lexeme $ do
-  firstChar <- letterChar <|> char '_'
+    firstChar <- letterChar <|> char '_'
-  rest <- many $ alphaNumChar <|> char '_'
+    rest <- many $ alphaNumChar <|> char '_'
-  return $ firstChar : rest
+    return $ firstChar : rest
 
 pVar :: Parser Expr
 pVar = label "variable" $ lexeme $ do
-  var <- pIdentifier
+    var <- pIdentifier
-  binders <- get
+    binders <- get
-  case elemIndex var binders of
+    case elemIndex var binders of
-    Just i -> return $ Var $ fromIntegral i
+        Just i -> return $ Var (fromIntegral i) var
-    Nothing -> customFailure $ UnboundVariable var binders
+        Nothing -> customFailure $ UnboundVariable var binders
 
 defChoice :: NE.NonEmpty String -> Parser ()
 defChoice options = lexeme $ label labelText $ void $ choice $ NE.map string options
-  where labelText = NE.head options
+  where
+    labelText = NE.head options
+
+pParamGroup :: Parser [(String, Expr)]
+pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do
+    idents <- some pIdentifier
+    _ <- defChoice $ ":" :| []
+    ty <- pExpr
+    modify (flip (foldl $ flip (:)) idents)
+    pure $ zip idents (iterate incIndices ty)
+
+pParams :: Parser [(String, Expr)]
+pParams = concat <$> some pParamGroup
 
 pLAbs :: Parser Expr
 pLAbs = lexeme $ label "λ-abstraction" $ do
-  _ <- defChoice $ "λ" :| ["lambda"]
+    _ <- defChoice $ "λ" :| ["lambda", "fun"]
-  ident <- pIdentifier
+    params <- pParams
-  _ <- defChoice $ ":" :| []
+    _ <- defChoice $ "." :| ["=>", "⇒"]
-  ty <- pExpr
+    body <- pExpr
-  _ <- defChoice $ "." :| []
+    modify (drop $ length params)
-  modify (ident :)
+    pure $ foldr (uncurry Abs) body params
-  body <- pExpr
-  modify $ drop 1
-  pure $ Abs ty body
 
 pPAbs :: Parser Expr
 pPAbs = lexeme $ label "Π-abstraction" $ do
-  _ <- defChoice $ "∏" :| ["Pi"]
+    _ <- defChoice $ "∏" :| ["Pi", "forall", "∀"]
-  ident <- pIdentifier
+    params <- pParams
-  _ <- defChoice $ ":" :| []
+    _ <- defChoice $ "." :| [","]
-  ty <- pExpr
+    body <- pExpr
-  _ <- defChoice $ "." :| []
+    modify (drop $ length params)
-  modify (ident :)
+    pure $ foldr (uncurry Pi) body params
-  body <- pExpr
+
-  modify $ drop 1
+pArrow :: Parser Expr
-  pure $ Pi ty body
+pArrow = lexeme $ label "->" $ do
+    a <- pAppTerm
+    _ <- defChoice $ "->" :| ["→"]
+    b <- pExpr
+    pure $ a .-> b
 
 pApp :: Parser Expr
 pApp = foldl1 App <$> some pTerm
@@ -85,17 +98,20 @@ pSquare = Square <$ defChoice ("□" :| ["[]"])
 
 pTerm :: Parser Expr
 pTerm =
-  lexeme $
+    lexeme $
-    label "term" $
+        label "term" $
-      choice
+            choice
-        [ between (char '(') (char ')') pExpr,
+                [ between (char '(') (char ')') pExpr
-          pVar,
+                , pVar
-          pStar,
+                , pStar
-          pSquare
+                , pSquare
-        ]
+                ]
+
+pAppTerm :: Parser Expr
+pAppTerm = lexeme $ pLAbs <|> pPAbs <|> pApp
 
 pExpr :: Parser Expr
-pExpr = lexeme $ pLAbs <|> pPAbs <|> pApp
+pExpr = lexeme $ try pArrow <|> pAppTerm
 
 pAll :: String -> Either String Expr
 pAll input = first errorBundlePretty $ fst $ runIdentity $ runStateT (runParserT pExpr "" input) []

dependent-lambda.cabal

@@ -6,12 +6,12 @@ cabal-version:      3.0
 -- Starting from the specification version 2.2, the cabal-version field must be
 -- the first thing in the cabal file.
 
--- Initial package description 'lambda-D' generated by
+-- Initial package description 'dependent-lambda' generated by
 -- 'cabal init'. For further documentation, see:
 --   http://haskell.org/cabal/users-guide/
 --
 -- The name of the package.
-name:               lambda-D
+name:               dependent-lambda
 
 -- The package version.
 -- See the Haskell package versioning policy (PVP) for standards
@@ -54,7 +54,7 @@ extra-doc-files:    CHANGELOG.md
 common warnings
     ghc-options: -Wall
 
-executable lambda-D
+executable dependent-lambda
     -- Import common warning flags.
     import:           warnings