#+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. * 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. 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 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 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 ",". =Let= expressions have syntax shown below. #+begin_src let ( ( := ) )+ in end #+end_src Below is a more concrete example. #+begin_src let (a := (and_elim_l A (and B C) h)) (bc := (and_elim_r A (and B C) h)) (b := (and_elim_l B C bc)) (c := (and_elim_r B C bc)) in and_intro (and A B) C (and_intro A B a b) c end #+end_src You can also directly bind functions. Here's an example. #+begin_src let (f (A : *) (x : A) := x) in f x end #+end_src The syntax for binding functions is just like with definitions. Definitions have abstract syntax as shown below. #+begin_src ( : )* : ? := | axiom; #+end_src (The distinction between == and == 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 → *=). Duplicate definitions are not normally allowed and will result in an error. #+begin_src 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. If the RHS of a definition is =axiom=, then =perga= will assume that the identifier is an inhabitant of the type ascribed to it (as such when using axioms, a type ascription is required). This allows you to use axioms. Line comments are =--= like in Haskell, and block comments are =[* *]= somewhat like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish. There isn't a proper module system (yet), but you can include other files in a dumb, C preprocessor way by using =@include = (NOTE: this unfortunately messes up line numbers in error messages). Filepaths are relative to the current file. * Usage Running =perga= without any arguments drops you into a basic repl. From here, you can type in definitions which =perga= will typecheck. Previous definitions are accessible in future definitions. The usual readline keybindings are available, including navigating history, which is saved between sessions (in =~/.cache/perga/history=). In the repl, you can enter ":q", press C-c, or press C-d to quit. Entering ":e" shows everything that has been defined along with their types. Entering ":t " prints the type of a particular identifier, while ":v " prints its value. Entering ":n " will fully normalize (including unfolding definitions) an expression, while ":w " will reduce it to weak head normal form. Finally ":l " loads a file. Here's an example session showing the capabilities of the repl. #+begin_src text > :l examples/computation.pg loading: examples/computation.pg > :e eight : nat eq : ∏ (A : *) . A -> A -> * eq_cong : ∏ (A B : *) (x y : A) (f : A -> B) . eq A x y -> eq B (f x) (f y) eq_refl : ∏ (A : *) (x : A) . eq A x x eq_sym : ∏ (A : *) (x y : A) . eq A x y -> eq A y x eq_trans : ∏ (A : *) (x y z : A) . eq A x y -> eq A y z -> eq A x z five : nat four : nat nat : * nine : nat one : nat one_plus_one_is_two : eq nat (plus one one) two plus : nat -> nat -> nat seven : nat six : nat suc : nat -> nat ten : nat three : nat times : nat -> nat -> nat two : nat two_plus_two_is_four : eq nat (plus two two) four two_times_five_is_ten : eq nat (times two five) ten zero : nat > :n plus one one λ (A : *) (f : A -> A) (x : A) . f (f x) > :n two λ (A : *) (f : A -> A) (x : A) . f (f x) > :w plus one one λ (A : *) (f : A -> A) (x : A) . one A f (one A f x) > :w two λ (A : *) (f : A -> A) (x : A) . f (one A f x) #+end_src You can also give =perga= a filename as an argument, in which case it will typecheck every definition in the file. If you give =perga= multiple filenames, it will process each one in turn, sharing an environment between them. Upon finishing, which should be nearly instantaneous, it will print out all files it processed, and "success!" if it successfully typechecked, and the first error it encountered otherwise. * Simple Example There are many very well commented examples in the [[./examples/]] folder. These include - [[./examples/logic.pg]], which defines the standard logical operators and proves standard results about them, - [[./examples/computation.pg]], which demonstrates using =perga= for computational purposes, - [[./examples/algebra.pg]], which defines standard algebraic structures and proves results for them, and - [[./examples/peano.pg]], which proves standard arithmetic results from the Peano axioms. I intend to extend these examples further. Here is an example file defining Leibniz equality and proving that it is reflexive, symmetric, and transitive. #+begin_src -- file: equality.pg -- Defining Leibniz equality -- Note that we can leave the ascription off eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y; -- Equality is reflexive, which is easy to prove -- Here we give an ascription so that when `perga` reports the type, -- it references `eq` rather than inferring the type. eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx; -- Equality is symmetric. This one's a little harder to prove. eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) => Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy; -- Equality is transitive. eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) => Hyz P (Hxy P Hx); #+end_src Running =perga equality.pg= yields the following output. #+begin_src eq : ∏ (A : *) . A -> A -> * eq_refl : ∏ (A : *) (x : A) . eq A x x eq_sym : ∏ (A : *) (x y : A) . eq A x y -> eq A y x eq_trans : ∏ (A : *) (x y z : A) . eq A x y -> eq A y z -> eq A x z #+end_src This means our proofs were accepted. Furthermore, as a sanity check, we can see that the types correspond exactly to what we wanted to prove. * Future Goals ** Substantive *** TODO Sections Coq-style sections would be very handy, and probably /relatively/ easy to implement (compared to everything else on this todo list). Upon parsing a definition inside a section, will somehow need to look ahead to see what variables are used to see how I need to modify =binders=, or just make every definition require every section variable as an argument. *** TODO Inference Not decidable, but I might be able to implement some basic unification algorithm, or switch to bidirectional type checking. 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 handy, especially not at the top level. *** 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 Module System 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, worse, a bunch of =and='s like I currently have; especially painful without [[Implicits][implicits]]) or type classes (probably much harder, but could be nicer), but any way of managing scope, importing files, etc. is a necessity. The [[https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B573FA00832D55D4878863DE1725D90B/S0956796814000264a.pdf/f-ing-modules.pdf][F-ing modules]] paper is probably a good reference. *** DONE Universes? Not super necessary, but occasionally extremely useful. Could be fun, idk. I was looking into bidirectional typing and came across a description of universes. It turned out to be much easier to implement than I was expecting, so I figured why not and added universes. So now =* : *1 : *2 : *3 : ...=. However, they're basically useless without [[Universe polymorphism][universe polymorphism]] of some kind. 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. *** 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 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. ** 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 repl The repl is decent, probably the most fully-featured repl I've ever made, but implementing something like [[https://abhinavsarkar.net/posts/repling-with-haskeline/][this]] would be awesome. *** 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. *** 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. *** TODO Add versions to =perga.cabal= and/or nixify Probably a smart idea. *** TODO More incremental parsing/typechecking Right now, if there's a failure, everything just stops immediately. More incremental parsing/typechecking could pave the way for more interactivity, e.g. development with holes, an LSP server, etc., not to mention better error messages. *** TODO Multiple levels of AST Right now, the parsing and typechecking kind of happens all at once on a single syntax representation. As I add fancier and fancier elaboration, it might be a good idea to have multiple syntax representations. So we'd have one level of syntax representing what is actually in the file (modulo some easy elaboration like with function definitions), and through a series of transformations transform it into something like the current =Expr= type with all the information needed for typechecking and all the complex language features removed. *** TODO Improve type checking algorithm I'm proud that I just kinda made up a working type checking algorithm, but it is clearly quite flawed. Even assuming no need to check beta equivalence, I'm pretty sure that this algorithm is approximately exponential in the length of a term, which is pretty terrible. It hasn't been a huge problem, but type checking just the term =R2_sub_R= in [[./examples/peano.pg]] takes about 1.5 seconds. Performance could easily be drastically improved with some memoization, but upgrading to an off-the-shelf bidirectional type checking algorithm seems like a good idea in general. Another problem with my current type checking algorithm is that it is very inflexible (e.g. adding optional return type ascriptions in functions, or type ascriptions in =let= bindings is currently impossible, while trivial to add with bidirectional type checking). I also have no idea how to add [[Inference][type inference]] or [[Implicits][implicits]] with how things are currently structured. A more flexible type checking algorithm, likely together with [[Multiple levels of AST][multiple levels of AST]], makes it seem more possible. *** 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. Something like #+begin_src text Theorem basic (S : *) (P : S → *) : (∀ (x : S), P x → Q x) → (∀ (x : S), P x) → ∀ (x : S), Q x. Proof 1. Suppose ∀ (x : S), P x → Q x 2. Suppose ∀ (x : S), P x 3. Let x : S 4. P x by [2 x] 5. Q x by [1 x 4] Qed #+end_src I think could be reliably translated into #+begin_src basic (S : *) (P : S → *) : (Π (x : S), P x → Q x) → (Π (x : S), P x) → Π (x : S), Q x := fun (a1 : Π (x : S), P x → Q x) ⇒ fun (a2 : Π (x : S), P x) ⇒ fun (x : S) ⇒ a1 x (a2 x); #+end_src and is more intuitively understandable to a mathematician not familiar with type theory, while the latter would be utter nonsense. I'm imagining the parser could be chosen based on the file extension or something. Some way to mix the syntaxes could be nice too. *** TODO Infix/misfix operators Infix/misfix operators would be very nice and make =perga= look more normal. It's funny, at the moment it looks a lot like a lisp, even though it's totally not. Here's an excerpt from the proof that addition is commutative that looks particularly lispy. #+begin_src (eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n) (plus_s_r n m) (eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n) (eq_cong nat nat (plus n m) (plus m n) suc IH) (eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n)))) #+end_src *** DONE treesitter parser and/or emacs mode There's a [[https://forgejo.ballcloud.cc/wball/tree-sitter-perga][tree-sitter parser]] and [[https://forgejo.ballcloud.cc/wball/perga.nvim][neovim plugin]] available now, but no emacs-mode. *** TODO TUI This is definitely a stretch goal, and I'm not sure how good of an idea it would be, but I'm imagining a TUI split into two panels. On the left you can see the term you are building with holes in it. On the right you have the focused hole's type as well as the types of everything in scope (like Coq and Lean show while you're in the middle of a proof). Then you can interact with the system by entering commands (e.g. =intros=, =apply=, etc.) which changes the proof term on the left. You'd also just be able to type in the left window as well, and edit the proof term directly. This way you'd get the benefits of working with tactics, making it way faster to construct proof terms, and the benefits of working with proof terms directly, namely transparency and simplicity. I'll probably want to look into [[https://hackage.haskell.org/package/brick][brick]] if I want to make this happen.