Next: Abstract solver type declarations, Up: Solver types [Contents]
Variables with solver types can have one of three possible insts:
free
, ground
or any
.
A variable with a solver type with inst any
may not (yet) be semantically ground, in the following sense:
if a variable is semantically ground,
then the set of values it unifies with form an equivalence class;
if a variable is non-ground,
then the set of values it unifies with do not form an equivalence class.
More formally, X
is ground
if for values Y
and Z
that unify with X
,
it is the case that Y
and Z
also unify with each other.
X
is non-ground
if there are values Y
and Z
that unify with X
,
but which do not unify with each other.
A non-solver type value will have inst any
if it is constructed using one or more inst any
values.
The builtin modes ia
and oa
are equivalent to in(any)
and out(any)
respectively.