Makkai

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

C ctx means C is a context.
C ⊢ X set means X is a set in context C.
C ⊢ m : X means m is an element of set X.
C ⊢ S signature means S is a signature in context C.
C ⊢ I :: S means I is an instance of signature S.

Contexts are built by extension with either kind of binding: - · ctx. - C, x : X ctx, when C ⊢ X set. - C, i :: S ctx, when C ⊢ S signature.

Everywhere below, ... ranges over a finite (possibly zero) index, and the labels xi, si, vi are assumed distinct within any single list.

The set layer

Built-Ins

For each B ∈ { Nat, Int, Float, Str }: - Formation. C ⊢ B set. - Intro. Literals of the appropriate form match the corresponding built-in (e.g. C ⊢ 7 : Nat).

Variables

C ⊢ x : X when x : X is in C.

Records

Formation. C ⊢ record { x0 : X0, ..., xn : Xn } set when C ⊢ X0 set, C, x0 : X0 ⊢ X1 set, ..., C, x0 : X0, ..., xn-1 : Xn-1 ⊢ Xn set.
Intro. C ⊢ { x0 = m0, ..., xn = mn } : record { x0 : X0, ..., xn : Xn } when C ⊢ m0 : X0, C ⊢ m1 : X1[m0/x0], ..., C ⊢ mn : Xn[m0/x0, ..., mn-1/xn-1].
Elim. C ⊢ m.xi : Xi[(m .x0)/x0, ..., (m .xi-1)/xi-1] when C ⊢ m : record { x0 : X0, ..., xn : Xn }.
β. { ..., xi = mi, ... } .xi=mi.
η. m=record { x0=m .x0, ..., xn=m .xn } when m : record { ... }.

Variants

Formation. C ⊢ variant [ v0 : X0 | ... | vn : Xn ] set when each C ⊢ Xi set.
Intro. C ⊢ vi. m : variant [ v0 : X0 | ... | vn : Xn ] when C ⊢ m : Xi.
Elim. C ⊢ case m of [ v0. x0 => n0 | ... | vn. xn => nn ] : X when C ⊢ m : variant [ v0 : X0 | ... | vn : Xn ] and, for each i, C, xi : Xi ⊢ ni : X.
β. case vi. m of [ ... | vi. xi => ni | ... ]=ni[m/xi].
η. m=case m of [ v0. x0 => v0. x0 | ... | vn. xn => vn. xn ] when m : variant [ ... ].

The signature layer

Theory

Formation. C ⊢ theory { s0 :: S0, ..., sn :: Sn } signature when C ⊢ S0 signature, C, s0 :: S0 ⊢ S1 signature, ..., C, s0 :: S0, ..., sn-1 :: Sn-1 ⊢ Sn signature.
Intro. C ⊢ { s0 = I0, ..., sn = In } :: theory { s0 :: S0, ..., sn :: Sn } when C ⊢ I0 :: S0, C ⊢ I1 :: S1[I0/s0], ..., C ⊢ In :: Sn[I0/s0, ..., In-1/sn-1].
Elim. C ⊢ I .si :: Si[(I .s0)/s0, ..., (I .si-1)/si-1] when C ⊢ I :: theory { s0 :: S0, ..., sn :: Sn }.
β. { ..., si=Ii, ... } .si=Ii.
η. I={ s0=I .s0, ..., sn=I .sn } when I :: theory { ... }.

Variables

C ⊢ i :: S when i :: S is in C.

The interface between signatures and sets

The signature `Set`

Formation. C ⊢ Set signature.
Intro. C ⊢ X :: Set when C ⊢ X set.
Elim. C ⊢ set-of(I) set when C ⊢ I :: Set.
β. set-of(X)=X when X :: Set arises from C ⊢ X set.
η. I=set-of(I) viewed as an instance, when I :: Set.

Extension signatures

Formation. C ⊢ (x: X) -> S signature when C ⊢ X set and C, x : X ⊢ S signature.
Intro. C ⊢ for (y: X). I :: (x: X) -> S when C, y : X ⊢ I :: S[y/x].
β. (for (x: X). I)(y)=I[y/x].
η. I=for (x: X). I(x) when x is not free in I.

Instances via case analysis

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

Lifted sets

Formation. C ⊢ <X> signature when C ⊢ X set.
Intro. C ⊢ <m> :: <X> when C ⊢ m : X.
Elim. C ⊢ element-of(I) : X when C ⊢ I :: <X>.
β. element-of(<m>)=m when m : X.
η. I=<element-of(I)> when I :: <X>.

Notes

There are no formal large eliminators, and as such we cannot perform case analysis on an element and produce varying set or signatures. However, the former construction may be losslessly encoded by detouring through instances-via-case-analysis and the signature Set. That is, set-of(case m of [ ... | vi. xi => Xi :: Set | ... ]) is a set that varies depending on an element.

The signatures Set and <_> each give a full isomorphism between the corresponding set-layer and signature-layer notion (sets ~ instances of Set; elements of X ~ instances of <X>), via set-of/element-of respectively. These are parallel in some sense, and do not interact.

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.