Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Universe Polymorphism

Universe polymorphism enables definitions to abstract over universe levels, creating truly generic constructions that work across the entire universe hierarchy. Our implementation includes a dedicated universe constraint solver that handles the complex arithmetic and constraint relationships that arise in polymorphic universe contexts.

Universe Constraint Solver

#![allow(unused)]
fn main() {
use std::collections::{HashMap, HashSet};
/// Universe level constraint solver for polymorphic universe levels
use crate::ast::{Universe, UniverseConstraint};
impl UniverseSolver {
    pub fn new() -> Self {
        UniverseSolver {
            substitutions: HashMap::new(),
        }
    }

    /// Solve universe constraints and return substitutions
    pub fn solve(&mut self, constraints: &[UniverseConstraint]) -> Result<(), String> {
        // XXX: Simple constraint solver, in a full system this would be much more
        // sophisticated
        for constraint in constraints {
            self.solve_constraint(constraint)?;
        }
        Ok(())
    }

    /// Solve a single constraint
    fn solve_constraint(&mut self, constraint: &UniverseConstraint) -> Result<(), String> {
        match constraint {
            UniverseConstraint::Equal(u1, u2) => self.unify_universes(u1, u2),
            UniverseConstraint::LessEq(u1, u2) => {
                // XXX: For now, treat less-equal as equality
                self.unify_universes(u1, u2)
            }
        }
    }

    /// Unify two universe levels
    fn unify_universes(&mut self, u1: &Universe, u2: &Universe) -> Result<(), String> {
        let u1_subst = self.apply_substitution(u1);
        let u2_subst = self.apply_substitution(u2);

        match (&u1_subst, &u2_subst) {
            (Universe::ScopedVar(_, x), u) | (u, Universe::ScopedVar(_, x)) => {
                if let Universe::ScopedVar(_, y) = u {
                    if x == y {
                        return Ok(());
                    }
                }

                // Occurs check
                if self.occurs_check(x, u) {
                    return Err(format!(
                        "Universe variable {} occurs in {}",
                        x,
                        self.universe_to_string(u)
                    ));
                }

                self.substitutions.insert(x.clone(), u.clone());
                Ok(())
            }

            (Universe::Const(n1), Universe::Const(n2)) if n1 == n2 => Ok(()),
            (Universe::Const(_), Universe::Const(_)) => {
                Err("Cannot unify different constants".to_string())
            }

            (Universe::Add(u1, n1), Universe::Add(u2, n2)) if n1 == n2 => {
                self.unify_universes(u1, u2)
            }
            (Universe::Add(_, _), Universe::Add(_, _)) => {
                Err("Cannot unify different additions".to_string())
            }

            (Universe::Max(u1, v1), Universe::Max(u2, v2)) => {
                self.unify_universes(u1, u2)?;
                self.unify_universes(v1, v2)
            }

            (Universe::IMax(u1, v1), Universe::IMax(u2, v2)) => {
                self.unify_universes(u1, u2)?;
                self.unify_universes(v1, v2)
            }

            _ => Err(format!(
                "Cannot unify universe levels {} and {}",
                self.universe_to_string(&u1_subst),
                self.universe_to_string(&u2_subst)
            )),
        }
    }

    /// Apply substitutions to a universe level
    fn apply_substitution(&self, u: &Universe) -> Universe {
        match u {
            Universe::ScopedVar(_scope, x) => {
                if let Some(subst) = self.substitutions.get(x) {
                    self.apply_substitution(subst)
                } else {
                    u.clone()
                }
            }
            Universe::Const(n) => Universe::Const(*n),
            Universe::Add(u, n) => Universe::Add(Box::new(self.apply_substitution(u)), *n),
            Universe::Max(u, v) => Universe::Max(
                Box::new(self.apply_substitution(u)),
                Box::new(self.apply_substitution(v)),
            ),
            Universe::IMax(u, v) => Universe::IMax(
                Box::new(self.apply_substitution(u)),
                Box::new(self.apply_substitution(v)),
            ),
            _ => u.clone(),
        }
    }

    /// Check if a universe variable occurs in a universe level
    fn occurs_check(&self, var: &str, u: &Universe) -> bool {
        match u {
            Universe::ScopedVar(_, x) => x == var,
            Universe::Add(u, _) => self.occurs_check(var, u),
            Universe::Max(u, v) | Universe::IMax(u, v) => {
                self.occurs_check(var, u) || self.occurs_check(var, v)
            }
            Universe::Const(_) => false,
            Universe::Meta(_) => false, // Meta variables don't contain named variables
        }
    }

    /// Convert universe to string representation
    fn universe_to_string(&self, u: &Universe) -> String {
        match u {
            Universe::Const(n) => n.to_string(),
            Universe::ScopedVar(scope, var) => format!("{}::{}", scope, var),
            Universe::Meta(id) => format!("?u{}", id),
            Universe::Add(u, n) => format!("({} + {})", self.universe_to_string(u), n),
            Universe::Max(u, v) => format!(
                "max({}, {})",
                self.universe_to_string(u),
                self.universe_to_string(v)
            ),
            Universe::IMax(u, v) => format!(
                "imax({}, {})",
                self.universe_to_string(u),
                self.universe_to_string(v)
            ),
        }
    }

    /// Get the final substitution for a universe variable
    pub fn get_substitution(&self, var: &str) -> Option<Universe> {
        self.substitutions
            .get(var)
            .map(|u| self.apply_substitution(u))
    }

    /// Apply all substitutions to a universe level
    pub fn substitute_universe(&self, u: &Universe) -> Universe {
        self.apply_substitution(u)
    }

    /// Get all substitutions
    pub fn get_all_substitutions(&self) -> &HashMap<String, Universe> {
        &self.substitutions
    }

    /// Check if universe level constraints are satisfiable
    pub fn is_satisfiable(&self, constraints: &[UniverseConstraint]) -> bool {
        let mut solver = self.clone();
        solver.solve(constraints).is_ok()
    }

    /// Generate fresh universe variable
    pub fn fresh_universe_var(&self, base: &str, avoid: &HashSet<String>) -> String {
        let mut counter = 0;
        loop {
            let name = if counter == 0 {
                base.to_string()
            } else {
                format!("{}{}", base, counter)
            };
            if !avoid.contains(&name) && !self.substitutions.contains_key(&name) {
                return name;
            }
            counter += 1;
        }
    }
}
impl Default for UniverseSolver {
    fn default() -> Self {
        Self::new()
    }
}
/// Universe level constraint solver
#[derive(Debug, Clone)]
pub struct UniverseSolver {
    /// Substitutions for universe variables
    substitutions: HashMap<String, Universe>,
}
}

