# `Ichor.Backtrack.Bindings`
[🔗](https://github.com/joetjen/ichor_runtime/blob/v0.2.0/lib/ichor/backtrack/bindings.ex#L1)

A substitution: which logic variables are bound to which terms so
far, opaque outside this module. `unify/4` is the whole unification
algorithm -- standard, recursive, structural unification with no
occurs-check (matches ISO Prolog's own default: `X = f(X)` succeeds,
building a cyclic term, rather than failing or looping to detect the
cycle -- occurs-check is opt-in in real Prolog too, via `unify_with_occurs_check/2`,
never the default).

Every function takes a `term_module` argument (an
`Ichor.Backtrack.Term` implementation) explicitly, so this module
never needs to know what a caller's own term representation looks
like.

# `t`

```elixir
@opaque t()
```

# `bind`

```elixir
@spec bind(t(), term(), term()) :: t()
```

Extends `bindings`, binding `var_id` to `value`.

# `new`

```elixir
@spec new() :: t()
```

An empty substitution.

# `resolve`

```elixir
@spec resolve(module(), t(), term()) :: term()
```

Follows variable bindings until reaching either an unbound variable
or a non-variable term -- shallow dereferencing only (never recurses
into a compound term's own arguments), matching Prolog's own `deref`.

# `unify`

```elixir
@spec unify(module(), t(), term(), term()) :: {:ok, t()} | :fail
```

Unifies `a` and `b` under `bindings`, extending them on success.
Two distinct (by `var_id/1`) unbound variables unify by binding one
to the other; an unbound variable and anything else unify by binding
the variable; two compound terms unify when their functor and arity
match and every argument pairwise unifies; anything else unifies with
plain `==/2`.

# `unify_occurs_check`

```elixir
@spec unify_occurs_check(module(), t(), term(), term()) :: {:ok, t()} | :fail
```

Like `unify/4`, but with an occurs-check: a variable is never allowed
to bind to a compound term containing itself, which would otherwise
silently build an infinite term (`X = f(X)`). `unify/4`'s own absence
of this matches ISO Prolog's own default, not what a type checker
needs -- `Ichor.Toolkit.TypeScheme` is built on this variant
specifically because unifying two types this way must fail (not loop
forever, not silently accept an infinite type) when one contains a
variable already bound to (or literally equal to) the other.

---

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