diff options
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 70 |
1 files changed, 43 insertions, 27 deletions
@@ -2,7 +2,9 @@ A simple type theory. -## Judgements +## 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 a match of set `X`. @@ -16,57 +18,71 @@ Contexts are built by extension with either kind of binding: 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 +### The set layer -### Built-Ins +#### 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 +#### 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 { ... }`. +#### 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 { ... }`. +#### 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 +### 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 { ... }`. +#### 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 +#### Variables - `C ⊢ i :: S` when `i :: S` is in `C`. -## The interface between signatures and sets +### The interface between signatures and sets -### The signature `Set` +#### 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 +#### 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 +A construction admitting an instance of any signature, given an element of a variant set and a branch for every tag. +- **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. |