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, [EMAIL PROTECTED] <[EMAIL PROTECTED]> 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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
