Problem with functional dependencies

[Mark P Jones]

Hi Marcin,

| In particular, should the following be legal:
|=20
| class C a b c | a -> b c
| instance C [a] b b
| f:: C [a] b c =3D> a
| f =3D undefined
|=20
| ghc panics and Hugs rejects it.

No, it is not legal.  Even if you delete the definition of f, the code
is still not legal because the class and the instance declaration are
inconsistent.

The class declaration says that you want to define a three place =
relation
on types called C.  We can think of the entries in this relation as rows
in a table with columns headed a, b, and c:

           a  |  b  |  c
     C =3D -----+-----+------
              |     |

Before we take a look at any instance declarations, this table is empty
(i.e., there are no rows).  But the functional dependency a -> b c that
you have specified establishes a constraint that any data that gets =
added
to the table by subsequent instance declarations must satisfy.  It says
that, if two rows have the same type in the a column, then they must =
also
have the same types in the b and c columns; "the values of b and c are
uniquely determined by the value of a."

So here are two plausible instance declarations that you could use:

  instance C Int Int Char
  instance C (Maybe t) t Int

Notice that the second declaration here is really an instance scheme;
the presence of a variable "t" means that it introduces a whole family
of instances, one for each possible instantiation of the variable "t".

With these two instance declarations in hand, our table looks something
like the following:

                 a         |     b     |  c
     C =3D ------------------+-----------+------
                Int        |   Int     | Char
            Maybe Int      |   Int     | Int
            Maybe Bool     |   Bool    | Int
            Maybe Char     |   Char    | Int
            Maybe [Int]    |   [Int]   | Int
         Maybe (Maybe Int) | Maybe Int | Int
                ...        |    ...    | ...

Conceptually, of course, there are now infinitely many rows in the =
table,
so what you see here is just a small part of the relation.  But notice =
that
the data in the table is entirely consistent with the functional =
dependency
a -> b c because no two rows have the same type in the a column.

Now consider the instance declaration that you have given:

  instance C [t] s s

Again, this is an instance scheme, generating one row in the table
for each possible instantiation of variables "t" and "s".  (To avoid
confusion with the names of the columns in C, I've chosen different
variable names from the ones you've used.)  For example, based on
this instance declaration, we would expect to continue adding rows
to the table along the following lines:

              a      |   b   |   c
     C =3D ------------+-------+-------
            [Int]    |  Int  |  Int           t=3DInt, s=3DInt
            [Int]    |  Bool |  Bool          t=3DInt, s=3DBool
            [Bool]   |  Int  |  Int           t=3DBool, s=3DInt
             ...     |  ...  |  ...

I hope now that the problem is becoming clear: this instance declaration
is not consistent with the dependency; in the first two lines above, for
example, we see two rows that violate the specification because they =
have
the same value of "a", but different values for "b" and "c".

In summary, the class declaration and its associated dependency are not
consistent with the instance declaration.  If you really wanted the rows
described by the instance declaration to be part of the relation C, then
the dependency you have written is not valid.  If you really did want =
the
restriction captured by the dependency, then the instance declaration is
not valid.  Hugs can't tell which of these is the real source of the
problem, but it does report, correctly, that there is an inconsistency.

A little more generally, given the class declaration and the dependency
that you've specified, Hugs will not allow any instance declaration for
something of the form  C t1 t2 t3  if there are variables in t2 or t3
that do not appear in t1.  If this restriction were not enforced, then
it would again be possible for there to be multiple rows with the same
"a" value, but different "b" and "c" entries.

I noticed the same problem in one of the earlier examples that you sent
to the list:

| class Foo a b | a
| instance Foo Int [a]
| -- This is rejected by Hugs (with fundep a->b) but I would definitely
| -- accept it.

I hope that it is now clear why Hugs rejects this definition.

| I don't fully understand fundeps.

The specific point described above is actually discussed twice in my =
ESOP
paper, once informally, and once in a more general setting.  I encourage
you to take a look at that paper for more details.  If you're basing =
your
knowledge of fundeps on the (now quite outdated) note on my web page, or
on the section of the Hugs manual on which it was based, you may well =
have
some gaps to fill in.  I'm not too happy with the ESOP paper either; I
couldn't include as much technical material there as I wanted because of
limited space.  If you have read the ESOP paper and still have =
questions,
please let me know and I will do my best to answer them.

All the best,
Mark