[Haskell-cafe] Re: A question about functional dependencies and existential

[Nicolas Frisby]

A wee bit off topic... but bear with me.

Oleg points out a distinction between declaring a class with
functional dependencies and implementing a class with functional
dependencies. Judging from my experience, it might behoove those
wrestling with type classes and FDs to emphasize that the class
declaration also merely declares the functional dependencies and does
not guarantee them as type-level functions. Moreover, instances
implementing the class implement the functional dependencies as well.
However, just because GHC accepts the instances as satisfying the
functional dependencies, it doesn't necessarily guarantee that the
functional dependencies can be aggressively used to resolve
polymorphism--let me elaborate on this last point. Consider

class C a b | a -> b where
    foo :: a -> b

instance C Int Int where
    foo = id
instance Num a => C Bool a where
    foo _ = 3

GHC 6.7.20070214 accepts this code with fglasgow-exts and undecidable
instances. I usually read the functional dependencies as "a determines
b" (and I suspect many other people do as well). Unfortunately, that
is not the guaranteed by the functional dependency analyzer. What is
guaranteed is that any two instances of C do not together contradict
the functional dependencies. Given C Bool x, I cannot infer what x is,
though I had thought that "a determines b".

When I was exercising my prefrontal Olegial cortex in writing my own
static record library a la Hlist, I learned this lesson the hard way.
Hopefully this saves the reader some trouble.

Motto: "appeasing the functional dependency analyzer DOES NOT mean
that the type class is actually a type function". Perhaps ATs do have
this quality? I'm not sure--but if they do I will definitely be a fan.

On 3/28/07, oleg at pobox.com <oleg at pobox.com> wrote:
>
> >>> class T root pos sel | pos -> root, root -> sel where
> >>>    f :: pos -> sel -> Bool
> >>> instance T root (Any root) sel
>
> > But the same applies to the second functional dependency and the type
> > variable sel. Every instantiation of root determines the instantiation
> > of sel. And that forbids instance T Int (Any Int) Bool and instance T
> > Int (Any Int) Int inside the same scope, doesn't it?
>
> Indeed that is your intent, expressed in the functional dependency. It
> may help to think of a class declaration as an `interface' and of the
> set of instances as an `implementation' (of the type class). In the
> example above, the "class T root pos sel" _declares_ a ternary
> relation T and specifies some `constraints'. The set of instances of T
> (in our example, there is only one instance) specifies the triples
> whose set defines the relation T. In Herbrand interpretation, an
> unground instance
>         instance C1 x y => C (Foo x) (Bar y)
> corresponds to a set of instances where the free type variables are
> substituted by all possible ground types provided the instance
> constraints (such as C1 x y) hold. In our example, an unground
> instance |instance T root (Any root) sel| is equivalent to a set of
> ground instances where |root| and |sel| are replaced with all possible
> ground types. Including
>         instance T Int (Any Int) Bool
>         instance T Int (Any Int) Int
> These two instances are in the model for
> `instance T root (Any root) sel'. A set of instances, an
> implementation of a type class, must satisfy the interface, that is,
> constraints imposed by the class declaration, including the functional
> dependency constraints. In our example, any implementation of T must
> satisfy root -> sel constraints. The above two instances show there
> exists a model of T where the functional dependency is
> violated. That's why both GHC 6.4 and Hugs reject the instance. Again,
> it is a mystery why GHC 6.6 accepts it.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>