From 89304b27ea81270684810c18d3315c9d399beaf9 Mon Sep 17 00:00:00 2001 From: tslil Date: Tue, 5 May 2026 11:15:07 +0100 Subject: address remaining TODO, fix issues with left-nesting for for and ext, add motivation blurb to the readme --- README.md | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index a6cf033..1ff5a86 100644 --- a/README.md +++ b/README.md @@ -2,6 +2,22 @@ A simple type theory. +## Motivation + +There's a pleasant story here about categorical semantics in `Alg(Fam(Lex))^op`, but the real impetus for developing and implementing this particular fragment was the exercise: i had never implemented a dependent type theory before, and wanted to know whether i could deduce how to do so by trying. You, the reader, may be the judge of those efforts. + +As a consequence, this code is 100% artisanal, hand-crafted, guaranteed-cruft-and-hacks human written (by me). + +Credit goes to [David Jaz](https://www.davidjaz.com/) for developing the fragment and its semantics. Credit goes to me for introducing errors. + +## Rust implementation + +Usage `makkai [--debug] file1.makkai ... fileN.makkai` + +See the [grammar](grammar.txt) for details, and the examples in `examples/`. + +Note: the checker does not presently support η-equivalence in all cases and so has some known errors, and likely therefore, some unknown errors. + ## Type Theory ### Judgements @@ -74,15 +90,6 @@ A construction admitting an instance of any signature, given an element of a var - **Intro.** `C ⊢ case m of { v0. x0 => I0 | ... | vn. xn => In } :: S` when `C ⊢ S signature`, `C ⊢ m : variant { v0. : X0 | ... | vn. : Xn }`, and, for each `i`, `C, xi : Xi ⊢ Ii :: S`. - **β.** `case vi. m of { ... | vi. xi => Ii | ... }=Ii[m/xi]`. - -## Rust implementation - -Usage `makkai [--debug] file1.makkai ... fileN.makkai` - -See the [grammar](grammar.txt) for details, and the examples in `examples/`. - -Note: the checker does not presently support η-equivalence in all cases. - # License Copyright tslil clingman 2026, this programme is free software and is made available under the terms of the GPL v3 or later. See LICENSE for details. -- cgit v1.3.1