simplified syntax and updated README

README.md

@@ -3,25 +3,29 @@
 
 # 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 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.
+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.
 
 All of the following example terms correctly parse, and should look familiar if you are used to standard lambda calculus notation or Coq syntax.
 
-    λ (α : *) . λ (β : *) . λ (x : α) . λ (y : β) . x
+    λ (α : *) ⇒ λ (β : *) ⇒ λ (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)
+    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)
 
-I mostly stick to Coq syntax throughout this file and the examples, as that is what I’m most used to and is easiest to type. I will probably make the syntax more strict in the future, as this level of flexibility is really not necessary.
+To be perfectly clear, `λ` abstractions can be written with either “λ” or “fun”, and are separated from their bodies by either “=>” or “⇒”. Binders with the same type can be grouped together, and multiple binders can occur between the “λ” and the “⇒”.
+
+`Π` types can be written with either “Π”, “∀”, or “forall”, and are separated from their bodies with a “,”. Arrow types can be written “->” or “→”. Like with `λ` abstractions, binders with the same type can be grouped, and multiple binders can occur between the “Π” and the “,”.
 
 Definitions work similarly, having abstract syntax as shown below.
 
     <ident> (<ident> : <type>)* : <type>? := <term> | axiom;
 
-(The distinction between `<type>` and `<term>` is for emphasis; they are the exact same syntactic category.) Here&rsquo;s a couple definitions of the `const` function from above showing the options with the syntax.
+(The distinction between `<type>` and `<term>` is for emphasis; they are the exact same syntactic category.) Here&rsquo;s a couple definitions of the `const` function from above showing the options with the syntax, and a more complex example declaring functional extensionality as an axiom (assuming equality has been previously defined having type `eq : Π (A : *) → A → A → *`).
 
-    const := λ (α : *) . λ (β : *) . λ (x : α) . λ (y : β) . x;
-    const : forall (α β : *), α → β → α := fun (α β : *) (x : α) (y : β) ⇒ x;
+    const := λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) => λ (y : β) => x;
+    const : ∀ (α β : *), α → β → α := fun (α β : *) (x : α) (y : β) ⇒ x;
     const (α β : *) (x : α) (y : β) : α := x;
+    
+    funext (A B : *) (f g : A → B) : (∀ (x : A), eq B (f x) (g x)) → eq (A → B) f g := axiom;
 
 Type ascriptions are optional. If included, `perga` will check to make sure your definition matches the ascription, and, if so, will remember the way your wrote the type when printing inferred types, which is particularly handy when using abbreviations for complex types. `perga` has no problem inferring the types of top-level definitions, as they are completely determined by the term, but I recommend including ascriptions most of the time, as they serve as a nice piece of documentation, help guide the implementation process, and make sure you are implementing the type you think you are.
 
@@ -120,7 +124,7 @@ Obviously not fully decidable, but I might be able to implement some basic unifi
 
 ### TODO Implicits
 
