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
For example, ‘pred(out) is det’ represents the instantiation state
of being bound to a higher-order predicate term which is
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])).
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.