Next: Existential types, Previous: Modules, Up: Top [Contents]
Mercury supports constrained polymorphism in the form of type classes. Type classes allow the programmer to write predicates and functions which operate on variables of any type (or sequence of types) for which a certain set of operations is defined.
A type class is a name for a set of types (or a set of sequences of types) for which certain predicates and/or functions, called the methods of that type class, are defined. A ‘typeclass’ declaration defines a new type class, and specifies the set of predicates and/or functions that must be defined on a type (or sequence of types) for it (them) to be considered to be an instance of that type class.
The typeclass declaration
gives the name of the type class that it is defining,
the names of the type variables which are parameters to the type class,
and the operations (i.e. methods) which form the interface of the type class.
For each method, all parameters of the typeclass must be determined
by the type declaration of the method.
The values of most parameter type variables
are determined by having them occur
in the declared type of an argument of the method.
However, if either the typeclass named in the constraint, or its superclasses,
include any functional dependencies, then
the value of a variable may also be implied by the values of other variables
(see Functional dependencies).
For example,
:- typeclass point(T) where [
% coords(Point, X, Y):
% X and Y are the cartesian coordinates of Point
pred coords(T, float, float),
mode coords(in, out, out) is det,
% translate(Point, X_Offset, Y_Offset) = NewPoint:
% NewPoint is Point translated X_Offset units in the X direction
% and Y_Offset units in the Y direction
func translate(T, float, float) = T
].
declares the type class point,
which represents points in two dimensional space.
pred, func and mode declarations
are the only legal declarations inside a typeclass declaration.
The mode and determinism of type class methods
must be explicitly declared or (for functions) defaulted, not inferred.
In other words, for each predicate declared in a type class,
there must be at least one mode declaration,
and each mode declaration in a type class
must include an explicit determinism annotation.
Functions with no explicit mode declaration
get the usual default mode (see Modes):
all arguments have mode in, the result has mode out,
and the determinism is det.
The number of parameters to the type class (e.g. T) is not limited.
For example, the following is allowed:
:- typeclass a(T1, T2) where […].
The parameters must be distinct variables.
Each typeclass declaration must have at least one parameter.
It is legal for a typeclass declaration to declare no methods,
for example
:- typeclass foo(T) where [].
There must not be more than one type class declaration with the same name and arity in the same module.
Once the interface of the type class
has been defined in the typeclass declaration,
we can use an instance declaration
to define how a particular type (or sequence of types)
satisfies the interface declared in the typeclass declaration.
An instance declaration has the form
:- instance classname(typename(typevar, …), …)
where [method_definition, method_definition, …].
An ‘instance’ declaration
gives a type for each parameter of the type class.
Each of these types must be either a type with no arguments,
or a polymorphic type whose arguments are all type variables.
For example int, list(T),
bintree(K, V) and bintree(T, T) are allowed,
but T and list(int) are not.
The types in an instance declaration must not be abstract types
which are elsewhere defined as equivalence types.
A program may not contain
more than one instance declaration for a particular type
(or sequence of types, in the case of a multi-parameter type class)
and typeclass.
These restrictions ensure that there are no overlapping instance declarations,
i.e. for each typeclass there is at most one instance declaration
that may be applied to any type (or sequence of types).
There is no special interaction between subtypes and the typeclass system. A subtype is not automatically an instance of a typeclass if there is an ‘instance’ declaration for its supertype.
Each method_definition entry
in the ‘where […]’ part of an instance declaration
defines the implementation of one of the class methods for this instance.
There are two ways of defining methods.
The first way to define a method is by giving the name of the predicate or function which implements that method. In this case, the method_definition must have one of the following forms:
pred(method_name/arity) is predname func(method_name/arity) is funcname
The predname or funcname must name a predicate or function of the specified arity whose type, modes, determinism, and purity are at least as permissive as the declared type, modes, determinism, and purity of the class method with the specified method_name and arity, after the types of the arguments in the instance declaration have been substituted in place of the parameters in the type class declaration.
The second way of defining methods is by listing the clauses for the definition inside the instance declaration. A method_definition can be a clause. These clauses are just like the clauses used to define ordinary predicates or functions (see Items), and so they can be facts, rules, or DCG rules. The only difference is that in instance declarations, clauses are separated by commas rather than being terminated by periods, and so rules and DCG rules in instance declarations must normally be enclosed in parentheses. As with ordinary predicates, you can have more than one clause for each method. The clauses must satisfy the declared type, modes, determinism and purity for the method, after the types of the arguments in the instance declaration have been substituted in place of the parameters in the type class declaration.
These two ways are mutually exclusive: each method must be defined either by a single naming definition (using the ‘pred(…) is predname’ or ‘func(…) is funcname’ form), or by a set of one or more clauses, but not both.
Here is an example of an instance declaration and the different kinds of method definitions that it can contain:
:- typeclass foo(T) where [
func method1(T, T) = int,
func method2(T) = int,
pred method3(T::in, int::out) is det,
pred method4(T::in, io.state::di, io.state::uo) is det,
func method5(bool, T) = T
].
:- instance foo(int) where [
% method defined by naming the implementation
func(method1/2) is (+),
% method defined by a fact
method2(X) = X + 1,
% method defined by a rule
(method3(X, Y) :- Y = X + 2),
% method defined by a DCG rule
(method4(X) --> io.print(X), io.nl),
% method defined by multiple clauses
method5(no, _) = 0,
(method5(yes, X) = Y :- X + Y = 0)
].
Each ‘instance’ declaration must define an implementation for every method declared in the corresponding ‘typeclass’ declaration. It is an error to define more than one implementation for the same method within a single ‘instance’ declaration.
Any call to a method must have argument types (and in the case of functions, return type) which are constrained to be a member of that method’s type class, or which match one of the instance declarations visible at the point of the call. A method call will invoke the predicate or function specified for that method in the instance declaration that matches the types of the arguments to the call.
Note that even if a type class has no methods, an explicit instance declaration is required for a type to be considered an instance of that type class.
Here is an example of some code using an instance declaration:
:- type coordinate
---> coordinate(
float, % X coordinate
float % Y coordinate
).
:- instance point(coordinate) where [
pred(coords/3) is coordinate_coords,
func(translate/3) is coordinate_translate
].
:- pred coordinate_coords(coordinate, float, float).
:- mode coordinate_coords(in, out, out) is det.
coordinate_coords(coordinate(X, Y), X, Y).
:- func coordinate_translate(coordinate, float, float) = coordinate.
coordinate_translate(coordinate(X, Y), Dx, Dy) = coordinate(X + Dx, Y + Dy).
We have now made the coordinate type
an instance of the point type class.
If we introduce a new type coloured_coordinate
which represents a point in two dimensional space
with a colour associated with it,
it can also become an instance of the type class:
:- type rgb
---> rgb(
int,
int,
int
).
:- type coloured_coordinate
---> coloured_coordinate(
float,
float,
rgb
).
:- instance point(coloured_coordinate) where [
pred(coords/3) is coloured_coordinate_coords,
func(translate/3) is coloured_coordinate_translate
].
:- pred coloured_coordinate_coords(coloured_coordinate, float, float).
:- mode coloured_coordinate_coords(in, out, out) is det.
coloured_coordinate_coords(coloured_coordinate(X, Y, _), X, Y).
:- func coloured_coordinate_translate(coloured_coordinate, float, float)
= coloured_coordinate.
coloured_coordinate_translate(coloured_coordinate(X, Y, Colour), Dx, Dy)
= coloured_coordinate(X + Dx, Y + Dy, Colour).
If we call ‘translate/3’ with the first argument having type ‘coloured_coordinate’, this will invoke ‘coloured_coordinate_translate’. Likewise, if we call ‘translate/3’ with the first argument having type ‘coordinate’, this will invoke ‘coordinate_translate’.
Further instances of the type class could be made, e.g. a type that represents the point using polar coordinates.
Since methods may be defined using clauses, and the interface sections of modules may not include clauses, instance declarations that specify method definitions may appear only in the implementation section of a module. If you want to export the knowledge that a type, or a sequence of types, is a member of a given typeclass, then put a version of the instance declaration that omits all method definitions (see Abstract instance declarations) into the interface section of the module that contains the full instance declaration in its implementation section.
Abstract typeclass declarations are typeclass declarations whose definitions are hidden. An abstract typeclass declaration has the same form as a typeclass declaration, but without the ‘where[…]’ part. An abstract typeclass declaration defines a name for a set of (sequences of) types, but does not define what methods must be implemented for instances of the type class.
Like abstract type declarations, abstract typeclass declarations are only useful in the interface section of a module. Each abstract typeclass declaration must be accompanied by a corresponding non-abstract typeclass declaration that defines the methods for that type class.
Non-abstract instance declarations can only be made in scopes where the non-abstract typeclass declaration is visible.
Abstract instance declarations are instance declarations whose implementations are hidden. An abstract instance declaration has the same form as an instance declaration, but without the ‘where […]’ part. An abstract instance declaration declares that a sequence of types is an instance of a particular type class without defining how the type class methods are implemented for those types. Like abstract type declarations, abstract instance declarations are only useful in the interface section of a module. Each abstract instance declaration must be accompanied in the implementation section of the same module by a corresponding non-abstract instance declaration that defines how the type class methods are implemented.
Here is an example:
:- module hashable.
:- interface.
:- import_module int, string.
:- typeclass hashable(T) where [func hash(T) = int].
:- instance hashable(int).
:- instance hashable(string).
:- implementation.
:- instance hashable(int) where [func(hash/1) is hash_int].
:- instance hashable(string) where [func(hash/1) is hash_string].
:- func hash_int(int) = int.
hash_int(X) = X.
:- func hash_string(string) = int.
hash_string(S) = H :-
% Use the standard library predicate string.hash/2.
string.hash(S, H).
:- end_module hashable.
Mercury allows a type class constraint to appear as part of a predicate or function’s type signature. This constrains the values that can be taken by type variables in the signature to belong to particular type classes.
A type class constraint has the form:
<= Typeclass(Type, …), …
where Typeclass is the name of a type class and Type is a type. Any variable that appears in Type must be determined by the predicate’s or function’s type signature. A variable is determined by a type signature if it appears in the type signature, but if functional dependencies are present, then it may also be determined from other variables (see Functional dependencies). Each type class constraint in a predicate or function declaration must contain at least one variable.
For example
:- pred distance(P1, P2, float) <= (point(P1), point(P2)).
:- mode distance(in, in, out) is det.
distance(A, B, Distance) :-
coords(A, Xa, Ya),
coords(B, Xb, Yb),
XDist = Xa - Xb,
YDist = Ya - Yb,
Distance = sqrt(XDist*XDist + YDist*YDist).
In the above example,
the distance predicate
is able to calculate the distance between any two points,
regardless of their representation,
as long as the coords operation has been defined.
These constraints are checked at compile time.
Type class constraints may also appear in typeclass declarations,
meaning that one type class is a “superclass” of another.
The arguments of a constraint on a type class declaration must be either type variables or ground types. Each constraint must contain at least one variable argument and all variables that appear in the arguments must also be arguments to the type class in question.
For example, the following declares the ‘ring’ type class, which describes types with a particular set of numerical operations defined:
:- typeclass ring(T) where [
func zero = (T::out) is det, % '+' identity
func one = (T::out) is det, % '*' identity
func plus(T::in, T::in) = (T::out) is det, % '+'/2 (forward mode)
func mult(T::in, T::in) = (T::out) is det, % '*'/2 (forward mode)
func negative(T::in) = (T::out) is det % '-'/1 (forward mode)
].
We can now add the following declaration:
:- typeclass euclidean(T) <= ring(T) where [
func div(T::in, T::in) = (T::out) is det,
func mod(T::in, T::in) = (T::out) is det
].
This introduces a new type class, euclidean,
of which ring is a superclass.
The operations defined by the euclidean type class
are div, mod,
as well as all those defined by the ring type class.
Any type declared to be an instance of euclidean
must also be declared to be an instance of ring.
Type class constraints on type class declarations gives rise to a superclass relation. This relation must be acyclic. That is, it is an error if a type class is its own (direct or indirect) superclass.
Type class constraints may also be placed upon instance declarations. The arguments of such constraints must be either type variables or ground types. Each constraint must contain at least one variable argument and all variables that appear in the arguments must be type variables that appear in the types in the instance declaration.
For example, consider the following declaration of a type class of types that may be printed:
:- typeclass portrayable(T) where [
pred portray(T::in, io.state::di, io.state::uo) is det
].
The programmer could declare instances such as
:- instance portrayable(int) where [
pred(portray/3) is io.write_int
].
:- instance portrayable(char) where [
pred(portray/3) is io.write_char
].
However, when it comes to writing the instance declaration
for a type such as list(T),
we want to be able print out the list elements
using the portray/3 for the particular type of the list elements.
This can be achieved by
placing a type class constraint on the instance declaration,
as in the following example:
:- instance portrayable(list(T)) <= portrayable(T) where [
pred(portray/3) is portray_list
].
:- pred portray_list(list(T), io.state, io.state) <= portrayable(T).
:- mode portray_list(in, di, uo) is det.
portray_list([], !IO).
portray_list([X | Xs], !IO) :-
portray(X, !IO),
io.write_char(' ', !IO),
portray_list(Xs, !IO).
For abstract instance declarations, the type class constraints on an abstract instance declaration must exactly match the type class constraints on the corresponding non-abstract instance declaration that defines that instance.
The abstract version of the above instance declaration would be
:- instance portrayable(list(T)) <= portrayable(T).
Type class constraints may include any number of functional dependencies.
A functional dependency constraint
takes the form (Domain -> Range).
The Domain and Range arguments are either single type variables,
or conjunctions of distinct type variables separated by commas.
:- typeclass Typeclass(Var, …) <= ((D -> R), …) … :- typeclass Typeclass(Var, …) <= (D1, D2, … -> R1, R2, …), …
Each type variable must appear in the parameter list of the typeclass. Abstract typeclass declarations must have exactly the same functional dependencies as their concrete forms.
Mutually recursive functional dependencies are allowed, so the following examples are legal:
:- typeclass foo(A, B) <= ((A -> B), (B -> A)). :- typeclass bar(A, B, C, D) <= ((A, B -> C), (B, C -> D), (D -> A, C)).
A functional dependency on a typeclass places an additional requirement on the set of instances which are allowed for that type class. The requirement is that all types bound to variables in the range of the functional dependency must be able to be uniquely determined by the types bound to variables in the domain of the functional dependency. If more than one functional dependency is present, then the requirement for each one must be satisfied.
For example, given the typeclass declaration
:- typeclass baz(A, B) <= (A -> B) where …
it would be illegal to have both of the instances
:- instance baz(int, int) where … :- instance baz(int, string) where …
although either one would be acceptable on its own.
The following instance would also be illegal
:- instance baz(string, list(T)) where …
since the variable T may not always be bound to the same type.
However, the instance
:- instance baz(list(S), list(T)) <= baz(S, T) where …
is legal because
the ‘baz(S, T)’ constraint ensures that
whatever T is bound to,
it is always uniquely determined from the binding of S.
The extra requirements that result from the use of functional dependencies allow the bindings of some variables to be determined from the bindings of others. This in turn relaxes some of the requirements of typeclass constraints on predicate and function signatures, and on existentially typed data constructors.
Without any functional dependencies, all variables in constraints must appear in the signature of the predicate or function being declared. However, variables which are in the range of a functional dependency need not appear in the signature, since it is known that their bindings will be determined from the bindings of the variables in the domain.
More formally, the constraints on a predicate or function signature induce a set of functional dependencies on the variables appearing in those constraints. A functional dependency ‘(A1, … -> B1, …)’ is induced from a constraint ‘Typeclass(Type1, …)’ if and only if the typeclass ‘Typeclass’ has a functional dependency ‘(D1, … -> R1, …)’, and for each typeclass parameter ‘Di’ there exists an ‘Aj’ every type variable appearing in the ‘Typek’ corresponding to ‘Di’, and each ‘Bi’ appears in the ‘Typej’ bound to the typeclass parameter ‘Rk’ for some k.
For example, with the definition of baz above,
the constraint baz(map(X, Y), list(Z))
induces the constraint (X, Y -> Z),
since X and Y appear in the domain argument,
and Z appears in the range argument.
The set of type variables determined from a signature is the closure of the set appearing in the signature under the functional dependencies induced from the constraints. The closure is defined as the smallest set of variables which includes all of the variables appearing in the signature, and is such that, for each induced functional dependency ‘Domain -> Range’, if the closure includes all of the variables in Domain then it includes all of the variables in Range.
For example, the declaration
:- pred p(X, Y) <= baz(map(X, Y), list(Z)).
is acceptable since the closure of {X,
Y} under the induced functional dependency must include Z.
Moreover, the typeclass baz/2 would be allowed
to have a method that only uses the first parameter, A,
since the second parameter, B, would always be determined from the first.
Note that, since all instances must satisfy the superclass constraints, the restrictions on instances obviously transfer from superclass to subclass. Again, this allows the requirements of typeclass constraints to be relaxed. Thus, the functional dependencies on the ancestors of constraints also induce functional dependencies on the variables, and the closure that we calculate takes these into account.
For example, in this code
:- typeclass quux(P, Q, R) <= baz(R, P) where … :- pred q(Q, R) <= quux(P, Q, R).
the signature of q/2 is acceptable
since the superclass constraint on quux/2
induces the dependency ‘R -> P’ on the type variables,
hence P is in the closure of {Q, R}.
The presence of functional dependencies
also allows “improvement” to occur during type inference.
This can occur in two ways.
First, if two constraints of a given class match
on all of the domain arguments of a functional dependency on that class,
then it can be inferred that they also match on the range arguments.
For example,
given the constraints baz(A, B1) and baz(A, B2),
it will be inferred that B1 = B2.
Similarly, if a constraint of a given class is subsumed by a known instance of that class in the domain arguments, then its range arguments can be unified with the corresponding instance range arguments. For example, given the instance:
:- instance baz(list(T), string) where …
then the constraint baz(list(int), X)
can be improved with the inference that X = string.
Previous: Type class constraints on instance declarations, Up: Type classes [Contents]