The language contains builtin ‘inst’ values
(pred) is Determinism pred(Mode) is Determinism pred(Mode1, Mode2) is Determinism … (func) = Mode is Determinism func(Mode1) = Mode is Determinism func(Mode1, Mode2) = Mode is Determinism …
These insts represent the instantiation state
of variables bound to higher-order predicate and function terms
with the appropriate mode and determinism.
For example, ‘pred(out) is det’ represents the instantiation state
of being bound to a higher-order predicate term which is det
and accepts one output argument;
the term ‘sum([1,2,3])’ from the example above
is one such higher-order predicate term which matches this instantiation state.
As a convenience, the language also contains builtin ‘mode’ values of the same name (and they are what we have been using in the examples up to now). These modes map from the corresponding ‘inst’ to itself. It is as if they were defined by
:- mode (pred is Determinism) == in(pred is Determinism).
:- mode (pred(Inst) is Determinism) ==
in(pred(Inst) is Determinism).
…
using the parametric inst ‘in/1’ mentioned in Modes which maps an inst to itself.
If you want to define a predicate which returns a higher-order predicate term, you would use a mode such as ‘free >> pred(…) is …’, or ‘out(pred(…) is … )’. For example:
:- pred foo(pred(int)). :- mode foo(free >> (pred(out) is det)) is det. foo(sum([1,2,3])).
In the above mode declaration, the current Mercury implementation requires parentheses around the higher-order inst. (This is because the operator ‘>>’ binds more tightly then the operator ‘is’.)
Note that in Mercury it is an error to attempt to unify two higher-order terms. This is because equivalence of higher-order terms is undecidable in the general case.
For example, given the definition of ‘foo’ above, the goal
foo((pred(X::out) is det :- X = 6))
is illegal. If you really want to compare higher-order predicates for equivalence, you must program it yourself; for example, the above goal could legally be written as
P = (pred(X::out) is det :- X = 6), foo(Q), all [X] (call(P, X) <=> call(Q, X)).
Note that the compiler will only catch direct attempts at higher-order unifications; indirect attempts (via polymorphic predicates, for example ‘(list.append([], [P], [Q])’ may result in an error at run-time rather than at compile-time.
Mercury also provides builtin ‘inst’ values for use with solver types:
any_pred is Determinism any_pred(Mode) is Determinism any_pred(Mode1, Mode2) is Determinism … any_func = Mode is Determinism any_func(Mode1) = Mode is Determinism any_func(Mode1, Mode2) = Mode is Determinism …
See Solver types for more details.