# `Ichor.Toolkit.TypeScheme`
[🔗](https://github.com/joetjen/ichor/blob/v0.3.0/lib/ichor/toolkit/type_scheme.ex#L1)

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.

# `scheme`

```elixir
@type scheme() :: {MapSet.t(term()), term()}
```

# `free_vars`

```elixir
@spec free_vars(module(), Ichor.Backtrack.Bindings.t(), term()) :: MapSet.t(term())
```

Every type variable free in `term`, after resolving through `bindings`.

# `generalize`

```elixir
@spec generalize(module(), Ichor.Backtrack.Bindings.t(), MapSet.t(term()), term()) ::
  scheme()
```

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`.

# `instantiate`

```elixir
@spec instantiate(module(), scheme(), (-> term())) :: term()
```

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.

# `resolve_deep`

```elixir
@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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*