In Mercury, the mode and determinism of a higher-order predicate or function term are part of that term’s inst, not its type. This allows a single higher-order predicate to work on argument predicates of different modes and determinism, which is particularly useful for library predicates such as ‘list.map’ and ‘list.foldl’.
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])).
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.
In order to call a higher-order term, the compiler must know its higher-order inst. This can cause problems when higher-order terms are placed into a polymorphic collection type and then extracted, since the declared mode for the extraction will typically be ‘out’ and the higher-order inst information will be lost. To partially alleviate this problem, and to make higher-order functional programming easier, if the term to be called has a function type, but no higher-order inst information, we assume that it has the default higher-order function inst ‘func(in, …, in) = out is Determinism’.
As a consequence of this, it is a mode error to pass a higher-order function term that does not match this standard mode to somewhere where its higher-order inst information may be lost, such as to a polymorphic predicate where the argument mode is ‘in’.
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.