The UniverseSolver manages universe-level constraints independently from the main constraint solver, enabling specialized algorithms for universe arithmetic and level unification. This separation allows for efficient handling of universe polymorphism without complicating the main type checking algorithms.

Universe Constraint Types

Universe constraints capture the relationships between universe levels that must be maintained for logical consistency:

#![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),
}
}

The constraint system handles two fundamental relationships:

Equality Constraints (Equal) require two universe levels to be identical, arising from type equality requirements in dependent contexts where universe levels must match exactly.

Ordering Constraints (LessEq) ensure that one universe level is less than or equal to another, maintaining the predicativity requirements that prevent logical paradoxes.

Universe Constraint Solving

#![allow(unused)]
fn main() {
/// Solve universe constraints and return substitutions
pub fn solve(&mut self, constraints: &[UniverseConstraint]) -> Result<(), String> {
    // XXX: Simple constraint solver, in a full system this would be much more
    // sophisticated
    for constraint in constraints {
        self.solve_constraint(constraint)?;
    }
    Ok(())
}
}

The main solving algorithm processes constraint lists through iterative constraint resolution, ensuring that all universe relationships are satisfied consistently:

#![allow(unused)]
fn main() {
/// Solve a single constraint
fn solve_constraint(&mut self, constraint: &UniverseConstraint) -> Result<(), String> {
    match constraint {
        UniverseConstraint::Equal(u1, u2) => self.unify_universes(u1, u2),
        UniverseConstraint::LessEq(u1, u2) => {
            // XXX: For now, treat less-equal as equality
            self.unify_universes(u1, u2)
        }
    }
}
}

Individual constraint solving handles the different constraint types through specialized algorithms. Equality constraints use unification, while ordering constraints require more complex analysis to ensure the universe hierarchy remains consistent.

Universe Unification Algorithm

