# Changes between Version 1 and Version 2 of FunDeps

Show
Ignore:
Timestamp:
01/05/13 12:42:55 (4 months ago)
Comment:

--

Unmodified
Removed
Modified
• ## FunDeps

v1 v2
1 Consistency of Functional Dependencies
2 --------------------------------------
1= Consistency of Functional Dependencies =
32
43The functional dependencies on a class restrict the instances that may
54be declared for a given class.  The instances of a class:
6
5{{{
76    class C a b c | b -> c where f :: ...
8
7}}}
98are consistent with its functional dependency if the following invariant holds:
10
9{{{
1110    byFD(C,1): forall a1 a2 b c1 c2. (C a1 b c1, C a2 b c2) => (c1 ~ c2)
12
11}}}
1312Please note that the question of FD-consistency is orthogonal to
1413instance coherence (i.e, uniqueness of evidence, overlapping instances,

2221
2322For example, if we have an instance:
24
23{{{
2524  I: instance F Int Int Char
26
25}}}
2726and we have a constraint `C: F Int Int a`, then we can use the
2827FD-invariant to prove that `a` must be `Char`:
28{{{
29    byFD(C,1) (C,I) :: a ~ Char
30}}}
2931
30     byFD(C,1) (C,I) :: a ~ Char
31
32
33 Checking FD-Consistency
34 -----------------------
32== Checking FD-Consistency ==
3533
3634To ensure FD-consistency, before accepting an instance we need to check

3937imported instances.  Consider adding a new instance to an FD-consistent
4038set of instances:
41
39{{{
4240    I: instance P(as,bs) => C t1(as,bs) t2(as) t3(as,bs)
43
41}}}
4442The notation `t(as)` states the variables in `t` are a subset of `as`.
4543

4745     instantiations of `I` to violate FD-consistency).  Self consistency
4846     follows if we can prove the following theorem:
49
47{{{
5048         forall as bs cs. (P, P[cs/bs]) => t3[cs/bs] ~ t3[cs/bs]
51
49}}}
5250  2. Check that `I` is FD-consistent with all existing instances of the class.
5351     So, for each existing instance, `J`:
54
52{{{
5553         J: instance Q(xs) => C s1(xs) s2(xs) s3(xs)
56
54}}}
5755     we need to show that:
58
56{{{
5957         forall as bs xs. (P,Q,s2 ~ t2) => (s3 ~ t3)
60
58}}}
6159     Assuming no type-functions in instance heads, the equality
6260     assumption is equivalent to stating that `s2` and `t2` may be
6361     unified, so another way to state our goal is:
64
62{{{
6563         forall as bs xs. (P[su], Q[su]) => (s3[su] ~ t3[su])
66
64}}}
6765     where `su` is the most general unifier of `s2` and `t2`.
6866

7472the FD-consistency follows trivially.
7573
76 Examples
77 --------
74== Examples ==
75
7876
7977  * FD-consistency is orthogonal to instance coherence.
8078
8179     FD-consistent but not coherent:
82
80{{{
8381         instance C Int Int Int where f = definition_1
8482         instance C Int Int Int where f = definition_2
85
83}}}
8684     Coherent but not FD-consistent:
87
85{{{
8886         instance C Int  Int Char where ...
8987         instance C Char Int Bool where ...
90
88}}}
9189   * FD-consistency is orthogonal to termination of instances.
9290
9391     FD-consistent but "non-terminating":
94
92{{{
9593         instance C a b c => C a b c
96
94}}}
9795     Terminating but not FD-consistent:
98
96{{{
9997         instance C Int  Int Char where ...
10098         instance C Char Int Bool where ...
101
102
99}}}