|
|
|
|
|
|
|
|
|
|
|
# Functional Dependencies
|
|
|
|
|
|
|
|
|
## Brief Explanation
|
|
|
|
|
|
|
|
|
|
|
|
Functional dependencies (borrowed from relational databases) restrict the instances of a [multi-parameter type class](multi-param-type-classes), e.g.
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
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](flexible-contexts)).
|
|
|
|
|
|
## References
|
|
|
|
|
|
|
|
|
- [ Type Classes with Functional Dependencies](http://www.cse.ogi.edu/~mpj/pubs/fundeps.html) by Mark P. Jones, in ESOP 2000. A semi-formal description of a more restricted system than implemented by GHC and Hugs.
|
|
|
- [ Simplifying and Improving Qualified Types](http://www.cse.ogi.edu/~mpj/pubs/improve.html) by Mark P. Jones (extended version of an FPCA'95 paper), provides background and theory on "improvement" of types.
|
|
|
- [ Understanding functional dependencies via Constraint Handling Rules](http://research.microsoft.com/Users/simonpj/Papers/fd-chr/) 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](http://cvs.haskell.org/Hugs/pages/hugsman/exts.html#sect7.1.1) in the Hugs 98 User Manual
|
|
|
- [ Problems](http://www.haskell.org//pipermail/haskell-prime/2006-February/000289.html) with functional dependencies (email) by SPJ + paper. [ See also](http://www.haskell.org/pipermail/haskell/2000-December/006324.html).
|
|
|
- [AssociatedTypes](associated-types) are an alternative solution.
|
|
|
|
|
|
## Tickets
|
|
|
|
|
|
|
|
|
|
|
|
<table><tr><th>[\#36](https://gitlab.haskell.org//haskell/prime/issues/36)</th>
|
|
|
<td>add FunctionalDependencies</td></tr>
|
|
|
<tr><th>[\#90](https://gitlab.haskell.org//haskell/prime/issues/90)</th>
|
|
|
<td>solve the MultiParamTypeClassDilemma</td></tr></table>
|
|
|
|
|
|
|
|
|
|
|
|
## Pros
|
|
|
|
|
|
|
|
|
- In GHC and Hugs for a long time.
|
|
|
- Used in important libraries, notably monad transformers.
|
|
|
- [MultiParamTypeClasses](multi-param-type-classes) 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:
|
|
|
|
|
|
1. Mark Jones's original proposal. Problem: It excludes some uses of FDs (see below).
|
|
|
1. GHC's implementation. Problem: It makes type checking undecidable (see below).
|
|
|
1. 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](associated-types)).
|
|
|
- [AssociatedTypes](associated-types) seem to be more promising, but in their current form are not quite as general as functional dependencies ([ http://www.haskell.org/pipermail/haskell-prime/2011-June/003423.html](http://www.haskell.org/pipermail/haskell-prime/2011-June/003423.html)).
|
|
|
|
|
|
## Original Proposal
|
|
|
|
|
|
|
|
|
|
|
|
This is the system proposed in the original paper, with names according to the FD-CHR 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):
|
|
|
|
|
|
|
|
|
1. **Coverage.**
|
|
|
For any instance
|
|
|
|
|
|
```wiki
|
|
|
instance ... => C t
|
|
|
```
|
|
|
|
|
|
any variable occurring free in t<sub>Y</sub> must also occur free in t<sub>X</sub>.
|
|
|
1. **Consistency.**
|
|
|
If there is a second instance
|
|
|
|
|
|
```wiki
|
|
|
instance ... => C s
|
|
|
```
|
|
|
|
|
|
then any substitution unifying t<sub>X</sub> with s<sub>X</sub> must also unify t<sub>Y</sub> with s<sub>Y</sub>.
|
|
|
|
|
|
|
|
|
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 non-termination (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](flexible-contexts)), this refers not to what instances are available, but what instances are possible.
|
|
|
|
|
|
|
|
|
|
|
|
A functional dependency X → Y allows two improvement rules:
|
|
|
|
|
|
|
|
|
1. **FD improvement.**
|
|
|
If a context contains predicates C t and C s such that t<sub>X</sub> = s<sub>X</sub>, infer t<sub>Y</sub> = s<sub>Y</sub>.
|
|
|
1. **Instance improvement.**
|
|
|
Given a predicate C s and an instance declaration
|
|
|
|
|
|
```wiki
|
|
|
instance ... => C t
|
|
|
```
|
|
|
|
|
|
such that s<sub>X</sub> = S t<sub>X</sub> for some substitution S, infer s<sub>Y</sub> = S t<sub>Y</sub>.
|
|
|
(This rule is justified by the above "consistency" condition.)
|
|
|
|
|
|
### Interaction with superclasses
|
|
|
|
|
|
|
|
|
|
|
|
The original version makes no changes to the treatment of superclasses, so given the classes (sect. 7)
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
class U a b | a -> b
|
|
|
class U a b => V a b
|
|
|
```
|
|
|
|
|
|
|
|
|
the constraint set `U a b, V a c` is irreducible.
|
|
|
(Adding a dependency to V does not change this.)
|
|
|
In GHC and Hugs, and the system studied in DF-CHR, the improvement rules are applied to the closure of the constraint set under superclasses.
|
|
|
In this example, that is `U a b, U a c, V a c`, so the functional dependency implies `b = c`.
|
|
|
(This example can also be rearranged to show nonconfluence for the original system.)
|
|
|
|
|
|
|
|
|
### Properties
|
|
|
|
|
|
|
|
|
- With [FlexibleInstances](flexible-instances) and no [OverlappingInstances](overlapping-instances), this system is coherent and decidable (CHR paper, corr. 1).
|
|
|
|
|
|
- Because it ignores the context, the "coverage" condition does not allow some instances for "transformere", e.g. in the monad transformer library (see [Use Cases](functional-dependencies#use-cases) below).
|
|
|
|
|
|
## GHC and Hugs
|
|
|
|
|
|
|
|
|
|
|
|
GHC and Hugs implement the following relaxed version of the above "coverage" condition:
|
|
|
|
|
|
|
|
|
1. **Dependency.**
|
|
|
For any instance
|
|
|
|
|
|
```wiki
|
|
|
instance ctxt => C t
|
|
|
```
|
|
|
|
|
|
any variable occurring free in t<sub>Y</sub> must be dependent (using dependencies of classes in the context) on variables that occur free in t<sub>X</sub>.
|
|
|
|
|
|
|
|
|
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:
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
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:
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
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:
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
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\] c d``.
|
|
|
|
|
|
|
|
|
(GHC and Hugs yield the former, because they defer context reduction: see [FlexibleContexts](flexible-contexts)).
|
|
|
|
|
|
|
|
|
## Proposed Fixes
|
|
|
|
|
|
|
|
|
|
|
|
The following are alternatives, based on different analyses of the above confluence problem.
|
|
|
|
|
|
|
|
|
### 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:
|
|
|
|
|
|
|
|
|
1. For any instance
|
|
|
|
|
|
```wiki
|
|
|
instance ... => C t
|
|
|
```
|
|
|
|
|
|
either
|
|
|
|
|
|
- any variable occurring free in t<sub>Y</sub> must also occur free in t<sub>X</sub>, or
|
|
|
- the functional dependency is *full* (involves all the arguments of the class), and the arguments t<sub>Y</sub> are distinct type variables determined by the free variables of t<sub>X</sub>.
|
|
|
|
|
|
|
|
|
The fullness condition restores confluence, while the variable argument condition restores termination (by making instance improvement trivial).
|
|
|
|
|
|
|
|
|
|
|
|
Note that functional dependencies corresponding to [associated type synonyms](associated-types) are always full.
|
|
|
|
|
|
|
|
|
### Modified instance improvement
|
|
|
|
|
|
|
|
|
|
|
|
Assume the dependency condition in place of coverage.
|
|
|
For an instance
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
instance ... => C t
|
|
|
```
|
|
|
|
|
|
|
|
|
if t<sub>Y</sub> is not covered by t<sub>X</sub>, then for any constraint `C s` with s<sub>X</sub> = S t<sub>X</sub>, there cannot be another matching instance (as it would violate the consistency condition).
|
|
|
Hence we can unify s with S t.
|
|
|
Local confluence is straight-forward.
|
|
|
(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<sub>X</sub> or is a single variable.
|
|
|
|
|
|
|
|
|
### Modified instance reduction
|
|
|
|
|
|
|
|
|
|
|
|
Another possibility is to modify instance reduction to record the functional dependency on the constraint being reduced (see [ http://www.cs.kent.ac.uk/\~cr3/chr/Tc2CHR.hs](http://www.cs.kent.ac.uk/~cr3/chr/Tc2CHR.hs)).
|
|
|
|
|
|
|
|
|
## Use Cases
|
|
|
|
|
|
|
|
|
<table><tr><th>[ Monad Transformers library](http://www.haskell.org/ghc/docs/6.4/html/libraries/mtl/) ([ new version](http://www.csee.ogi.edu/~diatchki/monadLib))</th>
|
|
|
<td>
|
|
|
Auxiliary parameters (state, errors, output, environment) are determined by the monad, e.g.:
|
|
|
|
|
|
```wiki
|
|
|
class (Monoid w, Monad m) => MonadWriter w m | m -> w
|
|
|
```
|
|
|
|
|
|
All dependencies are full, and there are two sorts of instances:
|
|
|
base case satisfying the coverage condition, e.g.
|
|
|
|
|
|
```wiki
|
|
|
instance (Monoid w, Monad m) => MonadWriter w (WriterT w m)
|
|
|
```
|
|
|
|
|
|
and transformer applications where the dependency is derived from dependencies in the context, e.g.
|
|
|
|
|
|
```wiki
|
|
|
instance (Error e, MonadWriter w m) => MonadWriter w (ErrorT e m)
|
|
|
```
|
|
|
|
|
|
</td></tr></table>
|
|
|
|
|
|
|
|
|
<table><tr><th>[ Edison](http://www.eecs.tufts.edu/~rdocki01/edison.html) data structures library</th>
|
|
|
<td>
|
|
|
Keys (or elements of sets) are determined by the collection, e.g.
|
|
|
|
|
|
```wiki
|
|
|
class (Coll c a, OrdCollX c a) => OrdColl c a | c -> a
|
|
|
```
|
|
|
|
|
|
The most complex case is represented by adaptors like
|
|
|
|
|
|
```wiki
|
|
|
instance (OrdColl h a, Ord a) => OrdColl (Min h a) a
|
|
|
```
|
|
|
|
|
|
All dependencies are full and all instances satisfy the coverage condition.
|
|
|
</td></tr></table>
|
|
|
|
|
|
|
|
|
<table><tr><th>[ collections](http://darcs.haskell.org/packages/collections/) package</th>
|
|
|
<td>
|
|
|
Elements are determined by the collection, e.g.
|
|
|
|
|
|
```wiki
|
|
|
class Foldable c o => Collection c i o | c -> i o
|
|
|
```
|
|
|
|
|
|
The most complex case is represented by views like
|
|
|
|
|
|
```wiki
|
|
|
instance Collection m (k,v) (k,v) => Collection (KeysView m k v) (k,v) k
|
|
|
```
|
|
|
|
|
|
All dependencies are full and all instances satisfy the coverage condition.
|
|
|
</td></tr></table>
|
|
|
|
|
|
|
|
|
<table><tr><th>[ Yampa](http://www.haskell.org/yampa/)</th>
|
|
|
<td>
|
|
|
Vector spaces, with the scalar type determined by the vector type.
|
|
|
Some non-full dependencies, but all instances satisfy the coverage condition.
|
|
|
</td></tr></table>
|
|
|
|
|
|
|
|
|
<table><tr><th>possible use in Hat tracer</th>
|
|
|
<td>
|
|
|
[thoughtsOnMixing.ps](/attachment/wiki/FunctionalDependencies/thoughtsOnMixing.ps)[](/raw-attachment/wiki/FunctionalDependencies/thoughtsOnMixing.ps)
|
|
|
</td></tr></table>
|
|
|
|
|
|
|
|
|
|
|
|
Functional dependencies are often used in fairly experimental work together with [UndecidableInstances](undecidable-instances) and [OverlappingInstances](overlapping-instances), but since those are unlikely to be included in Haskell', they are not considered further here.
|
|
|
|
|
|
|
|
|
---
|
|
|
|
|
|
|