#![allow(unused)]
fn main() {
/// Unify two universe levels
fn unify_universes(&mut self, u1: &Universe, u2: &Universe) -> Result<(), String> {
    let u1_subst = self.apply_substitution(u1);
    let u2_subst = self.apply_substitution(u2);

    match (&u1_subst, &u2_subst) {
        (Universe::ScopedVar(_, x), u) | (u, Universe::ScopedVar(_, x)) => {
            if let Universe::ScopedVar(_, y) = u {
                if x == y {
                    return Ok(());
                }
            }

            // Occurs check
            if self.occurs_check(x, u) {
                return Err(format!(
                    "Universe variable {} occurs in {}",
                    x,
                    self.universe_to_string(u)
                ));
            }

            self.substitutions.insert(x.clone(), u.clone());
            Ok(())
        }

        (Universe::Const(n1), Universe::Const(n2)) if n1 == n2 => Ok(()),
        (Universe::Const(_), Universe::Const(_)) => {
            Err("Cannot unify different constants".to_string())
        }

        (Universe::Add(u1, n1), Universe::Add(u2, n2)) if n1 == n2 => {
            self.unify_universes(u1, u2)
        }
        (Universe::Add(_, _), Universe::Add(_, _)) => {
            Err("Cannot unify different additions".to_string())
        }

        (Universe::Max(u1, v1), Universe::Max(u2, v2)) => {
            self.unify_universes(u1, u2)?;
            self.unify_universes(v1, v2)
        }

        (Universe::IMax(u1, v1), Universe::IMax(u2, v2)) => {
            self.unify_universes(u1, u2)?;
            self.unify_universes(v1, v2)
        }

        _ => Err(format!(
            "Cannot unify universe levels {} and {}",
            self.universe_to_string(&u1_subst),
            self.universe_to_string(&u2_subst)
        )),
    }
}
}

Universe unification demonstrates the complexity of working with universe-level arithmetic. The algorithm handles multiple universe expression forms:

  1. Variable Unification: When unifying a universe variable with any expression, we create a substitution mapping after performing occurs checking to prevent infinite universe expressions.

  2. Constant Unification: Universe constants can only unify with identical constants, ensuring that concrete levels like Type 0 and Type 1 remain distinct.

  3. Arithmetic Expressions: Universe expressions like u + 1 and max(u, v) require structural decomposition where we recursively unify the component universe expressions.

Substitution and Normalization

#![allow(unused)]
fn main() {
/// Apply substitutions to a universe level
fn apply_substitution(&self, u: &Universe) -> Universe {
    match u {
        Universe::ScopedVar(_scope, x) => {
            if let Some(subst) = self.substitutions.get(x) {
                self.apply_substitution(subst)
            } else {
                u.clone()
            }
        }
        Universe::Const(n) => Universe::Const(*n),
        Universe::Add(u, n) => Universe::Add(Box::new(self.apply_substitution(u)), *n),
        Universe::Max(u, v) => Universe::Max(
            Box::new(self.apply_substitution(u)),
            Box::new(self.apply_substitution(v)),
        ),
        Universe::IMax(u, v) => Universe::IMax(
            Box::new(self.apply_substitution(u)),
            Box::new(self.apply_substitution(v)),
        ),
        _ => u.clone(),
    }
}
}

Universe substitution application demonstrates the recursive nature of universe expressions. When substituting into compound expressions like Add or Max, we must recursively apply substitutions to all subcomponents while maintaining the arithmetic structure.

Occurs Check for Universe Variables

#![allow(unused)]
fn main() {
/// Check if a universe variable occurs in a universe level
fn occurs_check(&self, var: &str, u: &Universe) -> bool {
    match u {
        Universe::ScopedVar(_, x) => x == var,
        Universe::Add(u, _) => self.occurs_check(var, u),
        Universe::Max(u, v) | Universe::IMax(u, v) => {
            self.occurs_check(var, u) || self.occurs_check(var, v)
        }
        Universe::Const(_) => false,
        Universe::Meta(_) => false, // Meta variables don't contain named variables
    }
}
}

The occurs check prevents infinite universe expressions by ensuring that universe variables don’t appear within their own solutions. This check must traverse the entire structure of universe expressions, including arithmetic operations and maximum expressions.

Universe Expression Normalization

The universe solver includes normalization capabilities that simplify universe expressions to canonical forms:

#![allow(unused)]
fn main() {
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(),
}
}

This normalization process:

  • Arithmetic Simplification: Combines constants in addition expressions like Const(2) + 3 becoming Const(5)
  • Maximum Computation: Evaluates maximum expressions between constants
  • Canonical Forms: Maintains normalized expressions that improve unification success

Universe Polymorphic Definitions

Universe polymorphism enables definitions like:

def id.{u} (A : Sort u) (x : A) : A := x

The .{u} syntax introduces a universe parameter that can be instantiated at different levels:

