#### 8.3.1 Builtin higher-order insts and modes

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.

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.