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

[Claus Reinke]

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.