diff options
| -rw-r--r-- | README.md | 70 | ||||
| -rw-r--r-- | examples/one_simplex.makkai | 31 | ||||
| -rw-r--r-- | examples/signature_param.makkai | 4 | ||||
| -rw-r--r-- | grammar.txt | 34 | ||||
| -rw-r--r-- | src/checker_signature.rs | 37 | ||||
| -rw-r--r-- | src/main.rs | 96 | ||||
| -rw-r--r-- | src/parser.rs | 16 |
7 files changed, 186 insertions, 102 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. diff --git a/examples/one_simplex.makkai b/examples/one_simplex.makkai new file mode 100644 index 0000000..590cf04 --- /dev/null +++ b/examples/one_simplex.makkai @@ -0,0 +1,31 @@ +let signature Graph = theory { + Vertex :: Set, + Edge :: (s : set-of(Vertex)) (t : set-of(Vertex)) -> Set +} + +let set Empty = variant[] +let set Unit = record{} +let element pt : Unit = {} +let set F1 = variant [ one0 : Unit ] +let set F2 = variant [ two0 : Unit | two1 : Unit ] +let set F3 = variant [ three0 : Unit | three1 : Unit | three2: Unit ] + +let instance oneSimplex :: Graph = { + .Vertex = F3 :: Set, + .Edge = for (s : set-of(Vertex)) (t : set-of(Vertex)), + case s of [ + three0. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Unit :: Set | three2. pt => Unit :: Set ] + | three1. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Unit :: Set ] + | three2. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Empty :: Set ] + ] +} + +let set OneSimplexEdges = record { + source: set-of(oneSimplex .Vertex), + target: set-of(oneSimplex .Vertex), + connected: set-of(oneSimplex .Edge source target) +} + +let element vertex0 : F3 = three0. {} +let element vertex1 : F3 = three1. {} +let element edge01 : set-of(oneSimplex .Edge vertex0 vertex1) = pt diff --git a/examples/signature_param.makkai b/examples/signature_param.makkai new file mode 100644 index 0000000..9dae31b --- /dev/null +++ b/examples/signature_param.makkai @@ -0,0 +1,4 @@ +let signature S = theory { + F :: (x : Nat) (y : Bool) -> Set, + G :: (z : set-of(F 3 4)) -> Set // this sould fail +} diff --git a/grammar.txt b/grammar.txt index 9772501..e180bb0 100644 --- a/grammar.txt +++ b/grammar.txt @@ -7,6 +7,7 @@ element_decl = "let element" , elem_var , ":" , set , "=" , element ; theory_decl = "let signature" , sig_var , "=" , signature ; instance_decl = "let instance" , inst_var , "::" , signature , "=" , instance ; +(* Sets *) set = record_set | variant_set | builtin_set | claimed_set | set_var | "(" , set , ")" ; record_set = "record" , "{" , [ set_field { "," , set_field } ] , "}" ; set_field = lower_ident , ":" , set ; @@ -15,31 +16,40 @@ variant_field = lower_ident , ":" , set ; builtin_set = "Nat" | "Int" | "Float" | "Str" | "Bool" ; claimed_set = "set-of" , "(" , instance , ")" ; +(* Signatures *) signature = "Set" | theory_sig | function_sig | sig_var | "(" , signature , ")" ; theory_sig = "theory" , "{" , [ sig_field { "," , sig_field } ] , "}" ; -sig_field = "." , upper_ident , "::" , signature ; +sig_field = upper_ident , "::" , signature ; function_sig = param_list , "->" , signature ; param_list = param { param } ; param = "(" , elem_var , ":" , set , ")" ; +(* Elements *) element = case_elem | dot_elem ; -case_elem = "case" , element , "of" , "{" , [ case_arm { "|" , case_arm } ] , "}" ; -case_arm = inject_elem , elem_var , "=>" , element ; +case_elem = "case" , element , "of" , "[" , [ elem_case_arm { "|" , elem_case_arm } ] , "]" ; +elem_case_arm = inject_elem , elem_var , "=>" , element ; dot_elem = { inject_elem } , atom_elem , { project_elem } ; inject_elem = ident , "." ; project_elem = "." , ident ; -atom_elem = literal | elem_var | record_elem | "(" , element , ")" ; +atom_elem = literal | record_elem | "(" , element , ")" | elem_var ; record_elem = "{" , [ elem_assign { "," , elem_assign } ] , "}" ; -elem_assign = project_elem , "=" , element ; +elem_assign = elem_field_label , "=" , element ; +elem_field_label = "." , lower_ident ; -instance = for_inst | app_inst ; +(* Instances *) +instance = for_inst | case_inst | app_inst ; for_inst = "for" , param_list , "," , instance ; -app_inst = dot_inst { dot_elem } ; -dot_inst = atom_inst { project_elem } ; -atom_inst = set ":: Set" | inst_var | record_inst | "(" , instance , ")" ; +case_inst = "case" , element , "of" , "[" , [ inst_case_arm { "|" , inst_case_arm } ] , "]" ; +inst_case_arm = inject_elem , elem_var , "=>" , instance ; +app_inst = dot_inst , { dot_elem } ; +dot_inst = atom_inst , { project_elem } ; +atom_inst = set_coerce | inst_var | sig_var | record_inst | "(" , instance , ")" ; +set_coerce = set , "::" , "Set" ; record_inst = "{" , [ inst_assign { "," , inst_assign } ] , "}" ; -inst_assign = project_elem , "=" , instance ; +inst_assign = inst_field_label , "=" , instance ; +inst_field_label = "." , upper_ident ; +(* Literals *) literal = nat_lit | int_lit | float_lit | str_lit | bool_lit ; nat_lit = digit , { digit } ; int_lit = "-" , digit , { digit } ; @@ -47,6 +57,7 @@ float_lit = [ "-" ] , digit , { digit } , "." , digit , { digit } ; str_lit = '"' , { any_character_except_quote } , '"' ; bool_lit = "true" | "false" ; +(* Identifiers *) set_var = upper_ident ; sig_var = upper_ident ; elem_var = lower_ident ; @@ -60,3 +71,6 @@ upper_case_letter = "A"..."Z" ; lower_case_letter = "a"..."z" ; digit = "0"..."9" ; ident_char = upper_case_letter | lower_case_letter | digit | "_" | "'" ; + +(* Lexical *) +comment = "//" , { any_character_except_newline } , ( newline | end_of_input ) ; diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 42a581f..30598d3 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -420,18 +420,9 @@ impl CheckerState { other => (other, args.clone()), }; - let subject_sig: Option<Signature> = match &subject { - Instance::Var(v) => Some(self.lookup_instance(v)?.container.clone()), - Instance::Project { field, .. } => { - Some(self.lookup_signature_field(field)?.field.clone()) - } - // TODO: i think we need to handle case here - Instance::App { .. } - | Instance::Record(_) - | Instance::SetCoerce(_) - | Instance::For { .. } - | Instance::Case { .. } => None, - }; + // nevertheless we need the tiniest amount of bidirectionality + // here to deal with case, project, and var recursively + let subject_sig: Option<Signature> = self.stuck_subject_signature(&subject)?; if let Some(subject_sig) = subject_sig { let Signature::Ext { params, codomain } = subject_sig else { @@ -497,7 +488,7 @@ impl CheckerState { }) } Instance::Case { .. } => { - todo!("App applied to a Case instance?"); + unreachable!("_stuck_subject_signature should have dealt with this") } Instance::Var(_) | Instance::Project { .. } => { unreachable!("handled in the stuck-head branch above") @@ -533,4 +524,24 @@ impl CheckerState { .collect::<Result<Vec<_>, _>>()?; Ok((ctx, checked)) } + + fn stuck_subject_signature(&self, inst: &Instance) -> Result<Option<Signature>, CheckerError> { + match inst { + Instance::Var(v) => Ok(Some(self.lookup_instance(v)?.container.clone())), + Instance::Project { field, .. } => { + Ok(Some(self.lookup_signature_field(field)?.field.clone())) + } + // All arms of a stuck Case share a signature by the case + // elimination typing rule, and we've already expanded the body, so + // we can pick any arm. + Instance::Case { arms, .. } => self + .stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body), + + Instance::For { .. } | Instance::Record(_) | Instance::SetCoerce(_) => Ok(None), + + Instance::App { .. } => unreachable!( + "invariant violation: _stuck_head_signature called on a left-nested App" + ), + } + } } diff --git a/src/main.rs b/src/main.rs index 1925b41..2a8b274 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,59 +5,69 @@ mod checker_signature; mod checker_state; mod parser; +use std::env; +use std::fs; +use std::process; use tracing_subscriber::{layer::SubscriberExt, util::SubscriberInitExt}; use tracing_tree::HierarchicalLayer; fn main() { - tracing_subscriber::registry() - .with( - HierarchicalLayer::new(2) - .with_targets(false) - .with_bracketed_fields(true), - ) - .init(); + let args: Vec<String> = env::args().skip(1).collect(); - let src = r#" -// let signature Graph = theory { -// Vertex :: Set, -// Edge :: (s : set-of(Vertex)) (t : set-of(Vertex)) -> Set -// } + if args.is_empty() { + eprintln!("Usage: makkai [--debug] <file.makkai> [file.makkai ...]"); + process::exit(1); + } -// let set Empty = variant[] -// let set Unit = record{} -// let element pt : Unit = {} -// let set F1 = variant [ one0 : Unit ] -// let set F2 = variant [ two0 : Unit | two1 : Unit ] -// let set F3 = variant [ three0 : Unit | three1 : Unit | three2: Unit ] + let debug_mode = args.first().map_or(false, |arg| arg == "--debug"); -// let instance oneSimplex :: Graph = { -// .Vertex = F3 :: Set, -// .Edge = for (s : set-of(Vertex)) (t : set-of(Vertex)), -// case s of [ -// three0. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Unit :: Set | three2. pt => Unit :: Set ] -// | three1. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Unit :: Set ] -// | three2. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Empty :: Set ] -// ] -// } + if debug_mode { + tracing_subscriber::registry() + .with( + HierarchicalLayer::new(2) + .with_targets(false) + .with_bracketed_fields(true), + ) + .init(); + } -// let set OneSimplexEdges = record { -// source: set-of(oneSimplex .Vertex), -// target: set-of(oneSimplex .Vertex), -// connected: set-of(oneSimplex .Edge source target) -// } + let files: Vec<String> = if debug_mode { + args.into_iter().skip(1).collect() + } else { + args + }; -// let element vertex0 : F3 = three0. {} -// let element vertex1 : F3 = three1. {} -// let element edge01 : set-of(oneSimplex .Edge vertex0 vertex1) = pt + if files.is_empty() { + eprintln!("Usage: makkai [--debug] <file.makkai> [file.makkai ...]"); + process::exit(1); + } -let signature S = theory { - F :: (x : Nat) (y : Bool) -> Set, - G :: (z : set-of(F 3 5)) -> Set -} -"#; - let programme = parser::parse(src); + for file in files { + let src = match fs::read_to_string(&file) { + Ok(content) => content, + Err(e) => { + let msg = match e.kind() { + std::io::ErrorKind::NotFound => "file not found".to_string(), + _ => format!("io error: {}", e), + }; + eprintln!("{}: {}", file, msg); + process::exit(1); + } + }; + + let programme = match parser::parse_result(&src) { + Ok(p) => p, + Err(parse_err) => { + eprintln!("{}: Error\n\t{}", file, parse_err); + process::exit(1); + } + }; - if let Err(e) = programme.check() { - println!("{}", e); + if let Err(check_err) = programme.check() { + eprintln!("{} Error\n\t{}", file, check_err); + process::exit(1); + } else { + println!("{} Ok", file); + } } } diff --git a/src/parser.rs b/src/parser.rs index 285bb84..4e41644 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -269,23 +269,21 @@ parser! { } } -pub fn parse(src: &str) -> Programme { +pub fn parse_result(src: &str) -> Result<Programme, String> { match parser::program(src) { - Ok(p) => { - println!("{}", p); - p - } + Ok(p) => Ok(p), Err(e) => { let line = e.location.line; let col = e.location.column; let off = e.location.offset; - println!("FAIL at {}:{} (offset {})", line, col, off); - println!("expected: {:#}", e.expected); let before = &src[off.saturating_sub(40)..off]; let after = &src[off..(off + 40).min(src.len())]; - println!("...{}⟨HERE⟩{}...", before, after); - panic!("Parse failed!"); + + Err(format!( + "FAIL at {}:{} (offset {})\nexpected: {:#?}\n...{}⟨HERE⟩{}...", + line, col, off, e.expected, before, after + )) } } } |