Type System
Our Calculus of Constructions implementation centers around a type system that unifies terms, types, and kinds into a single syntactic framework. The implementation demonstrates how dependent types, universe polymorphism, and definitional equality work together to create a practical dependently-typed programming language.
AST Design and Term Language
The core of our implementation lies in the unified term language that represents all syntactic categories within a single AST structure. This design reflects the CoC principle that terms, types, and kinds are all inhabitants of the same computational universe.
#![allow(unused)] fn main() { use std::fmt; /// 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) } /// 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) } } /// 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>), } }
Our Term enum demonstrates the unification principle by using the same constructors to represent functions (Abs), function types (Pi), type constructors, and logical propositions. The same application constructor (App) represents both function application and type application, eliminating the artificial boundaries present in stratified type systems.
Variables (Var) and constants (Const) form the basic building blocks of our term language. Variables represent both term-level bindings and type-level bindings, while constants refer to defined names in the global context. The implementation treats both categories uniformly, enabling the same binding mechanisms to work across all abstraction levels.
Function Types and Lambda Abstractions
The Pi constructor represents dependent product types, generalizing both simple function types and universal quantification. When the bound variable appears in the body type, we obtain dependency; when it does not appear, the Pi-type reduces to a simple function type.
#![allow(unused)] fn main() { // Pi(variable_name, domain_type, codomain_type, is_implicit) Pi("x".to_string(), Box::new(nat_type), Box::new(vec_type), false) }
The boolean flag indicates whether the parameter should be treated as implicit, enabling our implementation to support both explicit and implicit argument passing. Lambda abstractions (Abs) create inhabitants of Pi-types, with the same constructor serving for both computational functions and proof terms.
Pattern Matching and Inductive Elimination
#![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, } }
Our implementation includes comprehensive pattern matching through the Match constructor, which enables elimination of inductive types. Each match arm specifies a constructor pattern and the corresponding elimination term, providing the computational content needed for inductive reasoning.
The pattern matching implementation supports nested patterns and variable bindings, enabling destructions of complex inductive data structures while maintaining type safety through exhaustiveness checking.
Universe System Implementation
The implementation includes a comprehensive universe system that prevents logical paradoxes while enabling flexible type-level computation. Our universe design supports both concrete levels and polymorphic universe variables.
#![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 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) } /// 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) } } /// 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 Levels and Arithmetic
The universe system supports multiple forms of universe expressions that enable both concrete level specifications and polymorphic universe computations. Concrete levels represented by Const(n) specify particular universe levels like Type 0, Type 1, and so forth, forming the foundation of the universe hierarchy and providing definite homes for specific types. Universe variables through ScopedVar enable universe polymorphism by allowing definitions to be parameterized over universe levels, permitting the same definition to work at multiple universe levels simultaneously. Level arithmetic operations using Add enable universe level computations such as u + 1, supporting common patterns where a type constructor must live at a universe level one higher than its parameter. Maximum operations provided by Max and IMax compute universe level selections that choose the higher of two levels, with IMax implementing the impredicative maximum used in proof-relevant contexts where the universe level computation must respect the logical structure of the proof.
Universe Constraint Solving
#![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) } /// 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) } /// 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) } } /// Universe level constraints for polymorphism #[derive(Debug, Clone, PartialEq, Eq)] pub enum UniverseConstraint { /// u ≤ v LessEq(Universe, Universe), /// u = v Equal(Universe, Universe), } }
Our implementation includes a dedicated universe constraint solver that handles the complex relationships between universe levels. The solver maintains a constraint graph and applies algorithms to determine consistent universe level assignments. The constraint solver manages level equality constraints that require two universe levels to be identical, arising from type equality requirements in dependent contexts where definitional equality demands universe level consistency. Level ordering constraints require one universe level to be strictly less than another, arising from the predicativity requirements of the type system that prevent logical paradoxes by maintaining a strict hierarchy of type universes. Arithmetic constraints involving universe level computations enable flexible universe level expressions while maintaining consistency, allowing complex universe polymorphic definitions to specify their universe requirements precisely through level arithmetic expressions that the solver can resolve to concrete level assignments.
Definitional Equality and Normalization
Our type checker implements definitional equality through a comprehensive normalization algorithm that handles β-reduction, η-expansion, and definitional unfolding of constant definitions.
#![allow(unused)] fn main() { /// Normalize a term by reducing redexes (beta reduction, eta-conversion, /// let expansion) pub fn normalize(&self, term: &Term, ctx: &Context) -> Term { match term { Term::App(f, arg) => { let f_norm = self.normalize(f, ctx); let arg_norm = self.normalize(arg, ctx); // Beta reduction: (λx.t) s ~> t[s/x] if let Term::Abs(x, _ty, body) = &f_norm { self.substitute(x, &arg_norm, body) } else { Term::App(Box::new(f_norm), Box::new(arg_norm)) } } Term::Abs(x, ty, body) => { let ty_norm = self.normalize(ty, ctx); let extended_ctx = ctx.extend(x.clone(), ty_norm.clone()); let body_norm = self.normalize(body, &extended_ctx); // Eta-conversion: λx. f x ≡ f when x is not free in f if let Term::App(f, arg) = &body_norm { if let Term::Var(arg_var) = arg.as_ref() { if arg_var == x && !Term::occurs_free(x, f) { // Apply eta-conversion: λx. f x ~> f return f.as_ref().clone(); } } } Term::Abs(x.clone(), Box::new(ty_norm), Box::new(body_norm)) } Term::Pi(x, ty, body, implicit) => { let ty_norm = self.normalize(ty, ctx); let extended_ctx = ctx.extend(x.clone(), ty_norm.clone()); let body_norm = self.normalize(body, &extended_ctx); Term::Pi(x.clone(), Box::new(ty_norm), Box::new(body_norm), *implicit) } Term::Let(x, _ty, val, body) => { // Let reduction: let x : T := v in b ~> b[v/x] let val_norm = self.normalize(val, ctx); self.substitute(x, &val_norm, body) } Term::Var(x) => { // Look up definitions and unfold them if let Some(def) = ctx.lookup_axiom(x) { def.clone() // Could be further normalized if it's a // definition } else { term.clone() } } _ => term.clone(), // Other terms are already in normal form } } }
The normalization algorithm implements β-reduction for function applications, handling both computational reductions and type-level computations. When a lambda abstraction is applied to an argument, the implementation performs substitution while carefully managing variable capture and scope.
\[ (λx : Nat. x + 1) \ 5 ⟹ 5 + 1 ⟹ 6 \]
The implementation extends β-reduction to handle dependent type computations, where type-level functions can be applied to produce new types through computation.
Eta Conversion
Eta conversion ensures that functions are equal to their eta-expanded forms, providing extensional equality for function types. The implementation applies η-expansion during normalization to ensure that definitionally equal terms are recognized as such.
\[ λx : A. f \ x ≡ f \text{ (when } x \notin \text{fv}(f)\text{)} \]
Let-Expansion and Definition Unfolding
The implementation handles let bindings through expansion, replacing let-bound variables with their definitions during normalization. This approach ensures that local definitions do not interfere with definitional equality while providing the computational content needed for type checking.
Definition unfolding enables the type checker to access the computational content of defined constants, allowing definitional equality to work across module boundaries and enabling powerful abstraction mechanisms.
Type Checking Algorithm
Our implementation employs bidirectional type checking that splits the type checking problem into synthesis and checking modes. This approach handles the complexity of dependent types while maintaining decidability and providing informative error messages.
#![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)) } }
Type Synthesis
The synthesis algorithm determines the type of a term by analyzing its structure and propagating type information through the syntax tree. Variable lookup operates by consulting the typing context, which maintains bindings for both term variables and type variables, ensuring that each variable reference corresponds to a valid binding in the current scope. Function application typing proceeds by synthesizing the function type, ensuring it forms a Pi-type, and checking that the argument type matches the domain specification, with careful handling of dependent types where the codomain may depend on the specific argument value. Pi-type formation verification ensures both the domain and codomain are well-typed, with the codomain checked in a context extended with the bound variable to properly handle the dependency relationship between the domain and codomain types.
#![allow(unused)] fn main() { /// Check that a term has a given type pub fn check(&mut self, term: &Term, ty: &Term, ctx: &Context) -> TypeResult<()> { // Special handling for checking against meta-variable types if let Term::Meta(_) = ty { // When checking against a meta-variable, infer the term's type and unify let _inferred = self.infer(term, ctx)?; // For now, just check they're compatible - in a full system we'd unify // and update the meta-variable return Ok(()); } match term { Term::Abs(x, param_ty, body) => { // Check if ty is a Pi-type if let Term::Pi(y, expected_param_ty, expected_body_ty, _impl) = ty { // Handle holes in parameter type let actual_param_ty = match param_ty.as_ref() { Term::Meta(name) if name == UNDERSCORE => { // Hole in parameter type - use the expected type expected_param_ty.clone() } _ => param_ty.clone(), }; // Check parameter types are definitionally equal (with conversion) if !self.definitionally_equal(&actual_param_ty, expected_param_ty, ctx)? { return Err(TypeError::TypeMismatch { expected: expected_param_ty.as_ref().clone(), actual: actual_param_ty.as_ref().clone(), }); } // Check body in extended context let extended_ctx = ctx.extend(x.clone(), actual_param_ty.as_ref().clone()); // Substitute parameter in expected body type - this is the key for dependent // types let expected_body_ty = if x == y { expected_body_ty.as_ref().clone() } else { // Rename bound variable y to x in the body type self.substitute(y, &Term::Var(x.clone()), expected_body_ty) }; self.check(body, &expected_body_ty, &extended_ctx) } else { Err(TypeError::NotAFunction { term: term.clone(), ty: ty.clone(), }) } } _ => { // General case: infer type and check definitional equivalence let inferred_ty = self.infer(term, ctx)?; // Handle implicit parameters: if inferred type has implicit params, // try to instantiate them to match the expected type let elaborated_ty = self.elaborate_implicit_parameters(&inferred_ty, ty, ctx)?; // Check definitional equivalence if self.definitionally_equal(&elaborated_ty, ty, ctx)? { Ok(()) } else { Err(TypeError::TypeMismatch { expected: ty.clone(), actual: elaborated_ty, }) } } } } }
Type Checking Mode
The checking algorithm verifies that a term has an expected type by comparing the term structure with the type structure. This mode often provides better error messages and more efficient checking for terms with complex dependent types. Lambda checking operates by verifying lambda abstractions against Pi-types, ensuring that the body has the correct type in the extended context where the lambda parameter is properly bound. When synthesis and checking produce different results, the algorithm falls back to definitional equality checking, normalizing both the synthesized and expected types to their canonical forms and comparing the results, enabling the type checker to recognize when terms are definitionally equal despite having different syntactic representations.
Context Management
#![allow(unused)] fn main() { use std::collections::HashMap; use crate::ast::{Term, Universe, UniverseConstraint, UniverseContext}; /// Definition with universe parameters #[derive(Debug, Clone, PartialEq)] pub struct Definition { /// Universe parameters for the definition pub universe_params: Vec<String>, /// The type of the definition pub ty: Term, /// Name of the definition (for scoping universe parameters) pub name: String, } impl Context { pub fn new() -> Self { Context { bindings: HashMap::new(), universe_vars: HashMap::new(), constructors: HashMap::new(), axioms: HashMap::new(), definitions: HashMap::new(), universe_context: UniverseContext::new(), } } /// Extend context with variable binding pub fn extend(&self, var: String, ty: Term) -> Self { let mut new_ctx = self.clone(); new_ctx.bindings.insert(var, ty); new_ctx } /// Extend context with multiple bindings pub fn extend_many(&self, bindings: Vec<(String, Term)>) -> Self { let mut new_ctx = self.clone(); for (var, ty) in bindings { new_ctx.bindings.insert(var, ty); } new_ctx } /// Look up variable type pub fn lookup(&self, var: &str) -> Option<&Term> { self.bindings.get(var) } /// Check if context has a binding for the given variable pub fn has_binding(&self, var: &str) -> bool { self.bindings.contains_key(var) } /// Get all variable bindings pub fn get_all_bindings(&self) -> impl Iterator<Item = (&String, &Term)> { self.bindings.iter() } /// Look up constructor type pub fn lookup_constructor(&self, name: &str) -> Option<&Term> { self.constructors.get(name) } /// Look up axiom type pub fn lookup_axiom(&self, name: &str) -> Option<&Term> { self.axioms.get(name) } /// Add constructor definition pub fn add_constructor(&mut self, name: String, ty: Term) { self.constructors.insert(name, ty); } /// Add axiom definition pub fn add_axiom(&mut self, name: String, ty: Term) { self.axioms.insert(name, ty); } /// Add definition with universe parameters pub fn add_definition(&mut self, name: String, universe_params: Vec<String>, ty: Term) { self.definitions.insert( name.clone(), Definition { universe_params, ty, name: name.clone(), }, ); } /// Look up definition with universe parameters pub fn lookup_definition(&self, name: &str) -> Option<&Definition> { self.definitions.get(name) } /// Add universe variable constraint pub fn add_universe_var(&mut self, var: String, constraint: Universe) { self.universe_vars.insert(var, constraint); } /// Check if variable is bound in context pub fn contains(&self, var: &str) -> bool { self.bindings.contains_key(var) } /// Get all variable names pub fn variables(&self) -> Vec<&String> { self.bindings.keys().collect() } /// Remove variable from context pub fn remove(&self, var: &str) -> Self { let mut new_ctx = self.clone(); new_ctx.bindings.remove(var); new_ctx } /// Get fresh variable name not in context pub fn fresh_var(&self, base: &str) -> String { let mut counter = 0; loop { let candidate = if counter == 0 { base.to_string() } else { format!("{}{}", base, counter) }; if !self.contains(&candidate) { return candidate; } counter += 1; } } /// Access universe context pub fn universe_context(&self) -> &UniverseContext { &self.universe_context } /// Extend context with universe variable pub fn extend_universe(&self, name: String) -> Self { let mut new_ctx = self.clone(); new_ctx.universe_context.add_var(name); new_ctx } /// Extend context with multiple universe variables pub fn extend_universe_many(&self, names: Vec<String>) -> Self { let mut new_ctx = self.clone(); for name in names { new_ctx.universe_context.add_var(name); } new_ctx } /// Add universe constraint pub fn add_universe_constraint(&mut self, constraint: UniverseConstraint) { self.universe_context.add_constraint(constraint); } /// Generate fresh universe variable pub fn fresh_universe_var(&self, base: &str) -> String { self.universe_context.fresh_var(base) } } impl Default for Context { fn default() -> Self { Self::new() } } /// Type checking errors related to context #[derive(Debug, Clone, PartialEq)] pub enum ContextError { UnboundVariable { name: String }, UnboundConstructor { name: String }, UnboundAxiom { name: String }, VariableAlreadyBound { name: String }, } impl std::fmt::Display for ContextError { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { ContextError::UnboundVariable { name } => { write!(f, "Unbound variable: {}", name) } ContextError::UnboundConstructor { name } => { write!(f, "Unbound constructor: {}", name) } ContextError::UnboundAxiom { name } => { write!(f, "Unbound axiom: {}", name) } ContextError::VariableAlreadyBound { name } => { write!(f, "Variable already bound: {}", name) } } } } impl std::error::Error for ContextError {} #[cfg(test)] mod tests { use super::*; use crate::ast::Universe; #[test] fn test_context_operations() { let ctx = Context::new(); let var_type = Term::Sort(Universe::Const(0)); let ctx2 = ctx.extend("x".to_string(), var_type.clone()); assert!(ctx2.contains("x")); assert_eq!(ctx2.lookup("x"), Some(&var_type)); assert!(!ctx.contains("x")); // Original context unchanged } #[test] fn test_fresh_var() { let mut ctx = Context::new(); ctx.bindings .insert("x".to_string(), Term::Sort(Universe::Const(0))); ctx.bindings .insert("x1".to_string(), Term::Sort(Universe::Const(0))); let fresh = ctx.fresh_var("x"); assert_eq!(fresh, "x2"); let fresh2 = ctx.fresh_var("y"); assert_eq!(fresh2, "y"); } #[test] fn test_extend_many() { let ctx = Context::new(); let bindings = vec![ ("x".to_string(), Term::Sort(Universe::Const(0))), ("y".to_string(), Term::Sort(Universe::Const(1))), ]; let ctx2 = ctx.extend_many(bindings); assert!(ctx2.contains("x")); assert!(ctx2.contains("y")); } } /// Type checking context containing variable bindings #[derive(Debug, Clone, PartialEq)] pub struct Context { /// Variable to type bindings bindings: HashMap<String, Term>, /// Universe variable constraints universe_vars: HashMap<String, Universe>, /// Constructor definitions constructors: HashMap<String, Term>, /// Axiom definitions (without universe params - for backwards compat) axioms: HashMap<String, Term>, /// Definitions with universe parameters definitions: HashMap<String, Definition>, /// Universe level context for polymorphism universe_context: UniverseContext, } }
The typing context maintains bindings for variables, definitions, axioms, and constructors. Our implementation uses a context structure that enables efficient lookup while supporting the complex scoping rules required for dependent types. Variable binding operations add new variable bindings with their types, enabling proper scoping in lambda abstractions and Pi-types where the bound variable may appear in the type of subsequent bindings. Definition extension capabilities allow adding new constant definitions with their types and bodies, enabling modular development and abstraction mechanisms that support large-scale program organization. Constructor registration functionality registers inductive type constructors with their types, enabling pattern matching and inductive reasoning that respects the structural properties of the data types and maintains type safety throughout elimination operations.
Implicit Arguments and Elaboration
Our implementation includes comprehensive support for implicit arguments that are automatically inferred by the type checker. This feature bridges the gap between the fully explicit internal representation and the more convenient surface syntax.
#![allow(unused)] fn main() { /// Elaborate implicit parameters by trying to instantiate them to match /// expected type This is a simple version that handles common cases /// without full constraint solving fn elaborate_implicit_parameters( &mut self, inferred_ty: &Term, expected_ty: &Term, ctx: &Context, ) -> TypeResult<Term> { // If inferred type has implicit parameters, try to instantiate them match inferred_ty { Term::Pi(param_name, param_ty, body_ty, true) => { // This is an implicit parameter - try to infer what it should be let implicit_arg = self.infer_implicit_argument(param_ty, expected_ty, ctx)?; // Substitute the implicit argument and continue elaboration let instantiated_ty = self.substitute(param_name, &implicit_arg, body_ty); self.elaborate_implicit_parameters(&instantiated_ty, expected_ty, ctx) } _ => { // No more implicit parameters, return the type as-is Ok(inferred_ty.clone()) } } } }
Implicit Argument Insertion
The type checker automatically inserts implicit arguments when encountering function applications where the function type has implicit parameters. Meta-variable generation creates fresh meta-variables to represent unknown implicit arguments, ensuring that each implicit parameter has a unique placeholder that can be resolved through subsequent constraint solving. Constraint collection gathers relationships that connect meta-variables to known type information, building a system of equations that captures the interdependencies between implicit arguments and the explicitly provided terms. Constraint solving employs the dedicated constraint solver to determine concrete values for meta-variables, using unification algorithms and type-directed search to find solutions that satisfy all accumulated constraints while respecting the type structure of the program.
Meta-variable Resolution
#![allow(unused)] fn main() { use std::collections::{HashMap, HashSet, VecDeque}; use std::fmt; use crate::ast::{Term, Universe}; use crate::context::Context; use crate::errors::TypeError; /// Meta-variable identifier #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct MetaId(pub u64); impl fmt::Display for MetaId { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "?m{}", self.0) } } /// Universe meta-variable identifier #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct UniverseMetaId(pub u64); impl fmt::Display for UniverseMetaId { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "?u{}", self.0) } } /// Constraint identifier #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct ConstraintId(pub u64); /// Constraint types #[derive(Debug, Clone)] pub enum Constraint { /// Unification: t1 ≡ t2 Unify { id: ConstraintId, left: Term, right: Term, strength: ConstraintStrength, }, /// Type constraint: term : type HasType { id: ConstraintId, term: Term, expected_type: Term, }, /// Universe unification: u1 ≡ u2 UnifyUniverse { id: ConstraintId, left: Universe, right: Universe, strength: ConstraintStrength, }, /// Universe level constraint: u1 ≤ u2 UniverseLevel { id: ConstraintId, left: Universe, right: Universe, }, /// Delayed constraint (for complex patterns) Delayed { id: ConstraintId, constraint: Box<Constraint>, waiting_on: HashSet<MetaId>, }, } /// Constraint strength for prioritization #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum ConstraintStrength { Required, // Must be solved Preferred, // Should be solved if possible Weak, // Can be postponed } /// Substitution mapping meta-variables to terms #[derive(Debug, Clone, Default)] pub struct Substitution { mapping: HashMap<MetaId, Term>, universe_mapping: HashMap<u32, Universe>, } impl Substitution { pub fn new() -> Self { Self::default() } pub fn insert(&mut self, meta: MetaId, term: Term) { self.mapping.insert(meta, term); } pub fn get(&self, meta: &MetaId) -> Option<&Term> { self.mapping.get(meta) } pub fn insert_universe(&mut self, meta_id: u32, universe: Universe) { self.universe_mapping.insert(meta_id, universe); } pub fn get_universe(&self, meta_id: &u32) -> Option<&Universe> { self.universe_mapping.get(meta_id) } /// Apply substitution to a term pub fn apply(&self, term: &Term) -> Term { match term { Term::Meta(name) => { // Try to parse meta ID and look up substitution if let Some(meta_id) = self.parse_meta_name(name) { if let Some(subst) = self.mapping.get(&meta_id) { // Recursively apply substitution return self.apply(subst); } } term.clone() } Term::App(f, arg) => Term::App(Box::new(self.apply(f)), Box::new(self.apply(arg))), Term::Abs(x, ty, body) => Term::Abs( x.clone(), Box::new(self.apply(ty)), Box::new(self.apply(body)), ), Term::Pi(x, ty, body, implicit) => Term::Pi( x.clone(), Box::new(self.apply(ty)), Box::new(self.apply(body)), *implicit, ), Term::Let(x, ty, val, body) => Term::Let( x.clone(), Box::new(self.apply(ty)), Box::new(self.apply(val)), Box::new(self.apply(body)), ), Term::Sort(u) => Term::Sort(self.apply_universe(u)), // Other cases remain unchanged _ => term.clone(), } } /// Apply substitution to a universe pub fn apply_universe(&self, universe: &Universe) -> Universe { let result = match universe { Universe::Meta(id) => { if let Some(subst) = self.universe_mapping.get(id) { // Recursively apply substitution self.apply_universe(subst) } else { universe.clone() } } Universe::Add(base, n) => Universe::Add(Box::new(self.apply_universe(base)), *n), Universe::Max(u, v) => Universe::Max( Box::new(self.apply_universe(u)), Box::new(self.apply_universe(v)), ), Universe::IMax(u, v) => Universe::IMax( Box::new(self.apply_universe(u)), Box::new(self.apply_universe(v)), ), // Constants, variables, and scoped variables remain unchanged during substitution Universe::Const(_) | Universe::ScopedVar(_, _) => universe.clone(), }; // Normalize the result to simplify expressions like Const(0) + 1 -> Const(1) self.normalize_universe_static(&result) } /// Static normalization fn normalize_universe_static(&self, u: &Universe) -> Universe { match u { Universe::Add(base, n) => { let base_norm = self.normalize_universe_static(base); match base_norm { Universe::Const(m) => Universe::Const(m + n), _ => Universe::Add(Box::new(base_norm), *n), } } Universe::Max(u1, u2) => { let u1_norm = self.normalize_universe_static(u1); let u2_norm = self.normalize_universe_static(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(), } } fn parse_meta_name(&self, name: &str) -> Option<MetaId> { if let Some(stripped) = name.strip_prefix("?m") { stripped.parse::<u64>().ok().map(MetaId) } else { None } } } /// Advanced constraint solver with dependency tracking pub struct Solver { /// Meta-variables metas: HashMap<MetaId, MetaInfo>, /// Active constraints constraints: HashMap<ConstraintId, Constraint>, /// Constraint queue (ordered by priority) queue: VecDeque<ConstraintId>, /// Solved substitutions substitution: Substitution, /// Next meta ID next_meta_id: u64, /// Next universe meta ID next_universe_meta_id: u32, /// Next constraint ID next_constraint_id: u64, /// Type checking context context: Context, /// Dependency graph: meta -> constraints that depend on it dependencies: HashMap<MetaId, HashSet<ConstraintId>>, /// Delayed constraints that couldn't be solved immediately delayed_constraints: HashSet<ConstraintId>, /// Recursion depth counter to prevent stack overflow recursion_depth: u32, /// Flag to enable Miller pattern solving (advanced) enable_miller_patterns: bool, /// Flag to enable HasType constraint solving (advanced) enable_has_type_solving: bool, } impl Solver { pub fn new(context: Context) -> Self { Self { metas: HashMap::new(), constraints: HashMap::new(), queue: VecDeque::new(), substitution: Substitution::new(), next_meta_id: 0, next_universe_meta_id: 0, next_constraint_id: 0, context, dependencies: HashMap::new(), delayed_constraints: HashSet::new(), recursion_depth: 0, enable_miller_patterns: false, // Advanced feature enable_has_type_solving: false, // Advanced feature } } /// Enable Miller pattern solving (advanced) pub fn enable_miller_patterns(&mut self) { self.enable_miller_patterns = true; } /// Check if Miller pattern solving is enabled pub fn miller_patterns_enabled(&self) -> bool { self.enable_miller_patterns } /// Enable HasType constraint solving (advanced) pub fn enable_has_type_solving(&mut self) { self.enable_has_type_solving = true; } /// Check if HasType constraint solving is enabled pub fn has_type_solving_enabled(&self) -> bool { self.enable_has_type_solving } /// Create a fresh meta-variable pub fn fresh_meta(&mut self, ctx_vars: Vec<String>, expected_type: Option<Term>) -> MetaId { let id = MetaId(self.next_meta_id); self.next_meta_id += 1; let info = MetaInfo { id, context: ctx_vars, expected_type, solution: None, dependencies: HashSet::new(), occurrences: Vec::new(), }; self.metas.insert(id, info); id } /// Create a fresh universe meta-variable pub fn fresh_universe_meta(&mut self) -> Universe { let id = self.next_universe_meta_id; self.next_universe_meta_id += 1; Universe::Meta(id) } /// Add a constraint to the solver pub fn add_constraint(&mut self, constraint: Constraint) -> ConstraintId { let id = match &constraint { Constraint::Unify { id, .. } | Constraint::HasType { id, .. } | Constraint::UnifyUniverse { id, .. } | Constraint::UniverseLevel { id, .. } | Constraint::Delayed { id, .. } => *id, }; // Track which metas appear in this constraint self.track_meta_occurrences(&constraint); self.constraints.insert(id, constraint); self.queue.push_back(id); id } /// Create a new constraint ID pub fn new_constraint_id(&mut self) -> ConstraintId { let id = ConstraintId(self.next_constraint_id); self.next_constraint_id += 1; id } /// Track meta-variable occurrences in constraints fn track_meta_occurrences(&mut self, constraint: &Constraint) { let metas = self.collect_metas_in_constraint(constraint); let constraint_id = match constraint { Constraint::Unify { id, .. } | Constraint::HasType { id, .. } | Constraint::UnifyUniverse { id, .. } | Constraint::UniverseLevel { id, .. } | Constraint::Delayed { id, .. } => *id, }; for meta_id in metas { if let Some(info) = self.metas.get_mut(&meta_id) { info.occurrences.push(constraint_id); } self.dependencies .entry(meta_id) .or_default() .insert(constraint_id); } } /// Collect all meta-variables in a constraint fn collect_metas_in_constraint(&self, constraint: &Constraint) -> HashSet<MetaId> { match constraint { Constraint::Unify { left, right, .. } => { let mut metas = self.collect_metas_in_term(left); metas.extend(self.collect_metas_in_term(right)); metas } Constraint::HasType { term, expected_type, .. } => { let mut metas = self.collect_metas_in_term(term); metas.extend(self.collect_metas_in_term(expected_type)); metas } Constraint::UnifyUniverse { .. } => { // Universe constraints don't directly contain term meta-variables // but they might contain universe meta-variables (which we track separately) HashSet::new() } Constraint::UniverseLevel { .. } => { // Same as above HashSet::new() } Constraint::Delayed { constraint, waiting_on, .. } => { let mut metas = waiting_on.clone(); metas.extend(self.collect_metas_in_constraint(constraint)); metas } } } /// Collect all meta-variables in a term fn collect_metas_in_term(&self, term: &Term) -> HashSet<MetaId> { let mut metas = HashSet::new(); self.collect_metas_recursive(term, &mut metas); metas } fn collect_metas_recursive(&self, term: &Term, metas: &mut HashSet<MetaId>) { match term { Term::Meta(name) => { if let Some(id) = self.parse_meta_name(name) { metas.insert(id); } } Term::App(f, arg) => { self.collect_metas_recursive(f, metas); self.collect_metas_recursive(arg, metas); } Term::Abs(_, ty, body) | Term::Pi(_, ty, body, _) => { self.collect_metas_recursive(ty, metas); self.collect_metas_recursive(body, metas); } Term::Let(_, ty, val, body) => { self.collect_metas_recursive(ty, metas); self.collect_metas_recursive(val, metas); self.collect_metas_recursive(body, metas); } _ => {} } } fn parse_meta_name(&self, name: &str) -> Option<MetaId> { if let Some(stripped) = name.strip_prefix("?m") { stripped.parse::<u64>().ok().map(MetaId) } else { None } } /// Main solving loop pub fn solve(&mut self) -> Result<Substitution, TypeError> { let max_iterations = 1000; let mut iterations = 0; while !self.queue.is_empty() && iterations < max_iterations { iterations += 1; // Pick the best constraint to solve if let Some(constraint_id) = self.pick_constraint() { let constraint = self.constraints .remove(&constraint_id) .ok_or_else(|| TypeError::Internal { message: "Constraint disappeared".to_string(), })?; match self.solve_constraint(constraint.clone()) { Ok(progress) => { if progress { // Propagate the solution self.propagate_solution()?; // Wake up delayed constraints that might now be solvable let woken_constraints = self.wake_delayed_constraints()?; // Add woken constraints back to queue with high priority for woken_id in woken_constraints { self.queue.push_front(woken_id); } } } Err(e) => { // Try to delay the constraint if possible if self.can_delay(&constraint_id) { // Determine which meta-variables to wait for let waiting_on = match &constraint { Constraint::Unify { left, right, .. } => { let mut metas = self.collect_metas_in_term(left); metas.extend(self.collect_metas_in_term(right)); metas .into_iter() .filter(|meta_id| self.is_unsolved_meta(meta_id)) .collect() } Constraint::HasType { term, expected_type, .. } => { let mut metas = self.collect_metas_in_term(term); metas.extend(self.collect_metas_in_term(expected_type)); metas .into_iter() .filter(|meta_id| self.is_unsolved_meta(meta_id)) .collect() } _ => HashSet::new(), }; if !waiting_on.is_empty() { // Put constraint back and delay it self.constraints.insert(constraint_id, constraint); self.delay_constraint(constraint_id, waiting_on)?; } else { // Can't delay, return error return Err(e); } } else { return Err(e); } } } } } if iterations >= max_iterations { return Err(TypeError::Internal { message: "Constraint solving did not converge".to_string(), }); } // Check for unsolved required constraints for constraint in self.constraints.values() { if let Constraint::Unify { strength: ConstraintStrength::Required, .. } = constraint { return Err(TypeError::Internal { message: "Unsolved required constraints remain".to_string(), }); } } Ok(self.substitution.clone()) } /// Pick the next constraint to solve based on heuristics fn pick_constraint(&mut self) -> Option<ConstraintId> { // Priority order: // 1. Constraints with no meta-variables // 2. Constraints with only solved meta-variables // 3. Simple pattern constraints (Miller patterns) // 4. Other constraints let mut best_constraint = None; let mut best_score = i32::MAX; for &id in &self.queue { if let Some(constraint) = self.constraints.get(&id) { let score = self.score_constraint(constraint); if score < best_score { best_score = score; best_constraint = Some(id); } } } if let Some(id) = best_constraint { self.queue.retain(|&x| x != id); Some(id) } else { self.queue.pop_front() } } /// Score a constraint for solving priority (lower is better) fn score_constraint(&self, constraint: &Constraint) -> i32 { let metas = self.collect_metas_in_constraint(constraint); if metas.is_empty() { return 0; // No metas, can solve immediately } let unsolved_count = metas .iter() .filter(|m| { self.metas .get(m) .and_then(|info| info.solution.as_ref()) .is_none() }) .count(); if unsolved_count == 0 { return 1; // All metas solved } // Check for Miller patterns if let Constraint::Unify { left, right, .. } = constraint { if self.is_miller_pattern_unification(left, right) || self.is_miller_pattern_unification(right, left) { return 10 + unsolved_count as i32; } } 100 + unsolved_count as i32 } /// Check if a unification is a Miller pattern (?M x1 ... xn = t) fn is_miller_pattern_unification(&self, left: &Term, right: &Term) -> bool { self.is_simple_miller_pattern(left, right) } /// Check if left is a simple Miller pattern and right is safe to solve with pub fn is_simple_miller_pattern(&self, left: &Term, right: &Term) -> bool { let (head, args) = self.decompose_application(left); if let Term::Meta(meta_name) = head { // Must have at least one argument to be interesting if args.is_empty() { return false; } // Check if all arguments are distinct variables let mut seen = HashSet::new(); for arg in &args { if let Term::Var(x) = arg { if !seen.insert(x.clone()) { return false; // Not distinct } } else { return false; // Not a variable } } // Check occurs check - right must not contain the meta-variable if let Some(meta_id) = self.parse_meta_name(meta_name) { if self.collect_metas_in_term(right).contains(&meta_id) { return false; // Occurs check failure } } // For now, only handle simple cases where right is a variable or constant match right { Term::Var(_) | Term::Const(_) | Term::Sort(_) => true, Term::Meta(_) => { // Allow meta-to-meta if they're different if let Term::Meta(right_name) = right { meta_name != right_name } else { false } } _ => false, // More complex cases need careful handling } } else { false } } /// Decompose an application into head and arguments fn decompose_application<'a>(&self, term: &'a Term) -> (&'a Term, Vec<&'a Term>) { let mut current = term; let mut args = Vec::new(); while let Term::App(f, arg) = current { args.push(arg.as_ref()); current = f; } args.reverse(); (current, args) } /// Solve a single constraint fn solve_constraint(&mut self, constraint: Constraint) -> Result<bool, TypeError> { const MAX_RECURSION_DEPTH: u32 = 100; if self.recursion_depth >= MAX_RECURSION_DEPTH { return Err(TypeError::Internal { message: format!( "Maximum recursion depth {} exceeded in solve_constraint", MAX_RECURSION_DEPTH ), }); } self.recursion_depth += 1; let result = self.solve_constraint_impl(constraint); self.recursion_depth -= 1; result } fn solve_constraint_impl(&mut self, constraint: Constraint) -> Result<bool, TypeError> { match constraint { Constraint::Unify { left, right, strength, .. } => self.unify(&left, &right, strength), Constraint::HasType { term, expected_type, .. } => { if self.enable_has_type_solving { self.solve_has_type_constraint(&term, &expected_type) } else { // Default behavior: don't solve HasType constraints Ok(false) } } Constraint::UnifyUniverse { left, right, strength, .. } => self.unify_universe(&left, &right, strength), Constraint::UniverseLevel { left, right, .. } => { // For now, treat level constraints as unification constraints self.unify_universe(&left, &right, ConstraintStrength::Preferred) } Constraint::Delayed { constraint, .. } => { // Re-queue the delayed constraint let inner = *constraint; self.add_constraint(inner); Ok(false) } } } /// Unify two terms fn unify( &mut self, left: &Term, right: &Term, strength: ConstraintStrength, ) -> Result<bool, TypeError> { const MAX_RECURSION_DEPTH: u32 = 50; if self.recursion_depth >= MAX_RECURSION_DEPTH { return Err(TypeError::Internal { message: format!( "Maximum recursion depth {} exceeded in unify", MAX_RECURSION_DEPTH ), }); } self.recursion_depth += 1; let result = self.unify_impl(left, right, strength); self.recursion_depth -= 1; result } fn unify_impl( &mut self, left: &Term, right: &Term, strength: ConstraintStrength, ) -> Result<bool, TypeError> { // Apply current substitution let left = self.substitution.apply(left); let right = self.substitution.apply(right); // Check if already equal if self.alpha_equal(&left, &right) { return Ok(false); } // Miller pattern detection and solving (if enabled) if self.enable_miller_patterns { if self.is_simple_miller_pattern(&left, &right) { if let Some((meta_name, spine)) = self.extract_miller_spine(&left) { // Try to solve the Miller pattern directly return self.solve_miller_pattern(&meta_name, &spine, &right); } } else if self.is_simple_miller_pattern(&right, &left) { if let Some((meta_name, spine)) = self.extract_miller_spine(&right) { // Try to solve the Miller pattern directly return self.solve_miller_pattern(&meta_name, &spine, &left); } } } match (&left, &right) { // Meta-variable cases (Term::Meta(m), t) | (t, Term::Meta(m)) => { if let Some(meta_id) = self.parse_meta_name(m) { self.solve_meta(meta_id, t) } else { Err(TypeError::Internal { message: format!("Invalid meta-variable: {}", m), }) } } // Structural cases (Term::App(f1, a1), Term::App(f2, a2)) => { let id1 = self.new_constraint_id(); let id2 = self.new_constraint_id(); self.add_constraint(Constraint::Unify { id: id1, left: *f1.clone(), right: *f2.clone(), strength, }); self.add_constraint(Constraint::Unify { id: id2, left: *a1.clone(), right: *a2.clone(), strength, }); Ok(true) } (Term::Pi(x1, t1, b1, i1), Term::Pi(x2, t2, b2, i2)) if i1 == i2 => { let id1 = self.new_constraint_id(); let id2 = self.new_constraint_id(); self.add_constraint(Constraint::Unify { id: id1, left: *t1.clone(), right: *t2.clone(), strength, }); // Rename bound variables to be consistent let fresh_var = format!("x{}", self.next_meta_id); let b1_renamed = self.rename_var(x1, &fresh_var, b1); let b2_renamed = self.rename_var(x2, &fresh_var, b2); self.add_constraint(Constraint::Unify { id: id2, left: b1_renamed, right: b2_renamed, strength, }); Ok(true) } (Term::Abs(x1, t1, b1), Term::Abs(x2, t2, b2)) => { let id1 = self.new_constraint_id(); let id2 = self.new_constraint_id(); self.add_constraint(Constraint::Unify { id: id1, left: *t1.clone(), right: *t2.clone(), strength, }); let fresh_var = format!("x{}", self.next_meta_id); let b1_renamed = self.rename_var(x1, &fresh_var, b1); let b2_renamed = self.rename_var(x2, &fresh_var, b2); self.add_constraint(Constraint::Unify { id: id2, left: b1_renamed, right: b2_renamed, strength, }); Ok(true) } // Universe (Sort) cases (Term::Sort(u1), Term::Sort(u2)) => self.unify_universe(u1, u2, strength), _ => { if strength == ConstraintStrength::Required { Err(TypeError::TypeMismatch { expected: left, actual: right, }) } else { Ok(false) // Can't solve, but not an error for weak // constraints } } } } /// Unify two universes fn unify_universe( &mut self, left: &Universe, right: &Universe, strength: ConstraintStrength, ) -> Result<bool, TypeError> { // Apply current substitution let left = self.substitution.apply_universe(left); let right = self.substitution.apply_universe(right); // Normalize universes (simplify expressions like 0+1 -> 1) let left = self.normalize_universe(&left); let right = self.normalize_universe(&right); // Check if already equal if left == right { return Ok(false); } match (&left, &right) { // Same constants (Universe::Const(n1), Universe::Const(n2)) if n1 == n2 => Ok(false), // Universe variable cases (Universe::ScopedVar(s1, v1), Universe::ScopedVar(s2, v2)) if s1 == s2 && v1 == v2 => { Ok(false) } (Universe::ScopedVar(_, _), Universe::ScopedVar(_, _)) => { // Different universe variables cannot be unified if strength == ConstraintStrength::Required { Err(TypeError::Internal { message: format!( "Cannot unify distinct universe variables {} and {}", left, right ), }) } else { Ok(false) } } // Meta-variable cases (Universe::Meta(id), u) | (u, Universe::Meta(id)) => self.solve_universe_meta(*id, u), // Structural cases (Universe::Add(base1, n1), Universe::Add(base2, n2)) if n1 == n2 => { let constraint_id = self.new_constraint_id(); self.add_constraint(Constraint::UnifyUniverse { id: constraint_id, left: *base1.clone(), right: *base2.clone(), strength, }); Ok(true) } // Arithmetic constraints: ?u+n = m means ?u = m-n (Universe::Add(base, n), Universe::Const(m)) | (Universe::Const(m), Universe::Add(base, n)) => { if *m >= *n { if let Universe::Meta(id) = base.as_ref() { self.solve_universe_meta(*id, &Universe::Const(m - n)) } else { // More complex case - generate constraint for base let constraint_id = self.new_constraint_id(); self.add_constraint(Constraint::UnifyUniverse { id: constraint_id, left: *base.clone(), right: Universe::Const(m - n), strength, }); Ok(true) } } else { Err(TypeError::Internal { message: format!("Cannot solve constraint: {} cannot equal {} (would require negative universe)", if matches!(&left, Universe::Add(_, _)) { &left } else { &right }, if matches!(&left, Universe::Const(_)) { &left } else { &right }), }) } } (Universe::Max(u1, v1), Universe::Max(u2, v2)) => { let id1 = self.new_constraint_id(); let id2 = self.new_constraint_id(); self.add_constraint(Constraint::UnifyUniverse { id: id1, left: *u1.clone(), right: *u2.clone(), strength, }); self.add_constraint(Constraint::UnifyUniverse { id: id2, left: *v1.clone(), right: *v2.clone(), strength, }); Ok(true) } (Universe::IMax(u1, v1), Universe::IMax(u2, v2)) => { let id1 = self.new_constraint_id(); let id2 = self.new_constraint_id(); self.add_constraint(Constraint::UnifyUniverse { id: id1, left: *u1.clone(), right: *u2.clone(), strength, }); self.add_constraint(Constraint::UnifyUniverse { id: id2, left: *v1.clone(), right: *v2.clone(), strength, }); Ok(true) } _ => { if strength == ConstraintStrength::Required { Err(TypeError::Internal { message: format!("Cannot unify universes {} and {}", left, right), }) } else { Ok(false) } } } } /// Normalize a universe expression fn normalize_universe(&self, u: &Universe) -> Universe { match u { Universe::Add(base, n) => { let base_norm = self.normalize_universe(base); match base_norm { Universe::Const(m) => Universe::Const(m + n), _ => Universe::Add(Box::new(base_norm), *n), } } Universe::Max(u1, u2) => { let u1_norm = self.normalize_universe(u1); let u2_norm = self.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(), } } /// Solve a universe meta-variable fn solve_universe_meta( &mut self, meta_id: u32, solution: &Universe, ) -> Result<bool, TypeError> { // Occurs check for universe meta-variables if self.occurs_in_universe(meta_id, solution) { return Err(TypeError::Internal { message: format!("Universe occurs check failed for ?u{}", meta_id), }); } // Record solution self.substitution.insert_universe(meta_id, solution.clone()); Ok(true) } /// Check if a universe meta-variable occurs in a universe expression fn occurs_in_universe(&self, meta_id: u32, universe: &Universe) -> bool { match universe { Universe::Meta(id) => *id == meta_id, Universe::Add(base, _) => self.occurs_in_universe(meta_id, base), Universe::Max(u, v) | Universe::IMax(u, v) => { self.occurs_in_universe(meta_id, u) || self.occurs_in_universe(meta_id, v) } _ => false, } } /// Solve a meta-variable fn solve_meta(&mut self, meta_id: MetaId, solution: &Term) -> Result<bool, TypeError> { // Occurs check if self.collect_metas_in_term(solution).contains(&meta_id) { return Err(TypeError::Internal { message: format!("Occurs check failed for ?m{}", meta_id.0), }); } // Check solution is well-scoped if let Some(meta_info) = self.metas.get(&meta_id) { if !self.is_well_scoped(solution, &meta_info.context) { return Err(TypeError::Internal { message: format!("Solution for ?m{} is not well-scoped", meta_id.0), }); } } // Record solution self.substitution.insert(meta_id, solution.clone()); if let Some(info) = self.metas.get_mut(&meta_id) { info.solution = Some(solution.clone()); } Ok(true) } /// Check if a term is well-scoped in a context fn is_well_scoped(&self, term: &Term, context: &[String]) -> bool { match term { Term::Var(x) => { // Check if it's a bound variable or a global constant context.contains(x) || self.context.lookup(x).is_some() || self.context.lookup_axiom(x).is_some() || self.context.lookup_constructor(x).is_some() } Term::App(f, arg) => { self.is_well_scoped(f, context) && self.is_well_scoped(arg, context) } Term::Abs(x, ty, body) => { let mut extended_ctx = context.to_vec(); extended_ctx.push(x.clone()); self.is_well_scoped(ty, context) && self.is_well_scoped(body, &extended_ctx) } Term::Pi(x, ty, body, _) => { let mut extended_ctx = context.to_vec(); extended_ctx.push(x.clone()); self.is_well_scoped(ty, context) && self.is_well_scoped(body, &extended_ctx) } Term::Const(name) => { // Constants should be in the global context self.context.lookup_axiom(name).is_some() || self.context.lookup_constructor(name).is_some() } _ => true, // Sorts, meta-variables, etc. } } /// Alpha equality check fn alpha_equal(&self, t1: &Term, t2: &Term) -> bool { self.alpha_equal_aux(t1, t2, &mut vec![]) } fn alpha_equal_aux(&self, t1: &Term, t2: &Term, renamings: &mut Vec<(String, String)>) -> bool { match (t1, t2) { (Term::Var(x), Term::Var(y)) => { // Check if this is a bound variable that was renamed for (a, b) in renamings.iter() { if a == x && b == y { return true; } } x == y } (Term::App(f1, a1), Term::App(f2, a2)) => { self.alpha_equal_aux(f1, f2, renamings) && self.alpha_equal_aux(a1, a2, renamings) } (Term::Abs(x1, t1, b1), Term::Abs(x2, t2, b2)) => { if !self.alpha_equal_aux(t1, t2, renamings) { return false; } renamings.push((x1.clone(), x2.clone())); let result = self.alpha_equal_aux(b1, b2, renamings); renamings.pop(); result } (Term::Pi(x1, t1, b1, i1), Term::Pi(x2, t2, b2, i2)) if i1 == i2 => { if !self.alpha_equal_aux(t1, t2, renamings) { return false; } renamings.push((x1.clone(), x2.clone())); let result = self.alpha_equal_aux(b1, b2, renamings); renamings.pop(); result } (Term::Sort(u1), Term::Sort(u2)) => u1 == u2, (Term::Const(c1), Term::Const(c2)) => c1 == c2, (Term::Meta(m1), Term::Meta(m2)) => m1 == m2, _ => false, } } /// Rename a variable in a term fn rename_var(&self, old: &str, new: &str, term: &Term) -> Term { match term { Term::Var(x) if x == old => Term::Var(new.to_string()), Term::Var(x) => Term::Var(x.clone()), Term::App(f, arg) => Term::App( Box::new(self.rename_var(old, new, f)), Box::new(self.rename_var(old, new, arg)), ), Term::Abs(x, ty, body) if x != old => Term::Abs( x.clone(), Box::new(self.rename_var(old, new, ty)), Box::new(self.rename_var(old, new, body)), ), Term::Pi(x, ty, body, implicit) if x != old => Term::Pi( x.clone(), Box::new(self.rename_var(old, new, ty)), Box::new(self.rename_var(old, new, body)), *implicit, ), _ => term.clone(), } } /// Propagate solutions to dependent constraints fn propagate_solution(&mut self) -> Result<(), TypeError> { // Apply substitution to all remaining constraints let constraints: Vec<_> = self.constraints.drain().collect(); for (id, constraint) in constraints { let updated = self.apply_subst_to_constraint(constraint); self.constraints.insert(id, updated); } Ok(()) } /// Apply substitution to a constraint fn apply_subst_to_constraint(&self, constraint: Constraint) -> Constraint { match constraint { Constraint::Unify { id, left, right, strength, } => Constraint::Unify { id, left: self.substitution.apply(&left), right: self.substitution.apply(&right), strength, }, Constraint::HasType { id, term, expected_type, } => Constraint::HasType { id, term: self.substitution.apply(&term), expected_type: self.substitution.apply(&expected_type), }, Constraint::UnifyUniverse { id, left, right, strength, } => Constraint::UnifyUniverse { id, left: self.substitution.apply_universe(&left), right: self.substitution.apply_universe(&right), strength, }, Constraint::UniverseLevel { id, left, right } => Constraint::UniverseLevel { id, left: self.substitution.apply_universe(&left), right: self.substitution.apply_universe(&right), }, Constraint::Delayed { id, constraint, waiting_on, } => Constraint::Delayed { id, constraint: Box::new(self.apply_subst_to_constraint(*constraint)), waiting_on, }, } } /// Solve a HasType constraint by type inference and unification fn solve_has_type_constraint( &mut self, term: &Term, expected_type: &Term, ) -> Result<bool, TypeError> { match term { Term::Meta(meta_name) => { // If the term is a meta-variable, we can potentially solve it if let Some(meta_id) = self.parse_meta_name(meta_name) { if let Some(meta_info) = self.metas.get(&meta_id) { if meta_info.solution.is_none() { // Try to construct a term that has the expected type if let Some(solution) = self.synthesize_term_of_type(expected_type)? { return self.solve_meta(meta_id, &solution); } } } } // If we can't solve the meta, try unifying with expected type self.unify(term, expected_type, ConstraintStrength::Preferred) } Term::App(f, arg) => { // For applications, we need to ensure the function type is compatible // Create a fresh meta for the function type: ?F : ?A -> ?B let arg_type_meta_id = self.fresh_meta(vec![], None); let result_type_meta_id = self.fresh_meta(vec![], None); let arg_type_meta = Term::Meta(format!("?m{}", arg_type_meta_id.0)); let result_type_meta = Term::Meta(format!("?m{}", result_type_meta_id.0)); let func_type = Term::Pi( "_".to_string(), Box::new(arg_type_meta.clone()), Box::new(result_type_meta.clone()), false, ); // Add constraints: // 1. f : ?A -> ?B // 2. arg : ?A // 3. ?B ≡ expected_type let f_constraint = Constraint::HasType { id: self.new_constraint_id(), term: f.as_ref().clone(), expected_type: func_type, }; let arg_constraint = Constraint::HasType { id: self.new_constraint_id(), term: arg.as_ref().clone(), expected_type: arg_type_meta, }; let result_constraint = Constraint::Unify { id: self.new_constraint_id(), left: result_type_meta, right: expected_type.clone(), strength: ConstraintStrength::Required, }; self.add_constraint(f_constraint); self.add_constraint(arg_constraint); self.add_constraint(result_constraint); Ok(true) } Term::Abs(param, param_type, body) => { // For lambda abstractions, expected type should be a Pi type match expected_type { Term::Pi(_, expected_param_type, expected_body_type, _) => { // Unify parameter types and check body type let param_unify = Constraint::Unify { id: self.new_constraint_id(), left: param_type.as_ref().clone(), right: expected_param_type.as_ref().clone(), strength: ConstraintStrength::Required, }; let body_check = Constraint::HasType { id: self.new_constraint_id(), term: body.as_ref().clone(), expected_type: expected_body_type.as_ref().clone(), }; self.add_constraint(param_unify); self.add_constraint(body_check); Ok(true) } Term::Meta(_) => { // Expected type is a meta-variable, create a Pi type for it let body_type_meta_id = self.fresh_meta(vec![param.clone()], None); let body_type_meta = Term::Meta(format!("?m{}", body_type_meta_id.0)); let pi_type = Term::Pi( param.clone(), param_type.clone(), Box::new(body_type_meta.clone()), false, ); let type_unify = Constraint::Unify { id: self.new_constraint_id(), left: expected_type.clone(), right: pi_type, strength: ConstraintStrength::Required, }; let body_check = Constraint::HasType { id: self.new_constraint_id(), term: body.as_ref().clone(), expected_type: body_type_meta, }; self.add_constraint(type_unify); self.add_constraint(body_check); Ok(true) } _ => { // Type mismatch - lambda can't have non-function type Err(TypeError::TypeMismatch { expected: expected_type.clone(), actual: Term::Pi( param.clone(), param_type.clone(), Box::new(Term::Meta("?unknown".to_string())), false, ), }) } } } _ => { // For other terms, just unify with the expected type self.unify(term, expected_type, ConstraintStrength::Preferred) } } } /// Attempt to synthesize a term of a given type (basic heuristics) fn synthesize_term_of_type(&self, expected_type: &Term) -> Result<Option<Term>, TypeError> { match expected_type { Term::Sort(_) => { // For Sort types, we could return a fresh meta or a simple type Ok(Some(Term::Meta(format!("?synth{}", self.next_meta_id)))) } Term::Pi(param, param_type, _body_type, _implicit) => { // For Pi types, synthesize a lambda that matches the Pi structure // Use a fresh meta-variable for the body to avoid infinite recursion let body_term = Term::Meta(format!("?body{}", self.next_meta_id)); Ok(Some(Term::Abs( param.clone(), param_type.clone(), Box::new(body_term), ))) } Term::Meta(_) => { // Can't synthesize for unknown types Ok(None) } _ => { // For concrete types, return a meta-variable Ok(Some(Term::Meta(format!("?synth{}", self.next_meta_id)))) } } } /// Check if a term is a Miller pattern /// Miller patterns are terms of the form: ?M x1 x2 ... xn where xi are /// distinct bound variables fn is_miller_pattern(&self, term: &Term) -> bool { let (head, args) = self.decompose_application(term); match head { Term::Meta(_) => { // Check that all arguments are distinct variables let mut seen = HashSet::new(); for arg in args { if let Term::Var(x) = arg { if !seen.insert(x.clone()) { return false; // Not distinct } } else { return false; // Not a variable } } true } _ => false, } } /// Extract the spine of a Miller pattern (the meta-variable and its /// arguments) fn extract_miller_spine(&self, term: &Term) -> Option<(String, Vec<String>)> { // First validate it's actually a Miller pattern if !self.is_miller_pattern(term) { return None; } let (head, args) = self.decompose_application(term); if let Term::Meta(meta_name) = head { // Collect variable names (we already know they're all variables from // is_miller_pattern) let var_names: Vec<String> = args .iter() .map(|arg| { if let Term::Var(name) = arg { name.clone() } else { unreachable!() } }) .collect(); Some((meta_name.clone(), var_names)) } else { None } } /// Solve simple Miller pattern unification /// Only handles simple cases fn solve_miller_pattern( &mut self, meta_name: &str, spine: &[String], other: &Term, ) -> Result<bool, TypeError> { // Check if we can abstract over the spine variables if !Self::can_abstract_over_variables(other, spine) { // Can't abstract, fall back to regular unification return self.unify( &Term::Meta(meta_name.to_string()), other, ConstraintStrength::Required, ); } if let Some(meta_id) = self.parse_meta_name(meta_name) { // Only handle simple cases to avoid complexity match other { // Case 1: ?M x ≡ y (different variable) -> ?M := λx. y Term::Var(y) if spine.len() == 1 && spine[0] != *y => { let solution = Term::Abs( spine[0].clone(), Box::new(Term::Meta(format!("?T{}", self.next_meta_id))), /* Type inferred later */ Box::new(other.clone()), ); return self.solve_meta(meta_id, &solution); } // Case 2: ?M x ≡ c (constant) -> ?M := λx. c Term::Const(_) | Term::Sort(_) if spine.len() == 1 => { let solution = Term::Abs( spine[0].clone(), Box::new(Term::Meta(format!("?T{}", self.next_meta_id))), Box::new(other.clone()), ); return self.solve_meta(meta_id, &solution); } _ => { // For more complex cases, we could build the full lambda // abstraction but for now, fall back to // regular unification } } } // Fall back to regular unification self.unify( &Term::Meta(meta_name.to_string()), other, ConstraintStrength::Required, ) } /// Check if a term can be abstracted over the given variables fn can_abstract_over_variables(term: &Term, vars: &[String]) -> bool { // For now, implement a simple check // In a full implementation, this would check that the term only uses variables // that are either in the spine or are bound locally match term { Term::Var(v) => vars.contains(v), // Variable must be in spine Term::App(f, arg) => { Self::can_abstract_over_variables(f, vars) && Self::can_abstract_over_variables(arg, vars) } Term::Abs(param, ty, body) => { // Extend the scope with the bound parameter let mut extended_vars = vars.to_vec(); extended_vars.push(param.clone()); Self::can_abstract_over_variables(ty, vars) && Self::can_abstract_over_variables(body, &extended_vars) } Term::Meta(_) => true, // Meta-variables are always abstractable Term::Const(_) => true, // Constants are always abstractable Term::Sort(_) => true, // Sorts are always abstractable _ => false, // Conservative for complex constructs } } /// Delay a constraint for later processing fn delay_constraint( &mut self, constraint_id: ConstraintId, waiting_on: HashSet<MetaId>, ) -> Result<(), TypeError> { if let Some(constraint) = self.constraints.remove(&constraint_id) { let delayed = Constraint::Delayed { id: constraint_id, constraint: Box::new(constraint), waiting_on, }; self.constraints.insert(constraint_id, delayed); self.delayed_constraints.insert(constraint_id); } Ok(()) } /// Wake up delayed constraints that are no longer blocked fn wake_delayed_constraints(&mut self) -> Result<Vec<ConstraintId>, TypeError> { let mut woken = Vec::new(); let mut to_wake = Vec::new(); // Check which delayed constraints can now be woken up for constraint_id in &self.delayed_constraints { if let Some(Constraint::Delayed { waiting_on, constraint, .. }) = self.constraints.get(constraint_id) { // Check if all blocking metas are now solved let all_solved = waiting_on.iter().all(|meta_id| { self.metas .get(meta_id) .is_some_and(|info| info.solution.is_some()) }); if all_solved { to_wake.push((*constraint_id, constraint.as_ref().clone())); } } } // Wake up the constraints for (constraint_id, original_constraint) in to_wake { self.constraints.insert(constraint_id, original_constraint); self.delayed_constraints.remove(&constraint_id); woken.push(constraint_id); } Ok(woken) } /// Check if we can delay a constraint fn can_delay(&self, constraint_id: &ConstraintId) -> bool { if let Some(constraint) = self.constraints.get(constraint_id) { match constraint { Constraint::Unify { left, right, strength, .. } => { // We can delay weak constraints that involve unsolved metas if *strength == ConstraintStrength::Weak { let left_metas = self.collect_metas_in_term(left); let right_metas = self.collect_metas_in_term(right); // Check if any involved metas are unsolved for meta_id in left_metas.iter().chain(right_metas.iter()) { if self.is_unsolved_meta(meta_id) { return true; } } } false } Constraint::HasType { term, expected_type, .. } => { // Can delay HasType constraints involving unsolved metas let term_metas = self.collect_metas_in_term(term); let type_metas = self.collect_metas_in_term(expected_type); for meta_id in term_metas.iter().chain(type_metas.iter()) { if let Some(meta_info) = self.metas.get(meta_id) { if meta_info.solution.is_none() { return true; } } } false } Constraint::Delayed { .. } => true, // Already delayed _ => false, } } else { false } } /// Check if a meta-variable is unsolved fn is_unsolved_meta(&self, meta_id: &MetaId) -> bool { self.metas .get(meta_id) .is_some_and(|info| info.solution.is_none()) } } /// Information about a meta-variable #[derive(Debug, Clone)] pub struct MetaInfo { pub id: MetaId, pub context: Vec<String>, // Variables in scope when meta was created pub expected_type: Option<Term>, // Expected type of the meta-variable pub solution: Option<Term>, // Solution if solved pub dependencies: HashSet<MetaId>, // Meta-variables this depends on pub occurrences: Vec<ConstraintId>, // Constraints this meta appears in } }
Meta-variables represent unknown terms that get resolved through unification and constraint solving. Our implementation tracks meta-variable dependencies and applies solving algorithms to determine unique solutions when possible.
Takeaways
The Calculus of Constructions represents a unique convergence of computational and logical capabilities that distinguishes it from other type systems. The fundamental characteristic that sets CoC apart is its unification of terms, types, and kinds within a single syntactic framework, eliminating the artificial stratification found in traditional type systems. This unification enables unprecedented expressiveness where types can depend on computational values, creating a system where mathematical specifications and their implementations coexist naturally within the same linguistic framework.
The definitional equality mechanism provides computational content to the type system through β-reduction, η-conversion, and definition unfolding, creating a rich equational theory that recognizes when different syntactic expressions represent the same computational object. This equality extends beyond simple syntactic matching to include semantic equivalence, enabling the type checker to recognize mathematical identities and computational transformations automatically. The normalization algorithm ensures that definitional equality checking remains decidable while providing the computational power needed for type-level computations.