7.8 KiB
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.
λ (α : *) . λ (β : *) . λ (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)
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
> fun (S : *)
Likewise propositions are functions from S → *, so we can continue
> fun (S : *) (P Q : S → *)
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
> fun (S : *) (P Q : S → *) (HP : forall (x : S), P x) (H : forall (x : S), P x → Q x)
Since we are trying to prove a universally quantified proposition, we need to introduce an x : S, so
> fun (S : *) (P Q : S → *) (HP : forall (x : S), P x) (H : forall (x : S), P x → Q x) (x : S)
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
> 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)
Pressing enter to send this term to the system, it responds with
λ (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
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, 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, 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 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 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. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn’t the best strategy. This is much less of an issue without 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 QuickCheck and/or 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.
TODO TUI
This is definitely a stretch goal, 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 brick in order to make this happen.