Type variables in type declarations for polymorphic predicates or functions are normally universally quantified. However, it is also possible to existentially quantify such type variables, by using an explicit existential quantifier of the form ‘some Vars’ before the ‘pred’ or ‘func’ declaration, where Vars is a list of variables.
For example:
% Here the type variables `T' is existentially quantified :- some [T] pred foo(T). % Here the type variables `T1' and `T2' are existentially quantified. :- some [T1, T2] func bar(int, list(T1), set(T2)) = pair(T1, T2). % Here the type variable `T2' is existentially quantified, % but the type variables `T1' and `T3' are universally quantified. :- some [T2] pred foo(T1, T2, T3).
Explicit universal quantifiers, of the form ‘all Vars’, are also permitted on ‘pred’ and ‘func’ declarations, although they are not necessary, since universal quantification is the default. (If both universal and existential quantifiers are present, the universal quantifiers must precede the existential quantifiers.) For example:
% Here the type variable `T2' is existentially quantified, % but the type variables `T1' and `T3' are universally quantified. :- all [T3] some [T2] pred foo(T1, T2, T3).