Version 19 (modified by 11 years ago) (diff)  ,

Functional Dependencies
Brief Explanation
Functional dependencies (borrowed from relational databases) restrict the instances of a multiparameter type class, e.g.
class ... => C a b c  a > b
says that any two instances of C
that agree in the first parameter must also agree in the second.
They are a partial solution to the following problems with MPTCs:
 ambiguity
 imprecise types and late error reporting, arising from deferred context reduction (see FlexibleContexts).
References
 Type Classes with Functional Dependencies by Mark P. Jones, in ESOP 2000. A semiformal description of a more restricted system than implemented by GHC and Hugs.
 Understanding functional dependencies via Constraint Handling Rules by Martin Sulzmann, Gregory J. Duck, Simon Peyton Jones, and Peter J. Stuckey, September 2005. This paper explains explores the restrictions required to guarantee sound, complete and decidable type inference in the presence of functional dependencies.
 Multiple parameter classes in the Hugs 98 User Manual
 Problems with functional dependencies (email) by SPJ + paper. See also.
 AssociatedTypes are an alternative solution.
Tickets
Pros
 In GHC and Hugs for a long time.
 Used in important libraries, notably monad transformers.
 MultiParamTypeClasses are of limited use without functional dependencies or something equivalent.
Cons
 There are (at least) three different versions of FDs, none of which is satisfactory:
 Mark Jones's original proposal. Problem: It excludes some uses of FDs (see below).
 GHC's implementation. Problem: It makes type checking undecidable (see below).
 Chameleon's implementation. Problem: Needs type inference based on constraint handling rules (not just HM). Doesn't support separate compilation atm.
 Including the dependent type parameters makes types more cluttered, and prevents hiding of these types (see AssociatedTypes).
 AssociatedTypes seem to be more promising.
Original Proposal
This is the system proposed in the original paper, with names according to the FDCHR paper.
Suppose a class C has a functional dependency X >
Y.
Restrictions on instances
The original paper imposed two restrictions on instances of the class C (sect. 6.1):
 Coverage.
For any instance
instance ... => C t
any variable occurring free in t_{Y} must also occur free in t_{X}.  Consistency.
If there is a second instance
instance ... => C s
then any substitution unifying t_{X} with s_{X} must also unify t_{Y} with s_{Y}.
Haskell 98 requires that the context of an instance declaration use only type variables that appear in the head. It was originally thought that this could be relaxed (original paper, sect. 6.3), to variables determined by those in the head, but this can lead to nontermination (CHR paper, ex. 16).
Improvement of inferred types
"Improvement", as used by Mark Jones, means using information about what instances could match a predicate to instantiate its type variables, or to fail. Note that since context reduction is deferred (see FlexibleContexts), this refers not to what instances are available, but what instances are possible.
A functional dependency X → Y allows two improvement rules:
 FD improvement. If a context contains predicates C t and C s such that t_{X} = s_{X}, infer t_{Y} = s_{Y}.
 Instance improvement.
Given a predicate C s and an instance declaration
instance ... => C t
such that s_{X} = S t_{X} for some substitution S, infer s_{Y} = S t_{Y}. (This rule is justified by the above "consistency" condition.)
Properties
With FlexibleInstances and no OverlappingInstances, this system is coherent and decidable (CHR paper, corr. 1).
Unfortunately the "coverage" condition rules out instances like the following, from the monad transformer library:
class (Monoid w, Monad m) => MonadWriter w m  m > w instance MonadWriter w m => MonadWriter w (ReaderT r m)
GHC and Hugs
GHC and Hugs implement the following relaxed version of the above "coverage" condition:
 Dependency.
For any instance
instance ctxt => C t
any variable occurring free in t_{Y} must be dependent (using dependencies of classes in the context) on variables that occur free in t_{X}.
They thus accept instances like the above MonadWriter
example.
Unfortunately, this relaxation breaks the guarantees of termination and coherence.
Loss of termination
The following instances (CHR paper, ex. 6) seem reasonable:
class Mul a b c  a b > c where (.*.) :: a > b > c instance Mul Int Int Int where (.*.) = (*) instance Mul Int Float Float where x .*. y = fromIntegral x * y instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
and yet instance inference fails to terminate for the following (erroneous) definition:
f = \ b x y > if b then x .*. [y] else y
Loss of confluence
The following instances (adapted from CHR paper, ex. 18) are sensitive to the order in which rules are applied:
class B a b  a > b class C a b c  a > b where f :: a > b > c > Bool instance B a b => C [a] b Bool
Given the constraint C [a] b Bool, C [a] c d
,
 if we apply the dependency first, and then reduce using the instances, we obtain
b = c, B a b, C [a] b d
.
 if we first reduce using the instances, we obtain
B a b, C [a] b d
.
(GHC and Hugs yield the former, because they defer context reduction: see FlexibleContexts).
Proposed Fixes
The following are alternatives.
Modified coverage condition
The following complex relaxation of the "coverage" condition is safe (CHR paper, sect. 6), and allows the instances in the monad transformer library:
 For any instance
instance ... => C t
either any variable occurring free in t_{Y} must also occur free in t_{X}, or
 the functional dependency is full (involves all the arguments of the class), and the arguments t_{Y} are type variables determined by the free variables of t_{X}.
The fullness condition restores confluence, while the variable argument condition restores termination.
Note that functional dependencies corresponding to associated type synonyms are always full.
Modified instance improvement
Assume the dependency condition in place of coverage. For an instance
instance ... => C t
if t_{Y} is not covered by t_{X}, then for any constraint C s
with s_{X} = S t_{X}, there cannot be another matching instance (as it would violate the consistency condition).
Hence we can unify s with S t.
Local confluence is straightforward.
(In the above confluence example, d
is instantiated to Bool
and both alternatives reduce to b = c, d = Bool, B a b
).
To guarantee termination, we would need to require that for any instance C t, each argument is either covered by t_{X} or is a single variable.
Attachments (1)

thoughtsOnMixing.ps (87.2 KB)  added by 11 years ago.
possible use case for FunctionalDependencies
Download all attachments as: .zip