Previous: Type class constraints on instance declarations, Up: Type classes [Contents]

Type class constraints may include any number of functional dependencies.
A *functional dependency* constraint
takes the form `(`

.
The `Domain` -> `Range`)`Domain` and `Range` arguments are either single type variables,
or conjunctions of type variables separated by commas.

:- typeclassTypeclass(Var, …) <= ((D->R), …) … :- typeclassTypeclass(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 ‘

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

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]