-Much, much more useful than [inference](#orgfd5754c), 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. Getting rid of stuff like [lines 213-215 of the example file](./examples/example.pg) would be amazing.
+Much, much more useful than [inference](#org8f16b1f), 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. Getting rid of stuff like [lines 213-215 of the example file](./examples/example.pg) would be amazing.
 
 
 ### TODO Module System
@@ -130,7 +134,7 @@ A proper module system would be wonderful. To me, ML style modules with structur
 
 ### TODO Universes?
 
-Not really all that necessary, especially without [inductive definitions](#org3e4a465), but could be fun.
+Not super necessary, but could be fun.
 
 
 ### TODO Inductive Definitions
@@ -163,7 +167,7 @@ Error messages are decent, but a little buggy. Syntax error messages are pretty
 
 ### TODO Better testing
 
-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. I made unit tests, then added a ton of stuff. Most of the unit tests are kind of pointless now. For now, I think running the code on the example file is pretty sufficient.
+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. I made unit tests, then added a ton of stuff. Most of the unit tests are kind of pointless now. For now, I think running the code on the example files is pretty sufficient.
 
 
 ### TODO Alternate syntax
@@ -197,7 +201,7 @@ I&rsquo;m imagining the parser could be chosen based on the file extension or so
 
 ### TODO treesitter parser and/or emacs mode
 
-Really not necessary, especially while the syntax is in a bit of flux, but would eventually be nice. The syntax is simple enough that a treesitter grammar shouldn&rsquo;t be too hard to write. An emacs mode would especially be nice if I ever get end up implementing an [alternate syntax](#org461e006), to better handle indentation, automatically adjust line numbers, etc.
+Really not necessary, especially while the syntax is in a bit of flux, but would eventually be nice. The syntax is simple enough that a treesitter grammar shouldn&rsquo;t be too hard to write. An emacs mode would especially be nice if I ever get end up implementing an [alternate syntax](#orgf39c63f), to better handle indentation, automatically adjust line numbers, etc.
 
 
 ### TODO TUI

README.org

@@ -4,25 +4,29 @@
 =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.
 
 * 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 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.
+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.
 
 All of the following example terms correctly parse, and should look familiar if you are used to standard lambda calculus notation or Coq syntax.
 #+begin_src
-  λ (α : *) . λ (β : *) . λ (x : α) . λ (y : β) . x
+  λ (α : *) ⇒ λ (β : *) ⇒ λ (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)
+  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
-I mostly stick to Coq syntax throughout this file and the examples, as that is what I'm most used to and is easiest to type. I will probably make the syntax more strict in the future, as this level of flexibility is really not necessary.
+To be perfectly clear, =λ= abstractions can be written with either "λ" or "fun", and are separated from their bodies by either "=>" or "⇒". Binders with the same type can be grouped together, and multiple binders can occur between the "λ" and the "⇒".
+
+=Π= 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 ",".
 
 Definitions work similarly, having abstract syntax as shown below.
 #+begin_src
   <ident> (<ident> : <type>)* : <type>? := <term> | axiom;
 #+end_src
-(The distinction between =<type>= and =<term>= is for emphasis; they are the exact same syntactic category.) Here's a couple definitions of the =const= function from above showing the options with the syntax.
+(The distinction between =<type>= and =<term>= is for emphasis; they are the exact same syntactic category.) Here's a couple definitions of the =const= function from above showing the options with the syntax, and a more complex example declaring functional extensionality as an axiom (assuming equality has been previously defined having type =eq : Π (A : *) → A → A → *=).
 #+begin_src
-  const := λ (α : *) . λ (β : *) . λ (x : α) . λ (y : β) . x;
-  const : forall (α β : *), α → β → α := fun (α β : *) (x : α) (y : β) ⇒ x;
+  const := λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) => λ (y : β) => x;
+  const : ∀ (α β : *), α → β → α := fun (α β : *) (x : α) (y : β) ⇒ x;
   const (α β : *) (x : α) (y : β) : α := x;
+
+  funext (A B : *) (f g : A → B) : (∀ (x : A), eq B (f x) (g x)) → eq (A → B) f g := axiom;
 #+end_src
 Type ascriptions are optional. If included, =perga= will check to make sure your definition matches the ascription, and, if so, will remember the way your wrote the type when printing inferred types, which is particularly handy when using abbreviations for complex types. =perga= has no problem inferring the types of top-level definitions, as they are completely determined by the term, but I recommend including ascriptions most of the time, as they serve as a nice piece of documentation, help guide the implementation process, and make sure you are implementing the type you think you are.
 
@@ -114,7 +118,7 @@ Much, much more useful than [[Inference][inference]], implicit arguments would b
 A proper module system would be wonderful. To me, ML style modules with structures, signatures, and functors seems like the right way to handle algebraic structures for a relatively simple language, rather than records (or a bunch of =and='s like I currently have) or type classes (probably much harder, but could be nicer), but any way of managing scope, importing files, etc. is a necessity.
 
 *** TODO Universes?
-Not really all that necessary, especially without [[Inductive Definitions][inductive definitions]], but could be fun.
+Not super necessary, 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 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.
@@ -134,7 +138,7 @@ The repl is decent, but implementing something like [[https://abhinavsarkar.net/
 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.
 
 *** TODO Better testing
-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. I made unit tests, then added a ton of stuff. Most of the unit tests are kind of pointless now. For now, I think running the code on the example file is pretty sufficient.
+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. I made unit tests, then added a ton of stuff. Most of the unit tests are kind of pointless now. For now, I think running the code on the example files is pretty sufficient.
 
 *** TODO Alternate syntax
 I've had a bunch of ideas for a more mathematician-friendly syntax bouncing around my head for a while. Implementing one of them would be awesome, but probably quite tricky.

lib/Parser.hs

@@ -69,7 +69,7 @@ pVar = label "variable" $ lexeme $ do
         Nothing -> Free var
 
 pPN :: Parser ()
-pPN = label "primitive notion" $ lexeme $ defChoice $ "PN" :| ["axiom"]
+pPN = label "primitive notion" $ lexeme $ defChoice $ pure "axiom"
 
 defChoice :: NE.NonEmpty Text -> Parser ()
 defChoice options = lexeme $ label (T.unpack $ NE.head options) $ void $ choice $ NE.map chunk options
@@ -90,18 +90,18 @@ pManyParams = lexeme $ concat <$> many pParamGroup
 
 pLAbs :: Parser Expr
 pLAbs = lexeme $ label "λ-abstraction" $ do
-    _ <- defChoice $ "λ" :| ["lambda", "fun"]
+    _ <- defChoice $ "λ" :| ["fun"]
     params <- pSomeParams
-    _ <- defChoice $ "." :| ["=>", "⇒"]
+    _ <- defChoice $ "=>" :| ["⇒"]
     body <- pExpr
     modify $ bindsToIS $ drop $ length params
     pure $ foldr (uncurry Abs) body params
 
 pPAbs :: Parser Expr
 pPAbs = lexeme $ label "Π-abstraction" $ do
-    _ <- defChoice $ "∏" :| ["Pi", "forall", "∀"]
+    _ <- defChoice $ "∏" :| ["forall", "∀"]
     params <- pSomeParams
-    _ <- defChoice $ "." :| [","]
+    _ <- defChoice $ pure ","
     body <- pExpr
     modify $ bindsToIS $ drop $ length params
     pure $ foldr (uncurry Pi) body params