Next: Trace goals, Previous: Impurity, Up: Top [Contents]

• The any inst: | ||

• Abstract solver type declarations: | ||

• Solver type definitions: | ||

• Implementing solver types: | ||

• Solver types and negated contexts: |

Solver types are an experimental addition to the language supporting the
implementation of constraint solvers. A program may place constraints
on and between variables of a solver type, limiting the values those
variables may take on before they are actually bound. For example, if
`X`

and `Y`

are variables belonging to a constrained integer
solver type, we might place constraints upon them such that ```
X > 3
+ Y
```

and `Y =< 7`

. A later attempt to unify `Y`

with
`10`

will fail (it would violate the second constraint); similarly
an attempt to unify `X`

with `5`

and `Y`

with `4`

would fail (it would violate the first constraint).