From d682ad6bbb5547ffbcc19da90275ff43e4e03e20 Mon Sep 17 00:00:00 2001 From: tslil Date: Wed, 6 May 2026 14:27:43 +0100 Subject: WiP --- README.md | 4 +++ examples/equality.makkai | 18 +++++++---- src/ast.rs | 10 ++++-- src/checker.rs | 3 +- src/checker_set.rs | 37 ++++++++++++++++++--- src/checker_signature.rs | 83 ++++++++++++++++++++++++++++++++++++++++++------ src/checker_state.rs | 2 +- src/parser.rs | 66 +++++++++++++++++++------------------- 8 files changed, 164 insertions(+), 59 deletions(-) diff --git a/README.md b/README.md index 1ff5a86..dedb96d 100644 --- a/README.md +++ b/README.md @@ -90,6 +90,10 @@ 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]`. +### 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. + # 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/equality.makkai b/examples/equality.makkai index ede2a54..438e930 100644 --- a/examples/equality.makkai +++ b/examples/equality.makkai @@ -4,19 +4,25 @@ let element pt : Unit = {} let set Three = variant [ zero : Unit | one : Unit | two : Unit ] -let signature SetWitRelation = theory { +let signature SetWithEquivRelation = theory { Carrier :: Set, - Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set + Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set, + Reflexive :: (x : set-of(Carrier)) -> , + Symmetric :: (x : set-of(Carrier)) (y : set-of(Carrier)) (r : set-of(Relation x y)) -> , + Transitive :: (x : set-of(Carrier)) (y : set-of(Carrier)) (z : set-of(Carrier)) (r : set-of(Relation x y)) (s : set-of(Relation z z)) -> } -let instance eqThree :: SetWitRelation = { +let instance eqThree :: SetWithEquivRelation = { .Carrier = Three :: Set, .Relation = for (x: Three) (y: Three), case x of [ zero. z => case y of [ zero. w => Unit :: Set | one. w => Empty :: Set | two. w => Empty :: Set ] | one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ] - | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ] ] + | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ] ], + .Reflexive = for (x: Three), case x of [ zero. z => | one. z => | two. z => ], + .Symmetric = for (x: Three)(y: Three)(r: set-of(Relation x y)), , + .Transitive = for (x: Three)(y: Three)(z: Three)(r: set-of(Relation x y))(s: set-of(Relation y z)), } -let set Diagonal = record { x : set-of(eqThree .Carrier), y : set-of(eqThree .Carrier), equal : set-of((eqThree .Relation) x y) } +// let set Diagonal = record { x : set-of(eqThree .Carrier), y : set-of(eqThree .Carrier), equal : set-of((eqThree .Relation) x y) } -let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt } +// let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt } diff --git a/src/ast.rs b/src/ast.rs index e254c65..24c7125 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -68,6 +68,9 @@ pub enum Signature { #[display("Set")] Set, + #[display("⟨{_0}⟩")] + FromSet(Set), + #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::>().join(" , "))] Theory(Vec>), @@ -126,7 +129,7 @@ pub enum Element { element: Box, }, - #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] + #[display("case {scrutinee} of [ {} ]", arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] Case { scrutinee: Box, arms: Vec>, @@ -147,6 +150,9 @@ pub enum Instance { #[display("({_0} :: Set)")] SetCoerce(Box), + #[display("⟨{_0}⟩")] + ElementCoerce(Element), + #[display("{_0}")] Var(String), @@ -171,7 +177,7 @@ pub enum Instance { field: String, }, - #[display("case {} of [ {} ]", scrutinee, arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] + #[display("case {scrutinee} of [ {} ]", arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] Case { scrutinee: Box, arms: Vec>, diff --git a/src/checker.rs b/src/checker.rs index 2474bab..f94fccc 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -16,7 +16,7 @@ impl CheckerState { let Programme(decls) = prog; for decl in decls { - debug!(%decl); + print!("{decl} ... "); self.reset_binders(); match decl { Decl::Set { name, set } => { @@ -47,6 +47,7 @@ impl CheckerState { self.add_instance(name.clone(), instance.into(), signature) } }?; + println!("Ok"); } debug!(%self); Ok(()) diff --git a/src/checker_set.rs b/src/checker_set.rs index a00ea81..1a89631 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -230,7 +230,7 @@ impl CheckerState { .element; Ok(sub_element) } - _ => panic!( + Element::Inject { .. } | Element::Literal(_) => panic!( "invariant violation: check_element returned neither a record or stuck computation for record set" ), } @@ -312,7 +312,6 @@ impl CheckerState { let scrutinee = self.check_element(scrutinee, owner)?; // which variant are we, if any - let matching: Option<(String, Element)> = match scrutinee { Element::Inject { ref field, @@ -326,6 +325,18 @@ impl CheckerState { ), }; + // are we allowed to posit the equality of elements scrutinee = + // (arm.tag). (arm.bound) when looking at necessarily + // non-matching arms? + let posit_equality_with = match &scrutinee { + Element::Var(v) => Some(v.clone()), + Element::Inject { .. } + | Element::Project { .. } + | Element::Case { .. } + | Element::Literal(_) + | Element::Record(_) => None, + }; + // for each arm, recurse with a concrete value (if we have one) // otherwise fall back to hypothetical elements; in the former // case record the end result @@ -333,7 +344,8 @@ impl CheckerState { let mut processed_arms = Vec::new(); for arm in arms { let OwnedField { - field: field_set, .. + field: field_set, + owner, } = self.lookup_variant_field(&arm.tag)?; let mut ctx = self.clone(); @@ -345,7 +357,9 @@ impl CheckerState { { let canonical = ctx.make_element_definition(binding_name, inner.clone(), binding_set)?; - let output = ctx.check_element((&arm.body).into(), set)?; + let this_set = ctx.check_set(set)?; + + let output = ctx.check_element((&arm.body).into(), &this_set)?; if matches!(computed_output, Some(_)) { panic!( "invariant violation: we somehow matched multiple arms in case analysis" @@ -359,7 +373,20 @@ impl CheckerState { } } else { let canonical = ctx.make_element_binding(binding_name, binding_set)?; - let body = ctx.check_element((&arm.body).into(), set)?; + + if let Some(ref scrutinee_var) = posit_equality_with { + ctx.make_element_definition( + scrutinee_var.clone(), + Element::Inject { + field: arm.tag.clone(), + element: Box::new(Element::Var(canonical.clone())), + }, + owner.clone(), + )?; + }; + let this_set = ctx.check_set(set)?; + let body = ctx.check_element((&arm.body).into(), &this_set)?; + CaseArm { tag: arm.tag.clone(), bound: canonical, diff --git a/src/checker_signature.rs b/src/checker_signature.rs index cc6cadc..ab54fd1 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -10,6 +10,7 @@ impl CheckerState { pub fn check_signature(&self, signature: &Signature) -> Result { match signature { Signature::Set => Ok(Signature::Set), + Signature::FromSet(set) => Ok(Signature::FromSet(self.check_set(set)?)), Signature::Var(v) => { let deref = self.lookup_signature(&v)?; Ok(deref.clone()) @@ -64,6 +65,7 @@ impl CheckerState { .into_iter() .map(|Param { name, set }| { let canonical = ctx.make_element_binding(name, set.clone())?; + let set = ctx.check_set(&set)?; Ok(Param { name: canonical, set, @@ -129,6 +131,22 @@ impl CheckerState { Ok(Instance::SetCoerce(set)) } } + Instance::ElementCoerce(element) => { + if let Some(signature) = signature { + let Signature::FromSet(set) = signature else { + return Err(CheckerError::WrongSignatureForInstance { + value: instance.clone().into(), + real: Signature::FromSet(Set::Var("_".to_string())), + claimed: signature.clone(), + }); + }; + let element = self.check_element(element, set)?; + Ok(Instance::ElementCoerce(element)) + } else { + // todo!("how do we handle check_element without a set?"); + Ok(Instance::ElementCoerce(element.clone())) + } + } Instance::Var(v) => { // Exactly the same discipline as for Element::Var, see there // for some sparse comments @@ -260,7 +278,11 @@ impl CheckerState { .instance; Ok(sub_element) } - _ => panic!( + Instance::For { .. } + | Instance::ElementCoerce(_) + | Instance::SetCoerce(_) + | Instance::App { .. } + | Instance::Case { .. } => panic!( "invariant violation: check_instance returned neither a record or stuck computation for record set" ), } @@ -314,11 +336,21 @@ impl CheckerState { ), }; + let posit_equality_with = match &scrutinee { + Element::Var(v) => Some(v.clone()), + Element::Inject { .. } + | Element::Project { .. } + | Element::Case { .. } + | Element::Literal(_) + | Element::Record(_) => None, + }; + let mut computed_output = None; let mut processed_arms = Vec::new(); for arm in arms { let OwnedField { - field: field_set, .. + field: field_set, + owner, } = self.lookup_variant_field(&arm.tag)?; let mut ctx = self.clone(); @@ -330,7 +362,15 @@ impl CheckerState { { let canonical = ctx.make_element_definition(binding_name, inner.clone(), binding_set)?; - let output = ctx.check_instance((&arm.body).into(), signature)?; + let this_signature = if let Some(signature) = signature { + let signature = ctx.check_signature(signature)?; + Some(signature) + } else { + None + }; + + let output = + ctx.check_instance((&arm.body).into(), this_signature.as_ref())?; if matches!(computed_output, Some(_)) { panic!( "invariant violation: we somehow matched multiple arms in case analysis" @@ -344,7 +384,26 @@ impl CheckerState { } } else { let canonical = ctx.make_element_binding(binding_name, binding_set)?; - let body = ctx.check_instance((&arm.body).into(), signature)?; + if let Some(ref scrutinee_var) = posit_equality_with { + ctx.add_element( + scrutinee_var.clone(), + Element::Inject { + field: arm.tag.clone(), + element: Box::new(Element::Var(canonical.clone())), + } + .into(), + owner.clone(), + )?; + }; + let this_signature = if let Some(signature) = signature { + let signature = ctx.check_signature(signature)?; + Some(signature) + } else { + None + }; + + let body = + ctx.check_instance((&arm.body).into(), this_signature.as_ref())?; CaseArm { tag: arm.tag.clone(), bound: canonical, @@ -508,7 +567,7 @@ impl CheckerState { // nevertheless we need the tiniest amount of bidirectionality // here to deal with case, project, and var recursively - let subject_sig: Option = self.stuck_subject_signature(&subject)?; + let subject_sig: Option = self._stuck_subject_signature(&subject)?; if let Some(subject_sig) = subject_sig { let Signature::Ext { params, codomain } = subject_sig else { @@ -567,7 +626,7 @@ impl CheckerState { ctx.check_instance(&residual, signature) } } - Instance::Record(_) | Instance::SetCoerce(_) => { + Instance::Record(_) | Instance::SetCoerce(_) | Instance::ElementCoerce(_) => { Err(CheckerError::NonFunctionalInstance { instance: subject, elements: args, @@ -611,7 +670,7 @@ impl CheckerState { Ok((ctx, checked)) } - fn stuck_subject_signature(&self, inst: &Instance) -> Result, CheckerError> { + fn _stuck_subject_signature(&self, inst: &Instance) -> Result, CheckerError> { match inst { Instance::Var(v) => Ok(Some(self.lookup_instance(v)?.container.clone())), Instance::Project { field, .. } => { @@ -620,10 +679,14 @@ impl CheckerState { // 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), + // TODO! this is wrong! + Instance::Case { arms, .. } => self + ._stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body), + Instance::ElementCoerce(_) + | 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/checker_state.rs b/src/checker_state.rs index ad01d50..a88c6b0 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -399,7 +399,7 @@ impl CheckerState { Signature::Ext { codomain, .. } => { self._register_signature_fields(codomain, rebind)?; } - _ => (), + Signature::Var(_) | Signature::Set | Signature::FromSet(_) => (), } Ok(()) } diff --git a/src/parser.rs b/src/parser.rs index f205407..73e8dd3 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -45,12 +45,12 @@ parser! { rule kw_false() = "false" wb() rule keyword() = - kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance() - / kw_record() / kw_variant() / kw_theory() - / kw_case() / kw_of() / kw_for() - / kw_Set() / kw_set_of() / kw_set() - / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() - / kw_true() / kw_false() + kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance() + / kw_record() / kw_variant() / kw_theory() + / kw_case() / kw_of() / kw_for() + / kw_Set() / kw_set_of() / kw_set() + / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() + / kw_true() / kw_false() // ==================================================================== // Identifiers @@ -134,19 +134,20 @@ parser! { = kw_set_of() _ "(" _ i:instance() _ ")" { i } rule set() -> Set - = kw_record() _ "{" _ fs:(set_field() ** ",") _ "}" { Set::Record(fs) } - / kw_variant() _ "[" _ vs:(variant_field() ** "|") _ "]" { Set::Variant(vs) } - / b:builtin() { Set::BuiltIn(b) } - / i:claimed_set() { Set::ClaimedSet(i) } - / v:set_var() { Set::Var(v) } - / "(" _ s:set() _ ")" { s } + = kw_record() _ "{" _ fs:(set_field() ** ",") _ "}" { Set::Record(fs) } + / kw_variant() _ "[" _ vs:(variant_field() ** "|") _ "]" { Set::Variant(vs) } + / b:builtin() { Set::BuiltIn(b) } + / i:claimed_set() { Set::ClaimedSet(i) } + / v:set_var() { Set::Var(v) } + / "(" _ s:set() _ ")" { s } // ==================================================================== // Signatures // ==================================================================== rule param() -> Param - = "(" _ n:elem_var() _ ":" _ s:set() _ ")" { Param { name: n, set: s } } + = "(" _ n:elem_var() _ ":" _ s:set() _ ")" + { Param { name: n, set: s } } rule param_list() -> Vec = param() ++ _ @@ -168,11 +169,12 @@ parser! { } rule signature() -> Signature - = kw_Set() { Signature::Set } - / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } - / s:sig_ext() { s } - / v:sig_var() { Signature::Var(v) } - / "(" _ s:signature() _ ")" { s } + = kw_Set() { Signature::Set } + / "<" _ s:set() _ ">" { Signature::FromSet(s) } + / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } + / s:sig_ext() { s } + / v:sig_var() { Signature::Var(v) } + / "(" _ s:signature() _ ")" { s } // ==================================================================== // Elements @@ -204,9 +206,8 @@ parser! { { CaseArm { tag: t, bound: x, body } } rule element() -> Element - = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" - { Element::Case { scrutinee: Box::new(scrut), arms } } - / d:dot_elem() { d } + = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } + / d:dot_elem() { d } // ==================================================================== // Instances @@ -221,10 +222,12 @@ parser! { { InstAssign { name: n, instance: i } } rule explicit_set_coerce() -> Set - = s:set() _ "::" _ kw_Set() { s } + = s:set() _ "::" _ kw_Set() + { s } rule atom_inst() -> Instance = s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) } + / "<" _ e:element() _ ">" { Instance::ElementCoerce(e) } / v:inst_var() { Instance::Var(v) } / f:sig_var() { Instance::Var(f) } / "{" _ fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) } @@ -269,24 +272,19 @@ parser! { } rule instance() -> Instance - = i:inst_for() { i } - / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" - { Instance::Case { scrutinee: Box::new(scrut), arms } } - / app_inst() + = i:inst_for() { i } + / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" { Instance::Case { scrutinee: Box::new(scrut), arms } } + / a:app_inst() { a } // ==================================================================== // Top-level declarations // ==================================================================== rule decl() -> Decl - = kw_let_set() _ n:set_var() _ "=" _ s:set() - { Decl::Set { name: n, set: s } } - / kw_let_element() _ n:elem_var() _ ":" _ s:set() _ "=" _ e:element() - { Decl::Element { name: n, set: s, element: e } } - / kw_let_signature() _ n:sig_var() _ "=" _ sg:signature() - { Decl::Signature { name: n, signature: sg } } - / kw_let_instance() _ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance() - { Decl::Instance { name: n, signature: sg, instance: i } } + = kw_let_set() _ n:set_var() _ "=" _ s:set() { Decl::Set { name: n, set: s } } + / kw_let_element() _ n:elem_var() _ ":" _ s:set() _ "=" _ e:element() { Decl::Element { name: n, set: s, element: e } } + / kw_let_signature() _ n:sig_var() _ "=" _ sg:signature() { Decl::Signature { name: n, signature: sg } } + / kw_let_instance() _ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance() { Decl::Instance { name: n, signature: sg, instance: i } } pub rule program() -> Programme = _ ds:(decl() ** _) _ { Programme(ds) } -- cgit v1.3.1