[Haskell-cafe] RE: A question about functional dependencies and existential quantification
| 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: A question about functional dependencies and existential quantification
Hi,
[EMAIL PROTECTED] 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: A question about functional dependencies and existential quantification
On 3/27/07, Jean-Marie Gaillourdet [EMAIL PROTECTED] wrote: 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
