Inductive Types
Inductive types form the foundation of data structures in the Calculus of Constructions, providing a systematic way to define recursive types with constructors and elimination principles. Our implementation supports universe-polymorphic inductive types with dependent pattern matching, enabling data type abstractions while maintaining logical consistency through the universe hierarchy.
Inductive types represent a crucial extension to the pure lambda calculus, allowing the definition of concrete data structures like natural numbers, lists, and trees through constructor-based specifications. The implementation provides both syntactic support for inductive declarations and semantic handling through specialized type checking algorithms that ensure constructor consistency and exhaustive pattern coverage.
Consider these intuitive examples that demonstrate the fundamental concept of inductive types. A simple enumeration like the days of the week can be expressed as an inductive type with seven constructors:
inductive DayOfWeek : Type with
| Monday : DayOfWeek
| Tuesday : DayOfWeek
| Wednesday : DayOfWeek
| Thursday : DayOfWeek
| Friday : DayOfWeek
| Saturday : DayOfWeek
| Sunday : DayOfWeek
Similarly, primary colors form another natural inductive type with three distinct constructors:
inductive Color : Type with
| Red : Color
| Green : Color
| Blue : Color
These examples illustrate how inductive types provide a systematic way to define finite sets of distinct values through constructor declarations, with each constructor serving as both a data constructor and a proof that the constructed value belongs to the inductive type.
More complex inductive types can include recursive constructors that reference the type being defined, enabling data structures like binary trees:
inductive BinaryTree (A : Type) : Type with
| Leaf : BinaryTree A
| Node : A -> BinaryTree A -> BinaryTree A -> BinaryTree A
This binary tree definition demonstrates several important concepts: the type is parameterized by an element type A, the Leaf constructor creates empty trees, and the Node constructor takes a value of type A along with two subtrees to create larger trees. The recursive nature of the Node constructor enables the construction of arbitrarily deep tree structures while maintaining type safety through the inductive type system.
Inductive Type Declarations
The core data structure for inductive type declarations captures all the essential components needed for constructor-based type definitions:
#![allow(unused)] fn main() { use std::fmt; /// Core terms in the Calculus of Constructions #[derive(Debug, Clone, PartialEq)] pub enum Term { /// Variables: x, y, z Var(String), /// Application: f a App(Box<Term>, Box<Term>), /// Lambda abstraction: λ x : A, t (written as fun x : A => t) Abs(String, Box<Term>, Box<Term>), /// Dependent product: Π x : A, B (written as (x : A) → B or {x : A} → B) Pi(String, Box<Term>, Box<Term>, bool), // bool = implicit /// Sort/Type: Sort u, Type, Prop Sort(Universe), /// Let binding: let x := t in s Let(String, Box<Term>, Box<Term>, Box<Term>), /// Match expression with patterns Match(Box<Term>, Vec<MatchArm>), /// Inductive type constructor Constructor(String, Vec<Term>), /// Local constant (for definitions and axioms) Const(String), /// Meta-variable for type inference Meta(String), /// Field projection: term.field Proj(Box<Term>, String), /// Dependent pair type (Sigma type): Σ (x : A), B Sigma(String, Box<Term>, Box<Term>), /// Pair constructor: ⟨a, b⟩ Pair(Box<Term>, Box<Term>), /// First projection: π₁ Fst(Box<Term>), /// Second projection: π₂ Snd(Box<Term>), } /// Universe levels for type theory #[derive(Debug, Clone, PartialEq, Eq)] pub enum Universe { Const(u32), // Concrete level: 0, 1, 2, ... ScopedVar(String, String), // Scoped universe variable: (scope_name, var_name) Meta(u32), // Universe metavariable: ?u₀, ?u₁, ... Add(Box<Universe>, u32), // Level + n Max(Box<Universe>, Box<Universe>), // max(u, v) IMax(Box<Universe>, Box<Universe>), // imax(u, v) } /// Universe level constraints for polymorphism #[derive(Debug, Clone, PartialEq, Eq)] pub enum UniverseConstraint { /// u ≤ v LessEq(Universe, Universe), /// u = v Equal(Universe, Universe), } /// Context for universe level variables #[derive(Debug, Clone, PartialEq)] pub struct UniverseContext { /// Currently bound universe variables pub variables: Vec<String>, /// Constraints on universe levels pub constraints: Vec<UniverseConstraint>, } /// Pattern matching arms #[derive(Debug, Clone, PartialEq)] pub struct MatchArm { pub pattern: Pattern, pub body: Term, } /// Patterns for match expressions #[derive(Debug, Clone, PartialEq)] pub enum Pattern { /// Variable pattern: x Var(String), /// Constructor pattern: Cons x xs Constructor(String, Vec<Pattern>), /// Wildcard pattern: _ Wildcard, } /// Function parameters #[derive(Debug, Clone, PartialEq)] pub struct Parameter { pub name: String, pub ty: Term, pub implicit: bool, // for {x : A} vs (x : A) } /// Constructor for inductive types #[derive(Debug, Clone, PartialEq)] pub struct Constructor { pub name: String, pub ty: Term, } /// Structure fields #[derive(Debug, Clone, PartialEq)] pub struct Field { pub name: String, pub ty: Term, } /// Module containing multiple declarations #[derive(Debug, Clone, PartialEq)] pub struct Module { pub declarations: Vec<Declaration>, } impl fmt::Display for Universe { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Universe::Const(n) => write!(f, "{}", n), Universe::ScopedVar(scope, var) => write!(f, "{}::{}", scope, var), Universe::Meta(id) => write!(f, "?u{}", id), Universe::Add(u, n) => write!(f, "{}+{}", u, n), Universe::Max(u, v) => write!(f, "max({}, {})", u, v), Universe::IMax(u, v) => write!(f, "imax({}, {})", u, v), } } } impl fmt::Display for Term { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Term::Var(x) => write!(f, "{}", x), Term::App(t1, t2) => write!(f, "({} {})", t1, t2), Term::Abs(x, ty, body) => write!(f, "(fun {} : {} => {})", x, ty, body), Term::Pi(x, ty, body, implicit) => { if Self::occurs_free(x, body) { if *implicit { write!(f, "{{{} : {}}} → {}", x, ty, body) } else { write!(f, "({} : {}) → {}", x, ty, body) } } else { write!(f, "{} → {}", ty, body) } } Term::Sort(u) => match u { Universe::Const(0) => write!(f, "Prop"), Universe::Const(n) => { if *n == 1 { write!(f, "Type") } else { write!(f, "Type {}", n - 1) } } Universe::Add(ref base, n) => { if let Universe::Const(1) = **base { write!(f, "Type {}", n) } else { write!(f, "Sort {}", u) } } _ => write!(f, "Sort {}", u), }, Term::Let(x, ty, val, body) => write!(f, "(let {} : {} := {} in {})", x, ty, val, body), Term::Match(scrutinee, arms) => { writeln!(f, "match {} with", scrutinee)?; for arm in arms { writeln!(f, "| {} => {}", arm.pattern, arm.body)?; } Ok(()) } Term::Constructor(name, args) => { write!(f, "{}", name)?; for arg in args { write!(f, " {}", arg)?; } Ok(()) } Term::Const(name) => write!(f, "{}", name), Term::Meta(name) => write!(f, "?{}", name), Term::Proj(term, field) => write!(f, "{}.{}", term, field), Term::Sigma(x, domain, codomain) => write!(f, "Σ ({} : {}), {}", x, domain, codomain), Term::Pair(fst, snd) => write!(f, "⟨{}, {}⟩", fst, snd), Term::Fst(pair) => write!(f, "π₁({})", pair), Term::Snd(pair) => write!(f, "π₂({})", pair), } } } impl fmt::Display for Pattern { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Pattern::Var(x) => write!(f, "{}", x), Pattern::Constructor(name, args) => { write!(f, "{}", name)?; for arg in args { write!(f, " {}", arg)?; } Ok(()) } Pattern::Wildcard => write!(f, "_"), } } } impl Term { /// Check if variable occurs free in term pub fn occurs_free(var: &str, term: &Term) -> bool { match term { Term::Var(x) => x == var, Term::App(t1, t2) => Self::occurs_free(var, t1) || Self::occurs_free(var, t2), Term::Abs(x, ty, body) => { Self::occurs_free(var, ty) || (x != var && Self::occurs_free(var, body)) } Term::Pi(x, ty, body, _) => { Self::occurs_free(var, ty) || (x != var && Self::occurs_free(var, body)) } Term::Sort(_) => false, Term::Let(x, ty, val, body) => { Self::occurs_free(var, ty) || Self::occurs_free(var, val) || (x != var && Self::occurs_free(var, body)) } Term::Match(scrutinee, arms) => { Self::occurs_free(var, scrutinee) || arms.iter().any(|arm| Self::occurs_free(var, &arm.body)) } Term::Constructor(_, args) => args.iter().any(|arg| Self::occurs_free(var, arg)), Term::Const(_) => false, Term::Meta(_) => false, Term::Proj(term, _) => Self::occurs_free(var, term), Term::Sigma(x, domain, codomain) => { Self::occurs_free(var, domain) || (x != var && Self::occurs_free(var, codomain)) } Term::Pair(fst, snd) => Self::occurs_free(var, fst) || Self::occurs_free(var, snd), Term::Fst(pair) | Term::Snd(pair) => Self::occurs_free(var, pair), } } } impl UniverseContext { pub fn new() -> Self { UniverseContext { variables: Vec::new(), constraints: Vec::new(), } } /// Add a universe variable to the context pub fn add_var(&mut self, name: String) { if !self.variables.contains(&name) { self.variables.push(name); } } /// Add a constraint to the context pub fn add_constraint(&mut self, constraint: UniverseConstraint) { self.constraints.push(constraint); } /// Check if a universe variable is bound in this context pub fn contains(&self, name: &str) -> bool { self.variables.contains(&name.to_string()) } /// Extend context with variables from another context pub fn extend(&self, other: &UniverseContext) -> Self { let mut new_ctx = self.clone(); for var in &other.variables { new_ctx.add_var(var.clone()); } for constraint in &other.constraints { new_ctx.add_constraint(constraint.clone()); } new_ctx } /// Generate a fresh universe variable name pub fn fresh_var(&self, base: &str) -> String { let mut counter = 0; loop { let name = if counter == 0 { base.to_string() } else { format!("{}{}", base, counter) }; if !self.contains(&name) { return name; } counter += 1; } } } impl Default for UniverseContext { fn default() -> Self { Self::new() } } impl Universe { /// Create a scoped universe variable pub fn scoped_var(scope: String, name: String) -> Self { Universe::ScopedVar(scope, name) } } /// Top-level declarations #[derive(Debug, Clone, PartialEq)] pub enum Declaration { /// Constant definition: def name {u...} (params) : type := body Definition { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, body: Term, }, /// Axiom: axiom name {u...} : type Axiom { name: String, universe_params: Vec<String>, // Universe level parameters ty: Term, }, /// Inductive type: inductive Name {u...} (params) : Type := constructors Inductive { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, constructors: Vec<Constructor>, }, /// Structure (single constructor inductive): structure Name {u...} := /// (fields) Structure { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, fields: Vec<Field>, }, } }
Inductive declarations specify a type name, optional universe parameters for universe polymorphism, type parameters for generic types, a result type specification, and a collection of constructor definitions. This structure enables complex inductive types ranging from simple enumerations to universe-polymorphic families of types.
#![allow(unused)] fn main() { use std::fmt; /// Core terms in the Calculus of Constructions #[derive(Debug, Clone, PartialEq)] pub enum Term { /// Variables: x, y, z Var(String), /// Application: f a App(Box<Term>, Box<Term>), /// Lambda abstraction: λ x : A, t (written as fun x : A => t) Abs(String, Box<Term>, Box<Term>), /// Dependent product: Π x : A, B (written as (x : A) → B or {x : A} → B) Pi(String, Box<Term>, Box<Term>, bool), // bool = implicit /// Sort/Type: Sort u, Type, Prop Sort(Universe), /// Let binding: let x := t in s Let(String, Box<Term>, Box<Term>, Box<Term>), /// Match expression with patterns Match(Box<Term>, Vec<MatchArm>), /// Inductive type constructor Constructor(String, Vec<Term>), /// Local constant (for definitions and axioms) Const(String), /// Meta-variable for type inference Meta(String), /// Field projection: term.field Proj(Box<Term>, String), /// Dependent pair type (Sigma type): Σ (x : A), B Sigma(String, Box<Term>, Box<Term>), /// Pair constructor: ⟨a, b⟩ Pair(Box<Term>, Box<Term>), /// First projection: π₁ Fst(Box<Term>), /// Second projection: π₂ Snd(Box<Term>), } /// Universe levels for type theory #[derive(Debug, Clone, PartialEq, Eq)] pub enum Universe { Const(u32), // Concrete level: 0, 1, 2, ... ScopedVar(String, String), // Scoped universe variable: (scope_name, var_name) Meta(u32), // Universe metavariable: ?u₀, ?u₁, ... Add(Box<Universe>, u32), // Level + n Max(Box<Universe>, Box<Universe>), // max(u, v) IMax(Box<Universe>, Box<Universe>), // imax(u, v) } /// Universe level constraints for polymorphism #[derive(Debug, Clone, PartialEq, Eq)] pub enum UniverseConstraint { /// u ≤ v LessEq(Universe, Universe), /// u = v Equal(Universe, Universe), } /// Context for universe level variables #[derive(Debug, Clone, PartialEq)] pub struct UniverseContext { /// Currently bound universe variables pub variables: Vec<String>, /// Constraints on universe levels pub constraints: Vec<UniverseConstraint>, } /// Pattern matching arms #[derive(Debug, Clone, PartialEq)] pub struct MatchArm { pub pattern: Pattern, pub body: Term, } /// Patterns for match expressions #[derive(Debug, Clone, PartialEq)] pub enum Pattern { /// Variable pattern: x Var(String), /// Constructor pattern: Cons x xs Constructor(String, Vec<Pattern>), /// Wildcard pattern: _ Wildcard, } /// Top-level declarations #[derive(Debug, Clone, PartialEq)] pub enum Declaration { /// Constant definition: def name {u...} (params) : type := body Definition { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, body: Term, }, /// Axiom: axiom name {u...} : type Axiom { name: String, universe_params: Vec<String>, // Universe level parameters ty: Term, }, /// Inductive type: inductive Name {u...} (params) : Type := constructors Inductive { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, constructors: Vec<Constructor>, }, /// Structure (single constructor inductive): structure Name {u...} := /// (fields) Structure { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, fields: Vec<Field>, }, } /// Function parameters #[derive(Debug, Clone, PartialEq)] pub struct Parameter { pub name: String, pub ty: Term, pub implicit: bool, // for {x : A} vs (x : A) } /// Structure fields #[derive(Debug, Clone, PartialEq)] pub struct Field { pub name: String, pub ty: Term, } /// Module containing multiple declarations #[derive(Debug, Clone, PartialEq)] pub struct Module { pub declarations: Vec<Declaration>, } impl fmt::Display for Universe { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Universe::Const(n) => write!(f, "{}", n), Universe::ScopedVar(scope, var) => write!(f, "{}::{}", scope, var), Universe::Meta(id) => write!(f, "?u{}", id), Universe::Add(u, n) => write!(f, "{}+{}", u, n), Universe::Max(u, v) => write!(f, "max({}, {})", u, v), Universe::IMax(u, v) => write!(f, "imax({}, {})", u, v), } } } impl fmt::Display for Term { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Term::Var(x) => write!(f, "{}", x), Term::App(t1, t2) => write!(f, "({} {})", t1, t2), Term::Abs(x, ty, body) => write!(f, "(fun {} : {} => {})", x, ty, body), Term::Pi(x, ty, body, implicit) => { if Self::occurs_free(x, body) { if *implicit { write!(f, "{{{} : {}}} → {}", x, ty, body) } else { write!(f, "({} : {}) → {}", x, ty, body) } } else { write!(f, "{} → {}", ty, body) } } Term::Sort(u) => match u { Universe::Const(0) => write!(f, "Prop"), Universe::Const(n) => { if *n == 1 { write!(f, "Type") } else { write!(f, "Type {}", n - 1) } } Universe::Add(ref base, n) => { if let Universe::Const(1) = **base { write!(f, "Type {}", n) } else { write!(f, "Sort {}", u) } } _ => write!(f, "Sort {}", u), }, Term::Let(x, ty, val, body) => write!(f, "(let {} : {} := {} in {})", x, ty, val, body), Term::Match(scrutinee, arms) => { writeln!(f, "match {} with", scrutinee)?; for arm in arms { writeln!(f, "| {} => {}", arm.pattern, arm.body)?; } Ok(()) } Term::Constructor(name, args) => { write!(f, "{}", name)?; for arg in args { write!(f, " {}", arg)?; } Ok(()) } Term::Const(name) => write!(f, "{}", name), Term::Meta(name) => write!(f, "?{}", name), Term::Proj(term, field) => write!(f, "{}.{}", term, field), Term::Sigma(x, domain, codomain) => write!(f, "Σ ({} : {}), {}", x, domain, codomain), Term::Pair(fst, snd) => write!(f, "⟨{}, {}⟩", fst, snd), Term::Fst(pair) => write!(f, "π₁({})", pair), Term::Snd(pair) => write!(f, "π₂({})", pair), } } } impl fmt::Display for Pattern { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Pattern::Var(x) => write!(f, "{}", x), Pattern::Constructor(name, args) => { write!(f, "{}", name)?; for arg in args { write!(f, " {}", arg)?; } Ok(()) } Pattern::Wildcard => write!(f, "_"), } } } impl Term { /// Check if variable occurs free in term pub fn occurs_free(var: &str, term: &Term) -> bool { match term { Term::Var(x) => x == var, Term::App(t1, t2) => Self::occurs_free(var, t1) || Self::occurs_free(var, t2), Term::Abs(x, ty, body) => { Self::occurs_free(var, ty) || (x != var && Self::occurs_free(var, body)) } Term::Pi(x, ty, body, _) => { Self::occurs_free(var, ty) || (x != var && Self::occurs_free(var, body)) } Term::Sort(_) => false, Term::Let(x, ty, val, body) => { Self::occurs_free(var, ty) || Self::occurs_free(var, val) || (x != var && Self::occurs_free(var, body)) } Term::Match(scrutinee, arms) => { Self::occurs_free(var, scrutinee) || arms.iter().any(|arm| Self::occurs_free(var, &arm.body)) } Term::Constructor(_, args) => args.iter().any(|arg| Self::occurs_free(var, arg)), Term::Const(_) => false, Term::Meta(_) => false, Term::Proj(term, _) => Self::occurs_free(var, term), Term::Sigma(x, domain, codomain) => { Self::occurs_free(var, domain) || (x != var && Self::occurs_free(var, codomain)) } Term::Pair(fst, snd) => Self::occurs_free(var, fst) || Self::occurs_free(var, snd), Term::Fst(pair) | Term::Snd(pair) => Self::occurs_free(var, pair), } } } impl UniverseContext { pub fn new() -> Self { UniverseContext { variables: Vec::new(), constraints: Vec::new(), } } /// Add a universe variable to the context pub fn add_var(&mut self, name: String) { if !self.variables.contains(&name) { self.variables.push(name); } } /// Add a constraint to the context pub fn add_constraint(&mut self, constraint: UniverseConstraint) { self.constraints.push(constraint); } /// Check if a universe variable is bound in this context pub fn contains(&self, name: &str) -> bool { self.variables.contains(&name.to_string()) } /// Extend context with variables from another context pub fn extend(&self, other: &UniverseContext) -> Self { let mut new_ctx = self.clone(); for var in &other.variables { new_ctx.add_var(var.clone()); } for constraint in &other.constraints { new_ctx.add_constraint(constraint.clone()); } new_ctx } /// Generate a fresh universe variable name pub fn fresh_var(&self, base: &str) -> String { let mut counter = 0; loop { let name = if counter == 0 { base.to_string() } else { format!("{}{}", base, counter) }; if !self.contains(&name) { return name; } counter += 1; } } } impl Default for UniverseContext { fn default() -> Self { Self::new() } } impl Universe { /// Create a scoped universe variable pub fn scoped_var(scope: String, name: String) -> Self { Universe::ScopedVar(scope, name) } } /// Constructor for inductive types #[derive(Debug, Clone, PartialEq)] pub struct Constructor { pub name: String, pub ty: Term, } }
Constructor definitions associate names with their type signatures, enabling the type checker to verify that constructor applications respect the declared interfaces. Each constructor must produce a value of the inductive type it belongs to, maintaining the logical coherence of the type system.
Constructor Type Specialization
When inductive types include parameters, constructor types must be specialized appropriately for each use context:
#![allow(unused)] fn main() { /// Specialize a constructor type by instantiating type parameters to match /// expected type fn specialize_constructor_type( &mut self, ctor_type: &Term, expected_type: &Term, _ctx: &Context, ) -> TypeResult<Term> { // For a constructor like nil : (A : Type) → List A // and expected type List B, we need to instantiate A with B let mut current_type = ctor_type.clone(); let mut substitutions = Vec::new(); // Collect all type parameters (Pi types where domain is Type) while let Term::Pi(param_name, param_ty, body, _implicit) = ¤t_type { if matches!(param_ty.as_ref(), Term::Sort(_)) { // This is a type parameter // We'll need to figure out what to substitute for it substitutions.push(param_name.clone()); current_type = body.as_ref().clone(); } else { break; } } // Now current_type should be the return type with free variables if substitutions.is_empty() { // No type parameters, just return the original type return Ok(ctor_type.clone()); } // Handle type parameter substitution if !substitutions.is_empty() { // Extract type arguments from expected_type let mut type_args = Vec::new(); let mut current_expected = expected_type; // For types like Pair A B, we need to extract both A and B while let Term::App(f, arg) = current_expected { type_args.push(arg.as_ref().clone()); current_expected = f; } type_args.reverse(); // Apply substitutions let mut specialized = ctor_type.clone(); for (param, arg) in substitutions.iter().zip(type_args.iter()) { // Skip the Pi binding for this parameter and substitute in the body if let Term::Pi(p, _, body, _) = &specialized { if p == param { specialized = self.substitute(param, arg, body); } } } return Ok(specialized); } // For more complex cases, would need proper unification Ok(ctor_type.clone()) } }
Constructor specialization handles the complex process of instantiating generic constructor types with specific type arguments. The algorithm traverses constructor type signatures and replaces type parameters with concrete arguments while preserving the constructor’s structural properties. This process enables generic inductive types like List A to work correctly when instantiated with specific element types.
The specialization process maintains universe polymorphism by properly handling universe parameters in constructor types. When a constructor belongs to a universe-polymorphic inductive type, the specialization algorithm ensures that universe constraints are preserved throughout the instantiation process.
Pattern Matching Implementation
Pattern matching provides the elimination principle for inductive types, allowing programs to analyze inductive values by case analysis:
#![allow(unused)] fn main() { use std::fmt; /// Core terms in the Calculus of Constructions #[derive(Debug, Clone, PartialEq)] pub enum Term { /// Variables: x, y, z Var(String), /// Application: f a App(Box<Term>, Box<Term>), /// Lambda abstraction: λ x : A, t (written as fun x : A => t) Abs(String, Box<Term>, Box<Term>), /// Dependent product: Π x : A, B (written as (x : A) → B or {x : A} → B) Pi(String, Box<Term>, Box<Term>, bool), // bool = implicit /// Sort/Type: Sort u, Type, Prop Sort(Universe), /// Let binding: let x := t in s Let(String, Box<Term>, Box<Term>, Box<Term>), /// Match expression with patterns Match(Box<Term>, Vec<MatchArm>), /// Inductive type constructor Constructor(String, Vec<Term>), /// Local constant (for definitions and axioms) Const(String), /// Meta-variable for type inference Meta(String), /// Field projection: term.field Proj(Box<Term>, String), /// Dependent pair type (Sigma type): Σ (x : A), B Sigma(String, Box<Term>, Box<Term>), /// Pair constructor: ⟨a, b⟩ Pair(Box<Term>, Box<Term>), /// First projection: π₁ Fst(Box<Term>), /// Second projection: π₂ Snd(Box<Term>), } /// Universe levels for type theory #[derive(Debug, Clone, PartialEq, Eq)] pub enum Universe { Const(u32), // Concrete level: 0, 1, 2, ... ScopedVar(String, String), // Scoped universe variable: (scope_name, var_name) Meta(u32), // Universe metavariable: ?u₀, ?u₁, ... Add(Box<Universe>, u32), // Level + n Max(Box<Universe>, Box<Universe>), // max(u, v) IMax(Box<Universe>, Box<Universe>), // imax(u, v) } /// Universe level constraints for polymorphism #[derive(Debug, Clone, PartialEq, Eq)] pub enum UniverseConstraint { /// u ≤ v LessEq(Universe, Universe), /// u = v Equal(Universe, Universe), } /// Context for universe level variables #[derive(Debug, Clone, PartialEq)] pub struct UniverseContext { /// Currently bound universe variables pub variables: Vec<String>, /// Constraints on universe levels pub constraints: Vec<UniverseConstraint>, } /// Pattern matching arms #[derive(Debug, Clone, PartialEq)] pub struct MatchArm { pub pattern: Pattern, pub body: Term, } /// Top-level declarations #[derive(Debug, Clone, PartialEq)] pub enum Declaration { /// Constant definition: def name {u...} (params) : type := body Definition { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, body: Term, }, /// Axiom: axiom name {u...} : type Axiom { name: String, universe_params: Vec<String>, // Universe level parameters ty: Term, }, /// Inductive type: inductive Name {u...} (params) : Type := constructors Inductive { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, constructors: Vec<Constructor>, }, /// Structure (single constructor inductive): structure Name {u...} := /// (fields) Structure { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, fields: Vec<Field>, }, } /// Function parameters #[derive(Debug, Clone, PartialEq)] pub struct Parameter { pub name: String, pub ty: Term, pub implicit: bool, // for {x : A} vs (x : A) } /// Constructor for inductive types #[derive(Debug, Clone, PartialEq)] pub struct Constructor { pub name: String, pub ty: Term, } /// Structure fields #[derive(Debug, Clone, PartialEq)] pub struct Field { pub name: String, pub ty: Term, } /// Module containing multiple declarations #[derive(Debug, Clone, PartialEq)] pub struct Module { pub declarations: Vec<Declaration>, } impl fmt::Display for Universe { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Universe::Const(n) => write!(f, "{}", n), Universe::ScopedVar(scope, var) => write!(f, "{}::{}", scope, var), Universe::Meta(id) => write!(f, "?u{}", id), Universe::Add(u, n) => write!(f, "{}+{}", u, n), Universe::Max(u, v) => write!(f, "max({}, {})", u, v), Universe::IMax(u, v) => write!(f, "imax({}, {})", u, v), } } } impl fmt::Display for Term { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Term::Var(x) => write!(f, "{}", x), Term::App(t1, t2) => write!(f, "({} {})", t1, t2), Term::Abs(x, ty, body) => write!(f, "(fun {} : {} => {})", x, ty, body), Term::Pi(x, ty, body, implicit) => { if Self::occurs_free(x, body) { if *implicit { write!(f, "{{{} : {}}} → {}", x, ty, body) } else { write!(f, "({} : {}) → {}", x, ty, body) } } else { write!(f, "{} → {}", ty, body) } } Term::Sort(u) => match u { Universe::Const(0) => write!(f, "Prop"), Universe::Const(n) => { if *n == 1 { write!(f, "Type") } else { write!(f, "Type {}", n - 1) } } Universe::Add(ref base, n) => { if let Universe::Const(1) = **base { write!(f, "Type {}", n) } else { write!(f, "Sort {}", u) } } _ => write!(f, "Sort {}", u), }, Term::Let(x, ty, val, body) => write!(f, "(let {} : {} := {} in {})", x, ty, val, body), Term::Match(scrutinee, arms) => { writeln!(f, "match {} with", scrutinee)?; for arm in arms { writeln!(f, "| {} => {}", arm.pattern, arm.body)?; } Ok(()) } Term::Constructor(name, args) => { write!(f, "{}", name)?; for arg in args { write!(f, " {}", arg)?; } Ok(()) } Term::Const(name) => write!(f, "{}", name), Term::Meta(name) => write!(f, "?{}", name), Term::Proj(term, field) => write!(f, "{}.{}", term, field), Term::Sigma(x, domain, codomain) => write!(f, "Σ ({} : {}), {}", x, domain, codomain), Term::Pair(fst, snd) => write!(f, "⟨{}, {}⟩", fst, snd), Term::Fst(pair) => write!(f, "π₁({})", pair), Term::Snd(pair) => write!(f, "π₂({})", pair), } } } impl fmt::Display for Pattern { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Pattern::Var(x) => write!(f, "{}", x), Pattern::Constructor(name, args) => { write!(f, "{}", name)?; for arg in args { write!(f, " {}", arg)?; } Ok(()) } Pattern::Wildcard => write!(f, "_"), } } } impl Term { /// Check if variable occurs free in term pub fn occurs_free(var: &str, term: &Term) -> bool { match term { Term::Var(x) => x == var, Term::App(t1, t2) => Self::occurs_free(var, t1) || Self::occurs_free(var, t2), Term::Abs(x, ty, body) => { Self::occurs_free(var, ty) || (x != var && Self::occurs_free(var, body)) } Term::Pi(x, ty, body, _) => { Self::occurs_free(var, ty) || (x != var && Self::occurs_free(var, body)) } Term::Sort(_) => false, Term::Let(x, ty, val, body) => { Self::occurs_free(var, ty) || Self::occurs_free(var, val) || (x != var && Self::occurs_free(var, body)) } Term::Match(scrutinee, arms) => { Self::occurs_free(var, scrutinee) || arms.iter().any(|arm| Self::occurs_free(var, &arm.body)) } Term::Constructor(_, args) => args.iter().any(|arg| Self::occurs_free(var, arg)), Term::Const(_) => false, Term::Meta(_) => false, Term::Proj(term, _) => Self::occurs_free(var, term), Term::Sigma(x, domain, codomain) => { Self::occurs_free(var, domain) || (x != var && Self::occurs_free(var, codomain)) } Term::Pair(fst, snd) => Self::occurs_free(var, fst) || Self::occurs_free(var, snd), Term::Fst(pair) | Term::Snd(pair) => Self::occurs_free(var, pair), } } } impl UniverseContext { pub fn new() -> Self { UniverseContext { variables: Vec::new(), constraints: Vec::new(), } } /// Add a universe variable to the context pub fn add_var(&mut self, name: String) { if !self.variables.contains(&name) { self.variables.push(name); } } /// Add a constraint to the context pub fn add_constraint(&mut self, constraint: UniverseConstraint) { self.constraints.push(constraint); } /// Check if a universe variable is bound in this context pub fn contains(&self, name: &str) -> bool { self.variables.contains(&name.to_string()) } /// Extend context with variables from another context pub fn extend(&self, other: &UniverseContext) -> Self { let mut new_ctx = self.clone(); for var in &other.variables { new_ctx.add_var(var.clone()); } for constraint in &other.constraints { new_ctx.add_constraint(constraint.clone()); } new_ctx } /// Generate a fresh universe variable name pub fn fresh_var(&self, base: &str) -> String { let mut counter = 0; loop { let name = if counter == 0 { base.to_string() } else { format!("{}{}", base, counter) }; if !self.contains(&name) { return name; } counter += 1; } } } impl Default for UniverseContext { fn default() -> Self { Self::new() } } impl Universe { /// Create a scoped universe variable pub fn scoped_var(scope: String, name: String) -> Self { Universe::ScopedVar(scope, name) } } /// Patterns for match expressions #[derive(Debug, Clone, PartialEq)] pub enum Pattern { /// Variable pattern: x Var(String), /// Constructor pattern: Cons x xs Constructor(String, Vec<Pattern>), /// Wildcard pattern: _ Wildcard, } }
The pattern system supports constructor patterns that destructure inductive values, variable patterns that bind matched components to names, and wildcard patterns that match any value without binding. This comprehensive pattern language enables complete analysis of inductive data structures.
#![allow(unused)] fn main() { use std::fmt; /// Core terms in the Calculus of Constructions #[derive(Debug, Clone, PartialEq)] pub enum Term { /// Variables: x, y, z Var(String), /// Application: f a App(Box<Term>, Box<Term>), /// Lambda abstraction: λ x : A, t (written as fun x : A => t) Abs(String, Box<Term>, Box<Term>), /// Dependent product: Π x : A, B (written as (x : A) → B or {x : A} → B) Pi(String, Box<Term>, Box<Term>, bool), // bool = implicit /// Sort/Type: Sort u, Type, Prop Sort(Universe), /// Let binding: let x := t in s Let(String, Box<Term>, Box<Term>, Box<Term>), /// Match expression with patterns Match(Box<Term>, Vec<MatchArm>), /// Inductive type constructor Constructor(String, Vec<Term>), /// Local constant (for definitions and axioms) Const(String), /// Meta-variable for type inference Meta(String), /// Field projection: term.field Proj(Box<Term>, String), /// Dependent pair type (Sigma type): Σ (x : A), B Sigma(String, Box<Term>, Box<Term>), /// Pair constructor: ⟨a, b⟩ Pair(Box<Term>, Box<Term>), /// First projection: π₁ Fst(Box<Term>), /// Second projection: π₂ Snd(Box<Term>), } /// Universe levels for type theory #[derive(Debug, Clone, PartialEq, Eq)] pub enum Universe { Const(u32), // Concrete level: 0, 1, 2, ... ScopedVar(String, String), // Scoped universe variable: (scope_name, var_name) Meta(u32), // Universe metavariable: ?u₀, ?u₁, ... Add(Box<Universe>, u32), // Level + n Max(Box<Universe>, Box<Universe>), // max(u, v) IMax(Box<Universe>, Box<Universe>), // imax(u, v) } /// Universe level constraints for polymorphism #[derive(Debug, Clone, PartialEq, Eq)] pub enum UniverseConstraint { /// u ≤ v LessEq(Universe, Universe), /// u = v Equal(Universe, Universe), } /// Context for universe level variables #[derive(Debug, Clone, PartialEq)] pub struct UniverseContext { /// Currently bound universe variables pub variables: Vec<String>, /// Constraints on universe levels pub constraints: Vec<UniverseConstraint>, } /// Patterns for match expressions #[derive(Debug, Clone, PartialEq)] pub enum Pattern { /// Variable pattern: x Var(String), /// Constructor pattern: Cons x xs Constructor(String, Vec<Pattern>), /// Wildcard pattern: _ Wildcard, } /// Top-level declarations #[derive(Debug, Clone, PartialEq)] pub enum Declaration { /// Constant definition: def name {u...} (params) : type := body Definition { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, body: Term, }, /// Axiom: axiom name {u...} : type Axiom { name: String, universe_params: Vec<String>, // Universe level parameters ty: Term, }, /// Inductive type: inductive Name {u...} (params) : Type := constructors Inductive { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, constructors: Vec<Constructor>, }, /// Structure (single constructor inductive): structure Name {u...} := /// (fields) Structure { name: String, universe_params: Vec<String>, // Universe level parameters params: Vec<Parameter>, ty: Term, fields: Vec<Field>, }, } /// Function parameters #[derive(Debug, Clone, PartialEq)] pub struct Parameter { pub name: String, pub ty: Term, pub implicit: bool, // for {x : A} vs (x : A) } /// Constructor for inductive types #[derive(Debug, Clone, PartialEq)] pub struct Constructor { pub name: String, pub ty: Term, } /// Structure fields #[derive(Debug, Clone, PartialEq)] pub struct Field { pub name: String, pub ty: Term, } /// Module containing multiple declarations #[derive(Debug, Clone, PartialEq)] pub struct Module { pub declarations: Vec<Declaration>, } impl fmt::Display for Universe { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Universe::Const(n) => write!(f, "{}", n), Universe::ScopedVar(scope, var) => write!(f, "{}::{}", scope, var), Universe::Meta(id) => write!(f, "?u{}", id), Universe::Add(u, n) => write!(f, "{}+{}", u, n), Universe::Max(u, v) => write!(f, "max({}, {})", u, v), Universe::IMax(u, v) => write!(f, "imax({}, {})", u, v), } } } impl fmt::Display for Term { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Term::Var(x) => write!(f, "{}", x), Term::App(t1, t2) => write!(f, "({} {})", t1, t2), Term::Abs(x, ty, body) => write!(f, "(fun {} : {} => {})", x, ty, body), Term::Pi(x, ty, body, implicit) => { if Self::occurs_free(x, body) { if *implicit { write!(f, "{{{} : {}}} → {}", x, ty, body) } else { write!(f, "({} : {}) → {}", x, ty, body) } } else { write!(f, "{} → {}", ty, body) } } Term::Sort(u) => match u { Universe::Const(0) => write!(f, "Prop"), Universe::Const(n) => { if *n == 1 { write!(f, "Type") } else { write!(f, "Type {}", n - 1) } } Universe::Add(ref base, n) => { if let Universe::Const(1) = **base { write!(f, "Type {}", n) } else { write!(f, "Sort {}", u) } } _ => write!(f, "Sort {}", u), }, Term::Let(x, ty, val, body) => write!(f, "(let {} : {} := {} in {})", x, ty, val, body), Term::Match(scrutinee, arms) => { writeln!(f, "match {} with", scrutinee)?; for arm in arms { writeln!(f, "| {} => {}", arm.pattern, arm.body)?; } Ok(()) } Term::Constructor(name, args) => { write!(f, "{}", name)?; for arg in args { write!(f, " {}", arg)?; } Ok(()) } Term::Const(name) => write!(f, "{}", name), Term::Meta(name) => write!(f, "?{}", name), Term::Proj(term, field) => write!(f, "{}.{}", term, field), Term::Sigma(x, domain, codomain) => write!(f, "Σ ({} : {}), {}", x, domain, codomain), Term::Pair(fst, snd) => write!(f, "⟨{}, {}⟩", fst, snd), Term::Fst(pair) => write!(f, "π₁({})", pair), Term::Snd(pair) => write!(f, "π₂({})", pair), } } } impl fmt::Display for Pattern { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Pattern::Var(x) => write!(f, "{}", x), Pattern::Constructor(name, args) => { write!(f, "{}", name)?; for arg in args { write!(f, " {}", arg)?; } Ok(()) } Pattern::Wildcard => write!(f, "_"), } } } impl Term { /// Check if variable occurs free in term pub fn occurs_free(var: &str, term: &Term) -> bool { match term { Term::Var(x) => x == var, Term::App(t1, t2) => Self::occurs_free(var, t1) || Self::occurs_free(var, t2), Term::Abs(x, ty, body) => { Self::occurs_free(var, ty) || (x != var && Self::occurs_free(var, body)) } Term::Pi(x, ty, body, _) => { Self::occurs_free(var, ty) || (x != var && Self::occurs_free(var, body)) } Term::Sort(_) => false, Term::Let(x, ty, val, body) => { Self::occurs_free(var, ty) || Self::occurs_free(var, val) || (x != var && Self::occurs_free(var, body)) } Term::Match(scrutinee, arms) => { Self::occurs_free(var, scrutinee) || arms.iter().any(|arm| Self::occurs_free(var, &arm.body)) } Term::Constructor(_, args) => args.iter().any(|arg| Self::occurs_free(var, arg)), Term::Const(_) => false, Term::Meta(_) => false, Term::Proj(term, _) => Self::occurs_free(var, term), Term::Sigma(x, domain, codomain) => { Self::occurs_free(var, domain) || (x != var && Self::occurs_free(var, codomain)) } Term::Pair(fst, snd) => Self::occurs_free(var, fst) || Self::occurs_free(var, snd), Term::Fst(pair) | Term::Snd(pair) => Self::occurs_free(var, pair), } } } impl UniverseContext { pub fn new() -> Self { UniverseContext { variables: Vec::new(), constraints: Vec::new(), } } /// Add a universe variable to the context pub fn add_var(&mut self, name: String) { if !self.variables.contains(&name) { self.variables.push(name); } } /// Add a constraint to the context pub fn add_constraint(&mut self, constraint: UniverseConstraint) { self.constraints.push(constraint); } /// Check if a universe variable is bound in this context pub fn contains(&self, name: &str) -> bool { self.variables.contains(&name.to_string()) } /// Extend context with variables from another context pub fn extend(&self, other: &UniverseContext) -> Self { let mut new_ctx = self.clone(); for var in &other.variables { new_ctx.add_var(var.clone()); } for constraint in &other.constraints { new_ctx.add_constraint(constraint.clone()); } new_ctx } /// Generate a fresh universe variable name pub fn fresh_var(&self, base: &str) -> String { let mut counter = 0; loop { let name = if counter == 0 { base.to_string() } else { format!("{}{}", base, counter) }; if !self.contains(&name) { return name; } counter += 1; } } } impl Default for UniverseContext { fn default() -> Self { Self::new() } } impl Universe { /// Create a scoped universe variable pub fn scoped_var(scope: String, name: String) -> Self { Universe::ScopedVar(scope, name) } } /// Pattern matching arms #[derive(Debug, Clone, PartialEq)] pub struct MatchArm { pub pattern: Pattern, pub body: Term, } }
Match arms associate patterns with result expressions, creating the case analysis structure that defines how pattern matching behaves. Each arm must produce a result of the same type, ensuring that pattern matching expressions have well-defined types regardless of which case is selected at runtime.
Pattern Type Checking
The type checking algorithm for pattern matching ensures that patterns are consistent with the types being matched and that all cases produce compatible result types:
#![allow(unused)] fn main() { /// Check a pattern against a type and return extended context with pattern /// variables fn check_pattern( &mut self, pattern: &Pattern, expected_type: &Term, ctx: &Context, ) -> TypeResult<Context> { match pattern { Pattern::Var(x) => { // Check if this is actually a constructor with no arguments if ctx.lookup_constructor(x).is_some() { // It's actually a constructor pattern with no arguments return self.check_pattern( &Pattern::Constructor(x.clone(), vec![]), expected_type, ctx, ); } // Variable pattern binds the scrutinee to the variable Ok(ctx.extend(x.clone(), expected_type.clone())) } Pattern::Wildcard => { // Wildcard matches anything, adds no bindings Ok(ctx.clone()) } Pattern::Constructor(ctor_name, ctor_args) => { // Look up constructor type - check both constructors and definitions let (ctor_type, is_instantiated) = if let Some(ty) = ctx.lookup_constructor(ctor_name) { (ty.clone(), false) } else if let Some(def) = ctx.lookup_definition(ctor_name) { // Instantiate universe parameters for universe-polymorphic constructors let instantiated = self.instantiate_universe_params( &def.ty, &def.universe_params, &def.name, ctx, )?; (instantiated, true) } else { return Err(TypeError::UnknownConstructor { name: ctor_name.clone(), }); }; if is_instantiated { // For instantiated constructors, use constraint-based approach // The constructor type already has metavariables that can unify correctly let return_type = extract_constructor_return_type(&ctor_type); // Use constraint solving to check the return type matches expected type let mut solver = Solver::new(ctx.clone()); let constraint_id = solver.new_constraint_id(); let constraint = crate::solver::Constraint::Unify { id: constraint_id, left: return_type.clone(), right: expected_type.clone(), strength: ConstraintStrength::Required, }; solver.add_constraint(constraint); let _subst = solver.solve()?; // This will error if unification fails // Extract argument types directly from instantiated constructor type let arg_types = extract_constructor_arg_types(&ctor_type); // Check sub-patterns against argument types if arg_types.len() != ctor_args.len() { return Err(TypeError::ConstructorArityMismatch { name: ctor_name.clone(), expected: arg_types.len(), actual: ctor_args.len(), }); } let mut extended_ctx = ctx.clone(); for (arg_pattern, arg_type) in ctor_args.iter().zip(arg_types.iter()) { extended_ctx = self.check_pattern(arg_pattern, arg_type, &extended_ctx)?; } Ok(extended_ctx) } else { // For regular constructors, use the existing specialization approach let specialized_ctor_type = self.specialize_constructor_type(&ctor_type, expected_type, ctx)?; let return_type = extract_constructor_return_type(&specialized_ctor_type); if !self.definitionally_equal(&return_type, expected_type, ctx)? { return Err(TypeError::TypeMismatch { expected: expected_type.clone(), actual: return_type, }); } // Extract argument types from specialized constructor type and check // sub-patterns let arg_types = extract_constructor_arg_types(&specialized_ctor_type); if ctor_args.len() != arg_types.len() { return Err(TypeError::ConstructorArityMismatch { name: ctor_name.clone(), expected: arg_types.len(), actual: ctor_args.len(), }); } let mut extended_ctx = ctx.clone(); for (arg_pattern, arg_type) in ctor_args.iter().zip(arg_types.iter()) { extended_ctx = self.check_pattern(arg_pattern, arg_type, &extended_ctx)?; } Ok(extended_ctx) } } } } }
Pattern type checking validates that constructor patterns match the structure of their corresponding constructors, that variable patterns receive appropriate types from the matched context, and that wildcard patterns are used correctly. The algorithm maintains a typing context that tracks the types of pattern variables for use in result expressions.
The pattern checker handles universe polymorphism by ensuring that constructor patterns properly instantiate universe-polymorphic constructors. When a pattern matches against a constructor from a universe-polymorphic inductive type, the checker verifies that universe constraints are satisfied throughout the pattern matching process.
Constructor Type Inference
Constructor applications in terms require specialized type inference to handle the interaction between constructor types and their arguments:
#![allow(unused)] fn main() { /// Infer the type of a term pub fn infer(&mut self, term: &Term, ctx: &Context) -> TypeResult<Term> { self.with_context(term, |checker| checker.infer_impl(term, ctx)) } }
Constructor type inference looks up constructor types from the context, specializes them with appropriate type arguments, and validates that the constructor is applied to arguments of the correct types. The algorithm handles both simple constructors and constructors that belong to universe-polymorphic inductive types.
Pattern Matching Utilities
Several utility functions support the pattern matching implementation by providing operations on patterns and constructor types:
#![allow(unused)] fn main() { use std::collections::HashMap; use crate::ast::{MatchArm, Pattern, Term, Universe}; /// Substitute universe variables in a term pub fn substitute_universes(term: &Term, subst: &HashMap<String, Universe>) -> Term { match term { Term::Sort(u) => Term::Sort(substitute_universe(u, subst)), Term::Var(x) => Term::Var(x.clone()), Term::Const(c) => Term::Const(c.clone()), Term::App(f, arg) => Term::App( Box::new(substitute_universes(f, subst)), Box::new(substitute_universes(arg, subst)), ), Term::Abs(x, ty, body) => Term::Abs( x.clone(), Box::new(substitute_universes(ty, subst)), Box::new(substitute_universes(body, subst)), ), Term::Pi(x, ty, body, implicit) => Term::Pi( x.clone(), Box::new(substitute_universes(ty, subst)), Box::new(substitute_universes(body, subst)), *implicit, ), Term::Let(x, ty, val, body) => Term::Let( x.clone(), Box::new(substitute_universes(ty, subst)), Box::new(substitute_universes(val, subst)), Box::new(substitute_universes(body, subst)), ), _ => term.clone(), // For other terms, no substitution needed } } /// Substitute universe variables in a universe expression pub fn substitute_universe(u: &Universe, subst: &HashMap<String, Universe>) -> Universe { let result = match u { Universe::ScopedVar(_scope, var) => { // For scoped variables, try to substitute using just the variable name // This allows substitution within the correct scope subst.get(var).cloned().unwrap_or_else(|| u.clone()) } Universe::Const(n) => Universe::Const(*n), Universe::Add(u, n) => { let base = substitute_universe(u, subst); Universe::Add(Box::new(base), *n) } Universe::Max(u1, u2) => Universe::Max( Box::new(substitute_universe(u1, subst)), Box::new(substitute_universe(u2, subst)), ), Universe::IMax(u1, u2) => Universe::IMax( Box::new(substitute_universe(u1, subst)), Box::new(substitute_universe(u2, subst)), ), _ => u.clone(), }; normalize_universe(&result) } /// Normalize a universe expression by simplifying it pub fn normalize_universe(u: &Universe) -> Universe { match u { Universe::Add(base, n) => match **base { Universe::Const(m) => Universe::Const(m + n), _ => u.clone(), }, Universe::Max(u1, u2) => { let u1_norm = normalize_universe(u1); let u2_norm = normalize_universe(u2); match (&u1_norm, &u2_norm) { (Universe::Const(n1), Universe::Const(n2)) => Universe::Const((*n1).max(*n2)), _ => Universe::Max(Box::new(u1_norm), Box::new(u2_norm)), } } _ => u.clone(), } } /// Rename variable in term pub fn rename_var(old: &str, new: &str, term: &Term) -> Term { match term { Term::Var(x) if x == old => Term::Var(new.to_string()), Term::Var(_) => term.clone(), Term::App(f, arg) => Term::App( Box::new(rename_var(old, new, f)), Box::new(rename_var(old, new, arg)), ), Term::Abs(x, ty, body) if x == old => { // Don't rename bound occurrences Term::Abs( new.to_string(), Box::new(rename_var(old, new, ty)), Box::new(body.as_ref().clone()), ) } Term::Abs(x, ty, body) => Term::Abs( x.clone(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, body)), ), Term::Pi(x, ty, body, implicit) if x == old => Term::Pi( new.to_string(), Box::new(rename_var(old, new, ty)), Box::new(body.as_ref().clone()), *implicit, ), Term::Pi(x, ty, body, implicit) => Term::Pi( x.clone(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, body)), *implicit, ), Term::Let(x, ty, val, body) if x == old => Term::Let( new.to_string(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, val)), Box::new(body.as_ref().clone()), ), Term::Let(x, ty, val, body) => Term::Let( x.clone(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, val)), Box::new(rename_var(old, new, body)), ), Term::Sigma(x, domain, codomain) if x == old => Term::Sigma( new.to_string(), Box::new(rename_var(old, new, domain)), Box::new(codomain.as_ref().clone()), ), Term::Sigma(x, domain, codomain) => Term::Sigma( x.clone(), Box::new(rename_var(old, new, domain)), Box::new(rename_var(old, new, codomain)), ), Term::Pair(fst, snd) => Term::Pair( Box::new(rename_var(old, new, fst)), Box::new(rename_var(old, new, snd)), ), Term::Fst(pair) => Term::Fst(Box::new(rename_var(old, new, pair))), Term::Snd(pair) => Term::Snd(Box::new(rename_var(old, new, pair))), Term::Proj(term, field) => Term::Proj(Box::new(rename_var(old, new, term)), field.clone()), Term::Match(scrutinee, arms) => { let scrutinee_renamed = rename_var(old, new, scrutinee); let arms_renamed = arms .iter() .map(|arm| { // For match arms, we need to be careful about pattern variable bindings let body_renamed = if pattern_binds_var(&arm.pattern, old) { // Variable is bound by pattern, don't rename in body arm.body.clone() } else { rename_var(old, new, &arm.body) }; MatchArm { pattern: arm.pattern.clone(), // Patterns don't contain renameable terms body: body_renamed, } }) .collect(); Term::Match(Box::new(scrutinee_renamed), arms_renamed) } _ => term.clone(), } } /// Generate fresh variable name avoiding conflicts pub fn fresh_var(base: &str, avoid: &[String]) -> String { let mut counter = 0; loop { let candidate = if counter == 0 { base.to_string() } else { format!("{}{}", base, counter) }; if !avoid.contains(&candidate) { return candidate; } counter += 1; } } /// Check if a type is "simple" (like Nat, Bool, etc.) pub fn is_simple_type(ty: &Term) -> bool { matches!(ty, Term::Const(_)) } /// Check if a term has implicit parameters pub fn has_implicit_params(ty: &Term) -> bool { match ty { Term::Pi(_, _, _, implicit) => *implicit, _ => false, } } /// Extract the return type from a constructor type (the final codomain after /// stripping Pi types) pub fn extract_constructor_return_type(ctor_type: &Term) -> Term { match ctor_type { Term::Pi(_, _, codomain, _) => extract_constructor_return_type(codomain), other => other.clone(), } } /// Extract argument types from a constructor type, skipping type parameters pub fn extract_constructor_arg_types(ctor_type: &Term) -> Vec<Term> { let mut arg_types = Vec::new(); let mut current = ctor_type; while let Term::Pi(_, domain, codomain, _) = current { // Skip type parameters (those whose type is a Sort) if !matches!(domain.as_ref(), Term::Sort(_)) { arg_types.push(domain.as_ref().clone()); } current = codomain; } arg_types } /// Check if a term contains universe metavariables pub fn contains_universe_metavariables(term: &Term) -> bool { match term { Term::Sort(u) => universe_contains_metavariables(u), Term::App(f, arg) => { contains_universe_metavariables(f) || contains_universe_metavariables(arg) } Term::Abs(_, ty, body) | Term::Pi(_, ty, body, _) => { contains_universe_metavariables(ty) || contains_universe_metavariables(body) } Term::Let(_, ty, val, body) => { contains_universe_metavariables(ty) || contains_universe_metavariables(val) || contains_universe_metavariables(body) } _ => false, } } /// Check if a universe expression contains metavariables pub fn universe_contains_metavariables(universe: &Universe) -> bool { match universe { Universe::Meta(_) => true, Universe::Add(base, _) => universe_contains_metavariables(base), Universe::Max(u, v) | Universe::IMax(u, v) => { universe_contains_metavariables(u) || universe_contains_metavariables(v) } _ => false, } } /// Check if a pattern binds a specific variable pub fn pattern_binds_var(pattern: &Pattern, var: &str) -> bool { match pattern { Pattern::Var(x) => x == var, Pattern::Wildcard => false, Pattern::Constructor(_, args) => args.iter().any(|arg| pattern_binds_var(arg, var)), } } }
This utility determines whether a pattern introduces a binding for a specific variable, enabling the type checker to track variable scopes correctly across pattern matching expressions.
#![allow(unused)] fn main() { use std::collections::HashMap; use crate::ast::{MatchArm, Pattern, Term, Universe}; /// Substitute universe variables in a term pub fn substitute_universes(term: &Term, subst: &HashMap<String, Universe>) -> Term { match term { Term::Sort(u) => Term::Sort(substitute_universe(u, subst)), Term::Var(x) => Term::Var(x.clone()), Term::Const(c) => Term::Const(c.clone()), Term::App(f, arg) => Term::App( Box::new(substitute_universes(f, subst)), Box::new(substitute_universes(arg, subst)), ), Term::Abs(x, ty, body) => Term::Abs( x.clone(), Box::new(substitute_universes(ty, subst)), Box::new(substitute_universes(body, subst)), ), Term::Pi(x, ty, body, implicit) => Term::Pi( x.clone(), Box::new(substitute_universes(ty, subst)), Box::new(substitute_universes(body, subst)), *implicit, ), Term::Let(x, ty, val, body) => Term::Let( x.clone(), Box::new(substitute_universes(ty, subst)), Box::new(substitute_universes(val, subst)), Box::new(substitute_universes(body, subst)), ), _ => term.clone(), // For other terms, no substitution needed } } /// Substitute universe variables in a universe expression pub fn substitute_universe(u: &Universe, subst: &HashMap<String, Universe>) -> Universe { let result = match u { Universe::ScopedVar(_scope, var) => { // For scoped variables, try to substitute using just the variable name // This allows substitution within the correct scope subst.get(var).cloned().unwrap_or_else(|| u.clone()) } Universe::Const(n) => Universe::Const(*n), Universe::Add(u, n) => { let base = substitute_universe(u, subst); Universe::Add(Box::new(base), *n) } Universe::Max(u1, u2) => Universe::Max( Box::new(substitute_universe(u1, subst)), Box::new(substitute_universe(u2, subst)), ), Universe::IMax(u1, u2) => Universe::IMax( Box::new(substitute_universe(u1, subst)), Box::new(substitute_universe(u2, subst)), ), _ => u.clone(), }; normalize_universe(&result) } /// Normalize a universe expression by simplifying it pub fn normalize_universe(u: &Universe) -> Universe { match u { Universe::Add(base, n) => match **base { Universe::Const(m) => Universe::Const(m + n), _ => u.clone(), }, Universe::Max(u1, u2) => { let u1_norm = normalize_universe(u1); let u2_norm = normalize_universe(u2); match (&u1_norm, &u2_norm) { (Universe::Const(n1), Universe::Const(n2)) => Universe::Const((*n1).max(*n2)), _ => Universe::Max(Box::new(u1_norm), Box::new(u2_norm)), } } _ => u.clone(), } } /// Rename variable in term pub fn rename_var(old: &str, new: &str, term: &Term) -> Term { match term { Term::Var(x) if x == old => Term::Var(new.to_string()), Term::Var(_) => term.clone(), Term::App(f, arg) => Term::App( Box::new(rename_var(old, new, f)), Box::new(rename_var(old, new, arg)), ), Term::Abs(x, ty, body) if x == old => { // Don't rename bound occurrences Term::Abs( new.to_string(), Box::new(rename_var(old, new, ty)), Box::new(body.as_ref().clone()), ) } Term::Abs(x, ty, body) => Term::Abs( x.clone(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, body)), ), Term::Pi(x, ty, body, implicit) if x == old => Term::Pi( new.to_string(), Box::new(rename_var(old, new, ty)), Box::new(body.as_ref().clone()), *implicit, ), Term::Pi(x, ty, body, implicit) => Term::Pi( x.clone(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, body)), *implicit, ), Term::Let(x, ty, val, body) if x == old => Term::Let( new.to_string(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, val)), Box::new(body.as_ref().clone()), ), Term::Let(x, ty, val, body) => Term::Let( x.clone(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, val)), Box::new(rename_var(old, new, body)), ), Term::Sigma(x, domain, codomain) if x == old => Term::Sigma( new.to_string(), Box::new(rename_var(old, new, domain)), Box::new(codomain.as_ref().clone()), ), Term::Sigma(x, domain, codomain) => Term::Sigma( x.clone(), Box::new(rename_var(old, new, domain)), Box::new(rename_var(old, new, codomain)), ), Term::Pair(fst, snd) => Term::Pair( Box::new(rename_var(old, new, fst)), Box::new(rename_var(old, new, snd)), ), Term::Fst(pair) => Term::Fst(Box::new(rename_var(old, new, pair))), Term::Snd(pair) => Term::Snd(Box::new(rename_var(old, new, pair))), Term::Proj(term, field) => Term::Proj(Box::new(rename_var(old, new, term)), field.clone()), Term::Match(scrutinee, arms) => { let scrutinee_renamed = rename_var(old, new, scrutinee); let arms_renamed = arms .iter() .map(|arm| { // For match arms, we need to be careful about pattern variable bindings let body_renamed = if pattern_binds_var(&arm.pattern, old) { // Variable is bound by pattern, don't rename in body arm.body.clone() } else { rename_var(old, new, &arm.body) }; MatchArm { pattern: arm.pattern.clone(), // Patterns don't contain renameable terms body: body_renamed, } }) .collect(); Term::Match(Box::new(scrutinee_renamed), arms_renamed) } _ => term.clone(), } } /// Check if a pattern binds a specific variable pub fn pattern_binds_var(pattern: &Pattern, var: &str) -> bool { match pattern { Pattern::Var(x) => x == var, Pattern::Wildcard => false, Pattern::Constructor(_, args) => args.iter().any(|arg| pattern_binds_var(arg, var)), } } /// Generate fresh variable name avoiding conflicts pub fn fresh_var(base: &str, avoid: &[String]) -> String { let mut counter = 0; loop { let candidate = if counter == 0 { base.to_string() } else { format!("{}{}", base, counter) }; if !avoid.contains(&candidate) { return candidate; } counter += 1; } } /// Check if a type is "simple" (like Nat, Bool, etc.) pub fn is_simple_type(ty: &Term) -> bool { matches!(ty, Term::Const(_)) } /// Check if a term has implicit parameters pub fn has_implicit_params(ty: &Term) -> bool { match ty { Term::Pi(_, _, _, implicit) => *implicit, _ => false, } } /// Extract argument types from a constructor type, skipping type parameters pub fn extract_constructor_arg_types(ctor_type: &Term) -> Vec<Term> { let mut arg_types = Vec::new(); let mut current = ctor_type; while let Term::Pi(_, domain, codomain, _) = current { // Skip type parameters (those whose type is a Sort) if !matches!(domain.as_ref(), Term::Sort(_)) { arg_types.push(domain.as_ref().clone()); } current = codomain; } arg_types } /// Check if a term contains universe metavariables pub fn contains_universe_metavariables(term: &Term) -> bool { match term { Term::Sort(u) => universe_contains_metavariables(u), Term::App(f, arg) => { contains_universe_metavariables(f) || contains_universe_metavariables(arg) } Term::Abs(_, ty, body) | Term::Pi(_, ty, body, _) => { contains_universe_metavariables(ty) || contains_universe_metavariables(body) } Term::Let(_, ty, val, body) => { contains_universe_metavariables(ty) || contains_universe_metavariables(val) || contains_universe_metavariables(body) } _ => false, } } /// Check if a universe expression contains metavariables pub fn universe_contains_metavariables(universe: &Universe) -> bool { match universe { Universe::Meta(_) => true, Universe::Add(base, _) => universe_contains_metavariables(base), Universe::Max(u, v) | Universe::IMax(u, v) => { universe_contains_metavariables(u) || universe_contains_metavariables(v) } _ => false, } } /// Extract the return type from a constructor type (the final codomain after /// stripping Pi types) pub fn extract_constructor_return_type(ctor_type: &Term) -> Term { match ctor_type { Term::Pi(_, _, codomain, _) => extract_constructor_return_type(codomain), other => other.clone(), } } }
Constructor return type extraction analyzes constructor type signatures to determine the result type produced by constructor applications. This operation is essential for validating that constructor uses are type-correct.
#![allow(unused)] fn main() { use std::collections::HashMap; use crate::ast::{MatchArm, Pattern, Term, Universe}; /// Substitute universe variables in a term pub fn substitute_universes(term: &Term, subst: &HashMap<String, Universe>) -> Term { match term { Term::Sort(u) => Term::Sort(substitute_universe(u, subst)), Term::Var(x) => Term::Var(x.clone()), Term::Const(c) => Term::Const(c.clone()), Term::App(f, arg) => Term::App( Box::new(substitute_universes(f, subst)), Box::new(substitute_universes(arg, subst)), ), Term::Abs(x, ty, body) => Term::Abs( x.clone(), Box::new(substitute_universes(ty, subst)), Box::new(substitute_universes(body, subst)), ), Term::Pi(x, ty, body, implicit) => Term::Pi( x.clone(), Box::new(substitute_universes(ty, subst)), Box::new(substitute_universes(body, subst)), *implicit, ), Term::Let(x, ty, val, body) => Term::Let( x.clone(), Box::new(substitute_universes(ty, subst)), Box::new(substitute_universes(val, subst)), Box::new(substitute_universes(body, subst)), ), _ => term.clone(), // For other terms, no substitution needed } } /// Substitute universe variables in a universe expression pub fn substitute_universe(u: &Universe, subst: &HashMap<String, Universe>) -> Universe { let result = match u { Universe::ScopedVar(_scope, var) => { // For scoped variables, try to substitute using just the variable name // This allows substitution within the correct scope subst.get(var).cloned().unwrap_or_else(|| u.clone()) } Universe::Const(n) => Universe::Const(*n), Universe::Add(u, n) => { let base = substitute_universe(u, subst); Universe::Add(Box::new(base), *n) } Universe::Max(u1, u2) => Universe::Max( Box::new(substitute_universe(u1, subst)), Box::new(substitute_universe(u2, subst)), ), Universe::IMax(u1, u2) => Universe::IMax( Box::new(substitute_universe(u1, subst)), Box::new(substitute_universe(u2, subst)), ), _ => u.clone(), }; normalize_universe(&result) } /// Normalize a universe expression by simplifying it pub fn normalize_universe(u: &Universe) -> Universe { match u { Universe::Add(base, n) => match **base { Universe::Const(m) => Universe::Const(m + n), _ => u.clone(), }, Universe::Max(u1, u2) => { let u1_norm = normalize_universe(u1); let u2_norm = normalize_universe(u2); match (&u1_norm, &u2_norm) { (Universe::Const(n1), Universe::Const(n2)) => Universe::Const((*n1).max(*n2)), _ => Universe::Max(Box::new(u1_norm), Box::new(u2_norm)), } } _ => u.clone(), } } /// Rename variable in term pub fn rename_var(old: &str, new: &str, term: &Term) -> Term { match term { Term::Var(x) if x == old => Term::Var(new.to_string()), Term::Var(_) => term.clone(), Term::App(f, arg) => Term::App( Box::new(rename_var(old, new, f)), Box::new(rename_var(old, new, arg)), ), Term::Abs(x, ty, body) if x == old => { // Don't rename bound occurrences Term::Abs( new.to_string(), Box::new(rename_var(old, new, ty)), Box::new(body.as_ref().clone()), ) } Term::Abs(x, ty, body) => Term::Abs( x.clone(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, body)), ), Term::Pi(x, ty, body, implicit) if x == old => Term::Pi( new.to_string(), Box::new(rename_var(old, new, ty)), Box::new(body.as_ref().clone()), *implicit, ), Term::Pi(x, ty, body, implicit) => Term::Pi( x.clone(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, body)), *implicit, ), Term::Let(x, ty, val, body) if x == old => Term::Let( new.to_string(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, val)), Box::new(body.as_ref().clone()), ), Term::Let(x, ty, val, body) => Term::Let( x.clone(), Box::new(rename_var(old, new, ty)), Box::new(rename_var(old, new, val)), Box::new(rename_var(old, new, body)), ), Term::Sigma(x, domain, codomain) if x == old => Term::Sigma( new.to_string(), Box::new(rename_var(old, new, domain)), Box::new(codomain.as_ref().clone()), ), Term::Sigma(x, domain, codomain) => Term::Sigma( x.clone(), Box::new(rename_var(old, new, domain)), Box::new(rename_var(old, new, codomain)), ), Term::Pair(fst, snd) => Term::Pair( Box::new(rename_var(old, new, fst)), Box::new(rename_var(old, new, snd)), ), Term::Fst(pair) => Term::Fst(Box::new(rename_var(old, new, pair))), Term::Snd(pair) => Term::Snd(Box::new(rename_var(old, new, pair))), Term::Proj(term, field) => Term::Proj(Box::new(rename_var(old, new, term)), field.clone()), Term::Match(scrutinee, arms) => { let scrutinee_renamed = rename_var(old, new, scrutinee); let arms_renamed = arms .iter() .map(|arm| { // For match arms, we need to be careful about pattern variable bindings let body_renamed = if pattern_binds_var(&arm.pattern, old) { // Variable is bound by pattern, don't rename in body arm.body.clone() } else { rename_var(old, new, &arm.body) }; MatchArm { pattern: arm.pattern.clone(), // Patterns don't contain renameable terms body: body_renamed, } }) .collect(); Term::Match(Box::new(scrutinee_renamed), arms_renamed) } _ => term.clone(), } } /// Check if a pattern binds a specific variable pub fn pattern_binds_var(pattern: &Pattern, var: &str) -> bool { match pattern { Pattern::Var(x) => x == var, Pattern::Wildcard => false, Pattern::Constructor(_, args) => args.iter().any(|arg| pattern_binds_var(arg, var)), } } /// Generate fresh variable name avoiding conflicts pub fn fresh_var(base: &str, avoid: &[String]) -> String { let mut counter = 0; loop { let candidate = if counter == 0 { base.to_string() } else { format!("{}{}", base, counter) }; if !avoid.contains(&candidate) { return candidate; } counter += 1; } } /// Check if a type is "simple" (like Nat, Bool, etc.) pub fn is_simple_type(ty: &Term) -> bool { matches!(ty, Term::Const(_)) } /// Check if a term has implicit parameters pub fn has_implicit_params(ty: &Term) -> bool { match ty { Term::Pi(_, _, _, implicit) => *implicit, _ => false, } } /// Extract the return type from a constructor type (the final codomain after /// stripping Pi types) pub fn extract_constructor_return_type(ctor_type: &Term) -> Term { match ctor_type { Term::Pi(_, _, codomain, _) => extract_constructor_return_type(codomain), other => other.clone(), } } /// Check if a term contains universe metavariables pub fn contains_universe_metavariables(term: &Term) -> bool { match term { Term::Sort(u) => universe_contains_metavariables(u), Term::App(f, arg) => { contains_universe_metavariables(f) || contains_universe_metavariables(arg) } Term::Abs(_, ty, body) | Term::Pi(_, ty, body, _) => { contains_universe_metavariables(ty) || contains_universe_metavariables(body) } Term::Let(_, ty, val, body) => { contains_universe_metavariables(ty) || contains_universe_metavariables(val) || contains_universe_metavariables(body) } _ => false, } } /// Check if a universe expression contains metavariables pub fn universe_contains_metavariables(universe: &Universe) -> bool { match universe { Universe::Meta(_) => true, Universe::Add(base, _) => universe_contains_metavariables(base), Universe::Max(u, v) | Universe::IMax(u, v) => { universe_contains_metavariables(u) || universe_contains_metavariables(v) } _ => false, } } /// Extract argument types from a constructor type, skipping type parameters pub fn extract_constructor_arg_types(ctor_type: &Term) -> Vec<Term> { let mut arg_types = Vec::new(); let mut current = ctor_type; while let Term::Pi(_, domain, codomain, _) = current { // Skip type parameters (those whose type is a Sort) if !matches!(domain.as_ref(), Term::Sort(_)) { arg_types.push(domain.as_ref().clone()); } current = codomain; } arg_types } }
Argument type extraction decomposes constructor type signatures to identify the types expected for constructor arguments. This information guides type checking of constructor applications and pattern matching expressions.
Context Integration
Constructor information is maintained in the typing context to support constructor lookups during type checking:
#![allow(unused)] fn main() { /// Add constructor definition pub fn add_constructor(&mut self, name: String, ty: Term) { self.constructors.insert(name, ty); } }
Adding constructors to the context makes them available for type checking and pattern matching operations. The context maintains the mapping from constructor names to their type signatures, enabling efficient lookup during type inference.
#![allow(unused)] fn main() { /// Look up constructor type pub fn lookup_constructor(&self, name: &str) -> Option<&Term> { self.constructors.get(name) } }
Constructor lookup retrieves type information for constructor names encountered in terms or patterns. This operation is fundamental to constructor type checking and pattern matching validation.
Universe Polymorphic Inductive Types
The implementation supports universe polymorphic inductive types that can exist at different universe levels:
#![allow(unused)] fn main() { def id (A : Type) (x : A) : A := x def compose_poly (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (x : A) : C := g (f x) def apply_twice (A : Type) (f : A -> A) (x : A) : A := f (f x) }
Universe polymorphic inductive types demonstrate the full power of the Calculus of Constructions’ universe system. These types can be instantiated at different universe levels while maintaining their structural properties, enabling generic programming patterns that work across the entire universe hierarchy.
Basic Inductive Type Examples
Simple inductive types like natural numbers and booleans provide concrete examples of the inductive type system in action:
#![allow(unused)] fn main() { inductive Bool : Type with | true : Bool | false : Bool inductive Nat : Type with | zero : Nat | succ : Nat -> Nat def is_zero (n : Nat) : Bool := match n with case zero => true case succ(_) => false }
These examples demonstrate basic inductive type declarations with simple constructors and straightforward pattern matching. The Bool type shows enumeration-style inductive types, while Nat demonstrates recursive inductive types with constructor parameters.
Advanced Pattern Matching
More pattern matching examples illustrate the expressive power of dependent pattern matching:
#![allow(unused)] fn main() { inductive Bool : Type with | true : Bool | false : Bool inductive Nat : Type with | zero : Nat | succ : Nat -> Nat def predecessor (n : Nat) : Nat := match n with case zero => zero case succ(m) => m def not_bool (b : Bool) : Bool := match b with case true => false case false => true }
Advanced pattern matching shows how constructors with parameters can be destructured through pattern matching, with pattern variables receiving appropriate types derived from the constructor signatures. The predecessor function demonstrates recursive constructor patterns, while the not_bool function shows simple enumeration pattern matching.
Dependent Inductive Types
The implementation supports dependent inductive types where constructor types can depend on term arguments, enabling data structures:
#![allow(unused)] fn main() { inductive Nat : Type with | zero : Nat | succ : Nat -> Nat inductive Vec (A : Type) : Nat -> Type with | nil : Vec A zero | cons : (n : Nat) -> A -> Vec A n -> Vec A (succ n) }
Dependent inductive types represent the full power of inductive types in dependent type theory. These types enable length-indexed vectors, well-typed abstract syntax trees, and other data structures where types carry computational information about their contents.