perga/README.md

# Table of Contents

1.  [Syntax](#org5c21ec8)
2.  [Basic Usage](#org3caa2bf)
    1.  [Sample Session](#org206dc85)
3.  [Goals](#org677567c)
    1.  [Substantive](#org6946354)
        1.  [DEFINITIONS](#orga4323f7)
        2.  [Inference](#org4a2e73d)
        3.  [Implicits](#orgd2f67c2)
        4.  [Universes?](#orgec0ab63)
        5.  [Inductive Definitions](#org2f139ca)
    2.  [Cosmetic/usage/technical](#orgf241f8d)
        1.  [Prettier pretty printing](#org8686345)
        2.  [Better usage](#orgee07e09)
        3.  [Improve error messages](#org9739c98)
        4.  [Improve β-equivalence check](#orgd3ee15c)
        5.  [Better testing](#orgb19926c)

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.


<a id="org5c21ec8"></a>

# 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&rsquo;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)


<a id="org3caa2bf"></a>

# 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.


<a id="org206dc85"></a>

## Sample Session

Here&rsquo;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.


<a id="org677567c"></a>

# Goals


<a id="org6946354"></a>

## Substantive


<a id="orga4323f7"></a>

### TODO DEFINITIONS

Some kind of definition system would be a difficult and substantial addition, but man is it necessary to do anything. Likewise, I&rsquo;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&rsquo;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.


<a id="org4a2e73d"></a>

### TODO Inference

Obviously not fully decidable, but I might be able to implement some basic unification algorithm. This isn&rsquo;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.


<a id="orgd2f67c2"></a>

### TODO Implicits

Much, much more useful than [inference](#org4a2e73d), 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.


<a id="orgec0ab63"></a>

### TODO Universes?

Not really necessary without [inductive definitions](#org2f139ca), but could be fun.


<a id="org2f139ca"></a>

### 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&rsquo;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.


<a id="orgf241f8d"></a>

## Cosmetic/usage/technical


<a id="org8686345"></a>

### 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](https://hackage.haskell.org/package/prettyprinter) to be able to nicely handle indentation and line breaks.


<a id="orgee07e09"></a>

### TODO Better usage

Read input from a file if a filename is given, otherwise drop into a repl. Perhaps use something like [haskeline](https://hackage.haskell.org/package/haskeline) to improve the repl (though `rlwrap` is fine, so not a huge priority).


<a id="org9739c98"></a>

### TODO Improve error messages

The error messages currently aren&rsquo;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&rsquo;m doing for unbound variables?


<a id="orgd3ee15c"></a>

### TODO Improve β-equivalence check

The check for β-equivalence could certainly be a lot smarter. This is much less of an issue without [inductive definitions](#org2f139ca)/recursion, as far less computation gets done in general, let alone at the type level. That being said, it&rsquo;s certainly not a bad idea.


<a id="orgb19926c"></a>

### TODO Better testing

Using some kind of testing framework, like [QuickCheck](https://hackage.haskell.org/package/QuickCheck) and/or [HUnit](https://hackage.haskell.org/package/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.