A question about functional dependencies and existential quantification
Jean-Marie Gaillourdet wrote
I am trying to do something like the following:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} module TestCase where
data Any root = forall pos sel . T root pos sel => ANY pos
class T root pos sel | pos -> root, root -> sel where f :: pos -> sel -> Bool
instance T root (Any root) sel where f (ANY p) s = f p s
The code as posted seems to have a problem. The problem is noted by GHC 6.4 and hugs but is accepted by GHC 6.6. Such a change in GHC seems strange. The problem is not related to existentials, so we just drop them
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} module TestCase where
data Any root = ANY
class T root pos sel | pos -> root, root -> sel where f :: pos -> sel -> Bool instance T root (Any root) sel
test x = f ANY x
Hugs and GHC 6.4 both complain about the instance of T: Hush (September 2006 version) says ERROR "/tmp/j.hs":9 - Instance is more general than a dependency allows and GHC 6.4.2 says Illegal instance declaration for `T root (Any root) sel' (the instance types do not agree with the functional dependencies of the class) In the instance declaration for `T root (Any root) sel' I concur. The class declares T as being a ternary relation such that the following holds forall r p p' s s'. T(r,p,s) && T(r,p',s') -> s = s' Now, the instance `T root (Any root) sel' is satisfied when root=Int, sel = Bool and when root=Int, sel = Int. Does it not? That falsifies the above proposition. In other words, the instance T is not functional with respect to the first and the third arguments. That is not surprising. What is surprising is why GHC 6.6 accepts such an instance?
Hi, oleg@pobox.com wrote:
The problem is not related to existentials, so we just drop them
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} module TestCase where
data Any root = ANY
class T root pos sel | pos -> root, root -> sel where f :: pos -> sel -> Bool instance T root (Any root) sel
test x = f ANY x
Hugs and GHC 6.4 both complain about the instance of T: Hush (September 2006 version) says ERROR "/tmp/j.hs":9 - Instance is more general than a dependency allows
and GHC 6.4.2 says
Illegal instance declaration for `T root (Any root) sel' (the instance types do not agree with the functional dependencies of the class) In the instance declaration for `T root (Any root) sel'
As I understand functional dependencies, and I am definitely _not_ an expert on them, they state, that given the lhs of a dependency is instantiated, the type variables of the rhs are determined, too. If that is correct, I don't understand why this instance should be to general, as every instantiation of "root" exactly determines the corresponding instantiation of "Any root".
I concur. The class declares T as being a ternary relation such that the following holds forall r p p' s s'. T(r,p,s) && T(r,p',s') -> s = s' Now, the instance `T root (Any root) sel' is satisfied when root=Int, sel = Bool and when root=Int, sel = Int. Does it not? That falsifies the above proposition. In other words, the instance T is not functional with respect to the first and the third arguments.
That is not surprising. What is surprising is why GHC 6.6 accepts such an instance?
GHC 6.6 does not accept such instances. Add the following code to the module TestCase
instance T Int Int Int instance T Int Int Bool
and you get the following error: TestCase.hs:10:0: Functional dependencies conflict between instance declarations: instance T Int Int Int -- Defined at TestCase.hs:10:0 instance T Int Int Bool -- Defined at TestCase.hs:11:0 -- Jean-Marie
On 3/27/07, Jean-Marie Gaillourdet
I concur. The class declares T as being a ternary relation such that the following holds forall r p p' s s'. T(r,p,s) && T(r,p',s') -> s = s' Now, the instance `T root (Any root) sel' is satisfied when root=Int, sel = Bool and when root=Int, sel = Int. Does it not? That falsifies the above proposition. In other words, the instance T is not functional with respect to the first and the third arguments.
That is not surprising. What is surprising is why GHC 6.6 accepts such an instance?
GHC 6.6 does not accept such instances. Add the following code to the module TestCase
instance T Int Int Int instance T Int Int Bool
I'm not an expert as well, but I think oleg was actually talking about
instance T Int (Any Int) Int instance T Int (Any Int) Bool
which also fails (on GHC 6.6) with: Functional dependencies conflict between instance declarations: instance T Int (Any Int) Int -- Defined at ... instance T Int (Any Int) Bool -- Defined at ... although just
instance T root (Any root) sel
is accepted. -- Felipe.
Jean-Marie Gaillourdet wrote:
class T root pos sel | pos -> root, root -> sel where f :: pos -> sel -> Bool instance T root (Any root) sel If that is correct, I don't understand why this instance should be to general, as every instantiation of "root" exactly determines the corresponding instantiation of "Any root".
The class T has two functional dependencies: pos -> root and root->sel. I believe you are talking about the former whereas my previous message was talking about the latter.
Hi Oleg and others, oleg@pobox.com wrote:
Jean-Marie Gaillourdet wrote:
class T root pos sel | pos -> root, root -> sel where f :: pos -> sel -> Bool instance T root (Any root) sel If that is correct, I don't understand why this instance should be to general, as every instantiation of "root" exactly determines the corresponding instantiation of "Any root".
The class T has two functional dependencies: pos -> root and root->sel. I believe you are talking about the former whereas my previous message was talking about the latter.
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? At least, that is what I would like to express by those two fundeps.
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.
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
oleg@pobox.com:
[...] 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.
Actually, GHC 6.6 does reject cases like the one discussed in this thread, but the check is not performed at the point of instance declaration. Instead, it is deferred until the point of use. For example:
{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
data Any a = Any
class Foo a b | a -> b where foo :: a -> b instance Foo (Any a) b where foo = undefined
test1 :: Char test1 = foo (Any :: Any Int)
GHC 6.6 compiles the above without error. But add this:
test2 :: Bool test2 = foo (Any :: Any Int)
And we get: Couldn't match expected type `Char' against inferred type `Bool' When using functional dependencies to combine Foo (Any Int) Bool, arising from use of `foo' at fd.hs:16:8-27 Foo (Any Int) Char, arising from use of `foo' at fd.hs:13:8-27
Hallo,
On 3/29/07, Nicolas Frisby
A wee bit off topic... but bear with me.
More off-topic... but bear with me. :-) I'm starting with Haskell. I'm writing a real application with Gtk2hs and HDBC for a small furniture shop. I have enjoyed it very much so far, and I like the productivity boost. But I do not understand GADTs or functional dependencies yet. When I read threads such as this I begin to think. Are these black magic type skills necessary for day-to-day work, or just for tasks not doable in other languages, or at least not doable without much effort? Are they for working around some problems of HM type systems or do they give Haskell super-language powers? I guess I could answer these questions if I understood what FD and GATDs are all about, but I'm not just there yet. :-) Cheers, -- -alex
Are they for working around some problems of HM type systems or do they give Haskell super-language powers? I guess I could answer these questions if I understood what FD and GATDs are all about, but I'm not just there yet. :-)
When you are done with furniture and decide to help us with abstract algebra then you will benefit from GADT. But curiosity shouldn't wait : http://www.cs.nott.ac.uk/~pni/Papers/Notes/GADTs.html Perhaps the proverbial cat didn't know that:-) Cheers, -Andrzej
readers of this thread might find ghc ticket #1241 relevant http://hackage.haskell.org/trac/ghc/ticket/1241
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. ..
then i wonder why that intent is not taken into account in the semantics you outline, which is widely used, but stems from the days before functional dependencies.
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'.
yes, but are they still in the model for that instance _under the dependency_? instance T root (Any root) sel | Any root->root,root->sel the difference seems a bit like that between these two qualified lists [instance T root (Any root) sel | root<-types,sel<-types] vs [instance T root (Any root) sel | root<-types,sel<-types,Any root->root,root->sel] where one can either complain that some elements of the first list do not fulfill some of the qualifiers in the second, or one can filter out those elements, and see whether the remainder is useable. or qualified types, if we see functional dependencies as type predicates f :: T root pos sel => pos -> sel -> Bool vs f :: (T root pos sel,pos->root,root->sel) => pos -> sel -> Bool where one can either complain that f isn't as polymorphic as the first type suggests, or one can take the additional type qualifiers into account. i'm not sure i have an opinion about all this anymore - it used to seem obvious to me that FDs, like qualified types, restrict polymorphism. but it has also become obvious that not everyone agrees with what i thought was the straightforward interpretation. i would be interested, however, if you -or anyone else who hasn't given up on FDs yet, could elaborate on what is wrong with this interpretation? thanks, claus ps i don't think that questions like this will simply go away by switching to a different front-end, like associated types.
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.
| > > class T root pos sel | pos -> root, root -> sel where | > > f :: pos -> sel -> Bool | > > | > > instance T root (Any root) sel where | > > f (ANY p) s = f p s ... | That is not surprising. What is surprising is why GHC 6.6 accepts such | an instance? Well, it shouldn't. As the user manual says, the flag -fallow-undecidable-instances lifts *both* the Paterson Conditions *and* the Coverage condition. I stupidly forgot that the Coverage Condition is needed both to help guarantee termination, and to help guarantee confluence (as our own paper says!). Losing the latter is more serious, and should not be an effect of -fallow-undecidable-instances. This is the same issue as http://hackage.haskell.org/trac/ghc/ticket/1241 What to do? - Never lift the Coverage Condition - Give it a flag all to itself -fno-coverage-condition - Combine it with -fallow-incoherent-instances More work is - Implement some of the more liberal coverage conditions described in the paper Simon
participants (9)
-
Alex Queiroz -
Andrzej Jaworski -
Claus Reinke -
Felipe Almeida Lessa -
Jean-Marie Gaillourdet -
Matthew Brecknell -
Nicolas Frisby -
oleg＠pobox.com -
Simon Peyton-Jones