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.
§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));