11.2 Existential class constraints

Existentially quantified type variables are especially useful in combination with type class constraints.

Type class constraints can be either universal or existential. Universal type class constraints are written using ‘<=’, as described in Type class constraints on predicates and functions; they signify a constraint that the caller must satisfy. Existential type class constraints are written in the same syntax as universal constraints, but using ‘=>’ instead of ‘<=’; they signify a constraint that the callee must satisfy. If a declaration has both universal and existential constraints, then the existential constraints must precede the universal constraints.

For example:

% Here `c1(T2)' and `c2(T2)' are existential constraints,
% and `c3(T1)' is a universal constraint,
:- all [T1] some [T2] ((pred p(T1, T2) => (c1(T2), c2(T2))) <= c3(T1)).

Existential constraints must only constrain type variables that are explicitly existentially quantified. Likewise, universal constraints must only constrain type variables that are universally quantified, although in this case the quantification does not have to be explicit because universal quantification is the default (see Syntax for explicit type quantifiers).