Substitutive Type Theory

I have been thinking on and working on things related to type theory for a long time. Type theories in general are quite unreadable, due either to complex hand-written Haskell-like files, or terse, unreadable tactical proofs. Further, extensional equality and related HoTT axioms are hard to work with in type theory, due to their inability to compute when equality combinators are applied to them. I have solutions for both of these problems, and just need to make a whole type theory from scratch to implement them, of course.

Chain Proofs

Type theories let you formally verify mathematical proofs, but the proofs require a level of detail and specificity, manually applying 'transitive' axioms to 'congruence' axioms to individual terms, that makes the resulting code impenetrable. On the other hand, tactical proof assistants like Coq and Lean create metaprogramming languages that generate these terms automatically, making 'proofs' shorter, but are still utterly impenetrable.

To combat this I want to make a proof system that focuses on what Agda people call 'derivations', proofs that link explicitly stated expressions together, one step at a time. This could be implemented as a language-native 'chain proof' syntax sugar, that finds the smallest subexpression that differs between two steps of a chain, and tries to type check a justification as a proof that those subexpressions are equal. Optionally, that justification could be a tactic that returns Maybe, resulting in a compile-time error if the tactic doesn't produce Just.

In other words, by focusing on 'substitution' as a primitive operation in writing proofs, I think proofs will become readable.

Extensionality

On the other hand, I also have a possible solution to making a type theory with extensionality, univalence, and HITs, that is also based on building 'substitution' into the language in a very different sense, which might lead to an implementation of a HoTT that can compute the way that type theory proofs are supposed to compute. Then you could show two functions are equal using extensionally, prove some result using that proof, and then see what that result actually computes to.

Note that if this HoTT stuff actually worked, you wouldn't really even care about HITs or univalence most of the time... You'd just get on with proving normal math things, but now with useful and convenient function extensionality, at last. HITs might let you define some quotients like rational numbers, and univalence might let you do some cutesie abstract algebra stuff, but extensional equality, that just unlocks mathematics for a proof assistant.

Like with the proof assistant ideas, the way that I want to approach HoTT is also by focusing on 'substitution' as a primitive operation that programmers use, since substitution (congruence, J-elimination, transport) is exactly where axioms like extensionality, univalence, and HIT elimination fail to normalise into anything useful. My approach would be to attack this head on by implementing the substitution primitives as metaprograms internally, through introspection on the lambda expressions and transitive paths they are applied to. This way 'paths' go from a useful fiction to a very real computational primitive that the language can generate, manipulate, and report to the user. This is to be contrasted with Cubical Type Theory, where substitution is side-stepped by changing the definition of equality, and then transitive paths are attacked later using confusing ideas of 'closing boxes', and much like all other type theory paradigms that I have been complaining about, the resulting code is totally impenetrable to later readers.

The themes that are shared between these two ideas are striking: make proof assistants more intuitive and powerful, by turning substitution into a meta-programming primitive. I don't know what to make of that commonality, other than to conclude it would make for a good name for the overall project, thus the "Substitutive Proof Assistant" is born, built on "Substitutive Type Theory".

Attempted Implementations

• github.com/spiveeworks/ml-lambda A lambda calculus parser and printer, written in SML, that I want to build out into a full STT implementation,
• github.com/spiveeworks/algebraic-proof-assistant/tree/hott A little MLTT written in C, designed to have a super lean representation of head normalised expressions. I was going to build this into STT but it was too much C.
• github.com/spiveeworks/algebraic-proof-assistant/ A little proof of concept of the chain proof style. The proofs are really nice, but the top-level syntax needs to be simplified to mix with code better, and the parser itself was way too clunky. Also written in C, of course.
• github.com/lofer-lang/lofer-tc An older MLTT thing written in Rust, parsed using LALRPOP. There are a lot of cool demos in this repo, implementing different data types using church encoding, and then doing type theory to them.
• github.com/lofer-lang/lofer-tc/tree/23fd15f4a6bf0f05ab5f4800cbf333bdd63c1acf An even older version of Lofer, where there were built-in types for void, unit, bool, sigma, pi, and fixpoint, and I was too cool for equality types at the time.

I would like to work on the SML one more, so I can just do some pattern matching on expressions and implement some STT, but I haven't. Oh well.