diff options
| -rw-r--r-- | README.md | 25 | ||||
| -rw-r--r-- | examples/equality.makkai | 30 | ||||
| -rw-r--r-- | src/ast.rs | 3 | ||||
| -rw-r--r-- | src/checker_set.rs | 30 | ||||
| -rw-r--r-- | src/checker_signature.rs | 8 | ||||
| -rw-r--r-- | src/parser.rs | 12 |
6 files changed, 85 insertions, 23 deletions
@@ -23,7 +23,7 @@ Note: the checker does not presently support η-equivalence in all cases and so ### 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`. +- `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`. @@ -52,11 +52,11 @@ For each `B ∈ { Nat, Int, Float, Str }`: - **η.** `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 { ... }`. +- **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 @@ -87,13 +87,22 @@ For each `B ∈ { Nat, Int, Float, Str }`: #### 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]`. +- **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. diff --git a/examples/equality.makkai b/examples/equality.makkai index 5e9a0f9..86b81ae 100644 --- a/examples/equality.makkai +++ b/examples/equality.makkai @@ -1,9 +1,11 @@ +// basic prelude let set Empty = variant[] let set Unit = record {} let element pt : Unit = {} - +// Bool is not inductive let set Two = variant [ zero : Unit | one : Unit] +// the main thrust let signature SetWithEquivRelation = theory { Carrier :: Set, Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set, @@ -15,6 +17,8 @@ let signature SetWithEquivRelation = theory { -> <set-of(Relation x z)> } + +// by cases we construct this on Two let instance eqTwo :: SetWithEquivRelation = { .Carrier = Two :: Set, .Relation = for (x: Two) (y: Two), @@ -25,7 +29,7 @@ let instance eqTwo :: SetWithEquivRelation = { case x of [ zero. _ => case y of [ zero. _ => <r> | one. _ => <r> ] | one. _ => case y of [ zero. _ => <r> | one. _ => <r> ] ], .Transitive = for (x: Two)(y: Two)(z: Two)(r: set-of(Relation x y))(s: set-of(Relation y z)), - case x of [ zero. _ => case y of + case x of [ zero. _ => case y of // there are choices here to use <r> or <s> in places that are irrelevant [ zero. _ => case z of [ zero. _ => <r> | one. _ => <s> ] | one. _ => case z of [ zero. _ => <pt>| one. _ => <r> ] ] | one. _ => case y of @@ -33,6 +37,26 @@ let instance eqTwo :: SetWithEquivRelation = { | one. _ => case z of [ zero. _ => <s> | one. _ => <r> ] ] ] } +// show off forming sets let set Diagonal = record { x : set-of(eqTwo .Carrier), y : set-of(eqTwo .Carrier), equal : set-of((eqTwo .Relation) x y) } - let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt } + +// prove inequality +let instance zeroNeqOne + :: (r : set-of((eqTwo .Relation) (zero. pt) (one. pt))) -> <Empty> + = for (r : set-of((eqTwo .Relation) (zero. pt) (one. pt))), <r> + +// prove inequality the fun way +let signature NeqParticular = theory { + SE :: SetWithEquivRelation, + A :: <set-of(SE .Carrier)>, + B :: <set-of(SE .Carrier)>, + Neq :: (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))) -> <Empty> +} + +let instance zeroNeqOne :: NeqParticular = { + .SE = eqTwo, + .A = <zero. pt>, + .B = <one. pt>, + .Neq = for (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))), <r> +} @@ -108,6 +108,9 @@ pub struct ElemAssign { #[derive(Clone, PartialEq, Display, Debug)] pub enum Element { + #[display{"element-of({_0})"}] + ClaimedElement(Box<Instance>), + #[display("{_0}")] Literal(Literal), diff --git a/src/checker_set.rs b/src/checker_set.rs index f13f686..2f934e2 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -120,6 +120,17 @@ impl CheckerState { } Ok(element.clone().into()) } + Element::ClaimedElement(instance) => { + let instance = self.check_instance( + instance.as_ref(), + set.map(|s| Signature::FromSet(s.clone())).as_ref(), + )?; + if let Instance::ElementCoerce(element) = instance { + Ok(element) + } else { + Ok(Element::ClaimedElement(Box::new(instance))) + } + } Element::Var(v) => { let lookup = self.lookup_element(&v)?; @@ -275,12 +286,13 @@ impl CheckerState { match inner { // We're stuck on something that bottoms out in a binding // blocking computation, nothing to be done here - Element::Var(_) | Element::Project { .. } | Element::Case { .. } => { - Ok(Element::Project { - element: Box::new(inner), - field: field.clone(), - }) - } + Element::Var(_) + | Element::Project { .. } + | Element::Case { .. } + | Element::ClaimedElement(_) => Ok(Element::Project { + element: Box::new(inner), + field: field.clone(), + }), Element::Record(assignations) => { let sub_element = assignations .into_iter() @@ -382,7 +394,10 @@ impl CheckerState { } => Some((field.clone(), *inner.clone())), // These are all the cases which could become stuck on a // formal binding - Element::Var(_) | Element::Project { .. } | Element::Case { .. } => None, + Element::Var(_) + | Element::Project { .. } + | Element::Case { .. } + | Element::ClaimedElement(_) => None, Element::Literal(_) | Element::Record(_) => panic!( "invariant violation: scrutinee is a non-variant value at variant set" ), @@ -394,6 +409,7 @@ impl CheckerState { let posit_equality_with = match &scrutinee { Element::Var(v) => Some(v.clone()), Element::Inject { .. } + | Element::ClaimedElement(_) | Element::Project { .. } | Element::Case { .. } | Element::Literal(_) diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 1ce8bc8..6acd271 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -336,7 +336,10 @@ impl CheckerState { ref field, element: ref inner, } => Some((field.clone(), *inner.clone())), - Element::Var(_) | Element::Project { .. } | Element::Case { .. } => None, + Element::ClaimedElement(_) + | Element::Var(_) + | Element::Project { .. } + | Element::Case { .. } => None, Element::Literal(_) | Element::Record(_) => panic!( "invariant violation: scrutinee is a non-variant value at variant set" ), @@ -344,7 +347,8 @@ impl CheckerState { let posit_equality_with = match &scrutinee { Element::Var(v) => Some(v.clone()), - Element::Inject { .. } + Element::ClaimedElement(_) + | Element::Inject { .. } | Element::Project { .. } | Element::Case { .. } | Element::Literal(_) diff --git a/src/parser.rs b/src/parser.rs index 8dbc31e..6ab5900 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -32,6 +32,7 @@ parser! { rule kw_theory() = "theory" wb() rule kw_case() = "case" wb() rule kw_of() = "of" wb() + rule kw_element_of() = "element-of" wb() rule kw_for() = "for" wb() rule kw_set() = "set" wb() rule kw_set_of() = "set-of" wb() @@ -48,8 +49,8 @@ parser! { 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_Set() / kw_set_of() / kw_set() / kw_element_of() + / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() / kw_true() / kw_false() // ==================================================================== @@ -205,8 +206,13 @@ parser! { = _ t:inject() _ x:elem_var() _ "=>" _ body:element() _ { CaseArm { tag: t, bound: x, body } } + rule claimed_element() -> Instance + = kw_element_of() _ "(" _ i:instance() _ ")" { i } + + rule element() -> Element - = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } + = i:claimed_element() { Element::ClaimedElement(Box::new(i)) } + / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } / d:dot_elem() { d } // ==================================================================== |