-- id instantiated at Type 0
id_nat : Nat → Nat := id.{0} Nat

-- id instantiated at Type 1
id_type : Type → Type := id.{1} Type

Fresh Variable Generation

#![allow(unused)]
fn main() {
/// Generate fresh universe variable
pub fn fresh_universe_var(&self, base: &str, avoid: &HashSet<String>) -> String {
    let mut counter = 0;
    loop {
        let name = if counter == 0 {
            base.to_string()
        } else {
            format!("{}{}", base, counter)
        };
        if !avoid.contains(&name) && !self.substitutions.contains_key(&name) {
            return name;
        }
        counter += 1;
    }
}
}

Fresh universe variable generation ensures that each universe abstraction gets unique variable names, preventing conflicts in complex polymorphic definitions. The algorithm:

  1. Base Name Generation: Starts with a descriptive base name
  2. Conflict Avoidance: Checks against existing variables and substitutions
  3. Counter Extension: Adds numeric suffixes when conflicts occur
  4. Uniqueness Guarantee: Ensures the returned name is globally unique

Substitution Management

#![allow(unused)]
fn main() {
/// Get the final substitution for a universe variable
pub fn get_substitution(&self, var: &str) -> Option<Universe> {
    self.substitutions
        .get(var)
        .map(|u| self.apply_substitution(u))
}
}

The solver provides access to resolved universe substitutions, enabling the main type checker to apply universe-level solutions throughout the type checking process.

#![allow(unused)]
fn main() {
/// Apply all substitutions to a universe level
pub fn substitute_universe(&self, u: &Universe) -> Universe {
    self.apply_substitution(u)
}
}

Universe substitution application handles the complete resolution of universe expressions, recursively applying all accumulated substitutions to produce fully resolved universe levels.

Integration with Type Checking

The universe solver integrates with the main type checking algorithm at several points:

Type Formation: When checking that types are well-formed, the universe solver ensures that universe level constraints are satisfied.

Polymorphic Instantiation: When instantiating polymorphic definitions, the universe solver generates fresh universe variables and maintains constraints between them.

Definitional Equality: When checking definitional equality between types with universe polymorphism, the universe solver ensures that universe relationships are preserved.

Constraint Satisfaction Checking

#![allow(unused)]
fn main() {
/// Check if universe level constraints are satisfiable
pub fn is_satisfiable(&self, constraints: &[UniverseConstraint]) -> bool {
    let mut solver = self.clone();
    solver.solve(constraints).is_ok()
}
}

The satisfiability checker enables the type checker to verify that universe constraint sets have solutions before committing to particular type assignments. This early checking prevents backtracking in complex type inference scenarios.

Universe Polymorphism Examples

Our implementation supports several forms of universe polymorphic definitions:

Polymorphic Data Types

structure Pair.{u, v} (A : Sort u) (B : Sort v) : Sort (max u v) :=
  (fst : A)
  (snd : B)

The Pair type is polymorphic over two universe levels, with the result type living at the maximum of the argument universe levels.

Polymorphic Functions

def const.{u, v} (A : Sort u) (B : Sort v) (x : A) (y : B) : A := x

The const function ignores its second argument and returns the first, working at any universe levels for both argument types.

Universe Level Arithmetic

def lift.{u} (A : Sort u) : Sort (u + 1) := A

The lift operation moves a type from universe u to universe u + 1, demonstrating universe level arithmetic in type expressions.

Failure modes

There are a couple of failure cases we handle with custom errors:

#![allow(unused)]
fn main() {
/// Convert universe to string representation
fn universe_to_string(&self, u: &Universe) -> String {
    match u {
        Universe::Const(n) => n.to_string(),
        Universe::ScopedVar(scope, var) => format!("{}::{}", scope, var),
        Universe::Meta(id) => format!("?u{}", id),
        Universe::Add(u, n) => format!("({} + {})", self.universe_to_string(u), n),
        Universe::Max(u, v) => format!(
            "max({}, {})",
            self.universe_to_string(u),
            self.universe_to_string(v)
        ),
        Universe::IMax(u, v) => format!(
            "imax({}, {})",
            self.universe_to_string(u),
            self.universe_to_string(v)
        ),
    }
}
}

The failures are categorized into three main types:

  • Unification Failures: Show the specific universe levels that couldn’t be unified
  • Occurs Check Violations: Identify infinite universe expressions
  • Arithmetic Inconsistencies: Point out invalid universe level arithmetic