pub struct Unifier { /* private fields */ }Expand description
Holds the inference variables of a type problem and the substitution that unification builds over them.
A Unifier is the working state of type inference. It mints fresh
TyVars with fresh, makes two types equal with
unify — recording the variable bindings that equality
requires — and reads a type back under those bindings with
resolve. A variable belongs to the unifier that minted it.
Unification is the standard first-order algorithm: two constructors match only if their heads and arity agree, in which case their arguments are unified pairwise; a variable unifies with any type by being bound to it, guarded by an occurs check so a variable can never be bound to a type that contains it. The substitution it produces is a most-general unifier — it constrains a variable only as far as making the two types equal demands.
§Examples
use type_lang::{TyCon, Type, Unifier};
const FUNCTION: TyCon = TyCon::new(0);
const INT: TyCon = TyCon::new(1);
let mut unifier = Unifier::new();
let arg = unifier.fresh();
let ret = unifier.fresh();
// Unify the inferred signature (?arg) -> ?ret with (int) -> int.
let inferred = Type::app(FUNCTION, [Type::var(arg), Type::var(ret)]);
let known = Type::app(FUNCTION, [Type::con(INT), Type::con(INT)]);
unifier.unify(&inferred, &known).expect("same constructor and arity");
// Both variables are now known to be int.
assert_eq!(unifier.resolve(&Type::var(arg)), Type::con(INT));
assert_eq!(unifier.resolve(&Type::var(ret)), Type::con(INT));Implementations§
Source§impl Unifier
impl Unifier
Sourcepub const fn new() -> Self
pub const fn new() -> Self
Creates an empty unifier with no variables.
§Examples
use type_lang::Unifier;
let unifier = Unifier::new();
assert!(unifier.is_empty());Sourcepub fn with_capacity(vars: usize) -> Self
pub fn with_capacity(vars: usize) -> Self
Creates an empty unifier with room for vars variables preallocated.
A hint only: it sizes the internal table so that minting up to vars
variables does not reallocate. Use it when the variable count is known up
front — for instance, one per binding in the scope being checked.
§Examples
use type_lang::Unifier;
let mut unifier = Unifier::with_capacity(8);
for _ in 0..8 {
let _ = unifier.fresh();
}
assert_eq!(unifier.var_count(), 8);Sourcepub fn fresh(&mut self) -> TyVar
pub fn fresh(&mut self) -> TyVar
Mints a fresh, unbound inference variable.
Variables are numbered in creation order from 0 and stay valid for the
life of the unifier. A fresh variable stands for “some type not yet known”;
it gains a binding only when unify requires one.
Variable ids are 32-bit, so a unifier addresses up to u32::MAX variables —
far beyond any realistic inference problem, since the binding table alone
would need tens of gigabytes long before the id space ran out. The bound is
asserted in debug builds.
§Examples
use type_lang::Unifier;
let mut unifier = Unifier::new();
let a = unifier.fresh();
let b = unifier.fresh();
assert_ne!(a, b);
assert_eq!(unifier.var_count(), 2);Sourcepub fn unify(&mut self, a: &Type, b: &Type) -> Result<(), TypeError>
pub fn unify(&mut self, a: &Type, b: &Type) -> Result<(), TypeError>
Unifies two types, binding variables as needed to make them equal.
On success the unifier’s substitution is extended so that a and b
resolve to the same type. On failure the call returns a
TypeError describing why, and any bindings made before the conflict
was reached are kept — unification is not transactional. A caller that
needs to try a unification speculatively should clone the
unifier first and keep the clone only if it succeeds.
§Errors
TypeError::Mismatchif the two types are built from different constructors or the same constructor at a different arity.TypeError::Occursif making them equal would require binding a variable to a type that contains it (an infinite type).
§Examples
use type_lang::{TyCon, Type, TypeError, Unifier};
const INT: TyCon = TyCon::new(0);
const BOOL: TyCon = TyCon::new(1);
let mut unifier = Unifier::new();
let v = unifier.fresh();
// A variable unifies with a concrete type by being bound to it.
unifier.unify(&Type::var(v), &Type::con(INT)).unwrap();
assert_eq!(unifier.resolve(&Type::var(v)), Type::con(INT));
// Two different constructors do not unify.
let err = unifier.unify(&Type::con(INT), &Type::con(BOOL)).unwrap_err();
assert!(matches!(err, TypeError::Mismatch { .. }));Sourcepub fn resolve(&self, ty: &Type) -> Type
pub fn resolve(&self, ty: &Type) -> Type
Resolves a type fully under the current substitution.
Every bound variable in ty is replaced by what it was bound to, all the
way down, leaving a type whose only variables are still unbound. A type with
no bound variables resolves to an equal copy of itself.
The walk is proportional to the size of the resolved result, which — for a substitution that maps a variable to a type mentioning it twice — can be larger than the input. Resolve once you are done constraining a type, rather than after every step.
§Examples
use type_lang::{TyCon, Type, Unifier};
const LIST: TyCon = TyCon::new(0);
const INT: TyCon = TyCon::new(1);
let mut unifier = Unifier::new();
let element = unifier.fresh();
let collection = unifier.fresh();
// ?collection = List<?element>, then ?element = int.
unifier
.unify(&Type::var(collection), &Type::app(LIST, [Type::var(element)]))
.unwrap();
unifier.unify(&Type::var(element), &Type::con(INT)).unwrap();
// Resolving the outer variable substitutes all the way down.
assert_eq!(
unifier.resolve(&Type::var(collection)),
Type::app(LIST, [Type::con(INT)]),
);
// An unbound variable resolves to itself.
let free = unifier.fresh();
assert_eq!(unifier.resolve(&Type::var(free)), Type::var(free));