17.4 Implementing solver types

A solver type is an abstraction, implemented using a combination of a private representation type and a constraint store.

The constraint store is an (impure) piece of state used to keep track of the extant constraints on variables of the solver type. This will typically be implemented using foreign code.

It is important that changes to the constraint store are properly trailed (see Trailing) so that changes can be undone on backtracking.

The solver type implementation should provide functions and predicates

• to construct and deconstruct solver type values,
• to place constraints on solver type variables,
• to convert any solver type variables to ground if possible (this is obviously an impure operation — see Impurity),
• to convert solver type values to non-solver type values (again, this is impure and requires the argument solver type values be sufficiently ground),
• to ask questions about the extant constraints on solver type variables without constraining them further (this too is impure because the set of constraints on a variable may change during execution of the program).