Hindley-Milner-style let-polymorphism: generalize/4 and
instantiate/3, built on Ichor.Backtrack.Bindings.unify_occurs_check/4
(plain unify/4 deliberately has no occurs-check, matching ISO
Prolog's own default -- a type checker needs one, or unifying a type
variable with a type containing itself would silently build an
infinite type instead of failing).
A "scheme" is {quantified :: MapSet.t(var_id), type} -- ∀ quantified. type
in the usual notation. generalize/4 computes one from a type and the
set of type variables still free in the surrounding environment
(never generalized away, since they belong to a binding whose own
type isn't finished yet -- typically every currently-in-scope lambda
parameter's own type variable); instantiate/3 produces a fresh copy
of a scheme's type, replacing every quantified variable with a newly
minted one -- what makes let id = fn x -> x in (id 1, id "s")
type-check, with two different instantiations of the same
polymorphic id.
Both need to rebuild a term (substituting quantified variables), so
term_module must implement Ichor.Backtrack.Term's optional
reconstruct/2 callback -- the one piece of this module that needs
construction, not just inspection, of a term.
Summary
Functions
Every type variable free in term, after resolving through bindings.
Generalizes type into a scheme: deep-resolves type through
bindings (so the scheme is self-contained -- reusable later, even
after bindings itself has moved on), then quantifies every free
variable not also present in env_free_vars.
Produces a fresh copy of scheme's type, replacing every quantified
variable with a newly minted one (fresh_var_fn.()), consistently
for repeated occurrences of the same variable -- a monomorphic scheme
(quantified empty, e.g. a lambda parameter's own binding) is
returned unchanged.
Fully resolves term through bindings, recursively -- unlike
Ichor.Backtrack.Bindings.resolve/3 (shallow, stops at the first
non-variable), this also resolves every bound variable nested inside
a compound term. Useful on its own for displaying/comparing a type
once inference is done, not just as generalize/4's own first step.
Types
Functions
@spec free_vars(module(), Ichor.Backtrack.Bindings.t(), term()) :: MapSet.t(term())
Every type variable free in term, after resolving through bindings.
Generalizes type into a scheme: deep-resolves type through
bindings (so the scheme is self-contained -- reusable later, even
after bindings itself has moved on), then quantifies every free
variable not also present in env_free_vars.
Produces a fresh copy of scheme's type, replacing every quantified
variable with a newly minted one (fresh_var_fn.()), consistently
for repeated occurrences of the same variable -- a monomorphic scheme
(quantified empty, e.g. a lambda parameter's own binding) is
returned unchanged.
@spec resolve_deep(module(), Ichor.Backtrack.Bindings.t(), term()) :: term()
Fully resolves term through bindings, recursively -- unlike
Ichor.Backtrack.Bindings.resolve/3 (shallow, stops at the first
non-variable), this also resolves every bound variable nested inside
a compound term. Useful on its own for displaying/comparing a type
once inference is done, not just as generalize/4's own first step.