Robinson first-order unification for the rank-1 HM type system.
Used by the parser in W-style: each application/connective node calls unify/3 immediately during the AST traversal, updating the running substitution.
Summary
Types
A type-shaped value accepted by unify/3 and apply_subst/2: a full
Type.t() struct, a bare reference (type variable), or an atom (concrete
base type).
A substitution map mapping type variable references to resolved types.
Functions
Applies a type substitution to a given type or reference.
Unifies two types under the given substitution. Returns either an updated
substitution that reconciles t1 with t2, or an error.
Unifies two types, raising a TypeError on failure.
Types
@type general_type() :: ShotDs.Data.Type.t() | reference() | atom()
A type-shaped value accepted by unify/3 and apply_subst/2: a full
Type.t() struct, a bare reference (type variable), or an atom (concrete
base type).
@type type_substitution() :: %{ required(reference()) => ShotDs.Data.Type.t() | atom() | reference() }
A substitution map mapping type variable references to resolved types.
Functions
@spec apply_subst(general_type(), type_substitution()) :: general_type()
Applies a type substitution to a given type or reference.
@spec unify(general_type(), general_type(), type_substitution()) :: {:ok, type_substitution()} | {:error, String.t()}
Unifies two types under the given substitution. Returns either an updated
substitution that reconciles t1 with t2, or an error.
Both arguments are first resolved through the current substitution, so callers do not need to pre-apply themselves. Standard Robinson first-order unification with occurs check.
@spec unify!(general_type(), general_type(), type_substitution()) :: type_substitution()
Unifies two types, raising a TypeError on failure.