10.8 Functional dependencies

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 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.