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@pobox.com
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe