Every constraint used in CHR rules has to be declared with a
`chr_constraint/1`

declaration by the constraint
specifier. For convenience multiple constraints may be declared at once with
the same `chr_constraint/1`

declaration followed by a comma-separated
list of constraint specifiers.

A constraint specifier is, in its compact form, `F/A` where `F` and `A` are respectively
the functor name and arity of the constraint, e.g.

:- chr_constraint foo/1. :- chr_constraint bar/2, baz/3.

In its extended form, a constraint specifier is `c``(`

`A_1``,...,`

`A_n``)`

where `c` is the constraint's functor, `n` its arity and the `A_i` are argument
specifiers. An argument specifier is a mode, optionally followed by a type. E.g.

:- chr_constraint get_value(+,?). :- chr_constraint domain(?int,+list(int)), alldifferent(?list(int)).

A mode is one of the following:

`-`

- The corresponding argument of every occurrence of the constraint is always unbound.
`+`

- The corresponding argument of every occurrence of the constraint is always ground.
`?`

- The corresponding argument of every occurrence of the constraint can have any instantiation, which may change over time. This is the default value.

A type can be a user-defined type or one of the built-in types. A type comprises a (possibly infinite) set of values. The type declaration for a constraint argument means that for every instance of that constraint the corresponding argument is only ever bound to values in that set. It does not state that the argument necessarily has to be bound to a value.

The built-in types are:

`int`

- The corresponding argument of every occurrence of the constraint is an integer.
`float`

- ... a floating point number.
`number`

- ... a number.
`natural`

- ... a positive integer.
`any`

- The corresponding argument of every occurrence of the constraint can have any type. This is the default value.

User-defined types are algebraic data types, similar to those in Haskell or the discriminated unions in Mercury. An algebraic data type is defined using

:- chr_typetype--->body.

If the type term is a functor of arity zero (i.e. one having zero arguments), it names a monomorphic type. Otherwise, it names a polymorphic type; the arguments of the functor must be distinct type variables. The body term is defined as a sequence of constructor definitions separated by semi-colons.

Each constructor definition must be a functor whose arguments (if any) are types. Discriminated union definitions must be transparent: all type variables occurring in the body must also occur in the type.

Here are some examples of algebraic data type definitions:

:- chr_type color ---> red ; blue ; yellow ; green. :- chr_type tree ---> empty ; leaf(int) ; branch(tree, tree). :- chr_type list(T) ---> [] ; [T | list(T)]. :- chr_type pair(T1, T2) ---> (T1 - T2).

Each algebraic data type definition introduces a distinct type. Two algebraic data types that have the same bodies are considered to be distinct types (name equivalence).

Constructors may be overloaded among different types: there may be any number of constructors with a given name and arity, so long as they all have different types.

Aliases can be defined using ‘`==`’. For example, if your program uses
lists of lists of integers, you can define an alias as follows:

:- chr_type lli == list(list(int)).

Send feedback on this subject.