3.3 Predicate and function type declarations

The argument types of each predicate must be explicitly declared with a ‘:- pred’ declaration. The argument types and return type of each function must be explicitly declared with a ‘:- func’ declaration. For example:

:- pred is_all_uppercase(string).

:- func strlen(string) = int.

Predicates and functions can be polymorphic; that is, their declarations can include type variables. For example:

:- pred member(T, list(T)).

:- func length(list(T)) = int.

A predicate or function can be declared to have a given higher-order type (see Higher-order) by using an explicit type qualification in the type declaration. This is useful where several predicates or functions need to have the same type signature, which often occurs for type class method implementations (see Type classes), and for predicates to be passed as higher-order terms.

For example,

:- type foldl_pred(T, U) == pred(T, U, U).
:- type foldl_func(T, U) == (func(T, U) = U).

:- pred p(int) : foldl_pred(T, U).
:- func f(int) : foldl_func(T, U).

is equivalent to

:- pred p(int, T, U, U).
:- pred f(int, T, U) = U.

Type variables in predicate and function declarations are implicitly universally quantified by default; that is, the predicate or function may be called with arguments and (in the case of functions) return value whose actual types are any instance of the types specified in the declaration. For example, the function ‘length/1’ declared above could be called with the argument having type ‘list(int)’, or ‘list(float)’, or ‘list(list(int))’, etc.

Type variables in predicate and function declarations can also be existentially quantified; this is discussed in Existential types.

There must only be one predicate with a given name and arity in each module, and only one function with a given name and arity in each module. It is an error to declare the same predicate or function twice.

There must be at least one clause defined for each declared predicate or function, except for those defined using the foreign language interface (see Foreign language interface). However, Mercury implementations are permitted to provide a method of processing Mercury programs in which such errors are not reported until and unless the predicate or function is actually called. (The Melbourne Mercury implementation provides this with its ‘--allow-stubs’ option. This can be useful during program development, since it allows you to execute parts of a program while the program’s implementation is still incomplete.)

Note that a predicate defined using DCG notation (see DCG-rules) will appear to be defined with two fewer arguments than it is declared with. It will also appear to be called with two fewer arguments when called from predicates defined using DCG notation. However, when called from an ordinary predicate or function, it must have all the arguments it was declared with.

The compiler infers the types of data-terms, and in particular the types of variables and overloaded constructors, functions, and predicates. A type assignment is an assignment of a type to every variable, and of a particular constructor, function, or predicate to every name in a clause. A type assignment is valid if it satisfies the following conditions.

Each constructor in a clause must have been declared in at least one visible type declaration. The type assigned to each constructor term must match one of the type declarations for that constructor, and the types assigned to the arguments of that constructor must match the argument types specified in that type declaration.

The type assigned to each function call term must match the return type of one of the ‘:- func’ declarations for that function, and the types assigned to the arguments of that function must match the argument types specified in that type declaration.

The type assigned to each predicate argument must match the type specified in one of the ‘:- pred’ declarations for that predicate. The type assigned to each head argument in a predicate clause must exactly match the argument type specified in the corresponding ‘:- pred’ declaration.

The type assigned to each head argument in a function clause must exactly match the argument type specified in the corresponding ‘:- func’ declaration, and the type assigned to the result term in a function clause must exactly match the result type specified in the corresponding ‘:- func’ declaration.

The type assigned to each data-term with an explicit type qualification (see Explicit type qualification) must match the type specified by the type qualification expression².

(Here “match” means to be an instance of, i.e. to be identical to for some substitution of the type parameters, and “exactly match” means to be identical up to renaming of type parameters.)

One type assignment A is said to be more general than another type assignment B if there is a binding of the type parameters in A that makes it identical (up to renaming of parameters) to B. If there is more than one valid type assignment, the compiler must choose the most general one. If there are two valid type assignments which are not identical up to renaming and neither of which is more general than the other, then there is a type ambiguity, and compiler must report an error. A clause is type-correct if there is a unique (up to renaming) most general valid type assignment. Every clause in a Mercury program must be type-correct.