TypeFamilies vs. FunctionalDependencies & type-level recursion

[dm-list-haskell-prime at scs.stanford.edu]

At Wed, 15 Jun 2011 20:48:07 -0400,
Dan Doel wrote:
> 
> I know that the actual, current implementation won't violate type
> safety. But there are reasonable expectations for how *functional
> dependencies* might work that would cause problems. Here's an example.
> 
>     class C a b | a -> b
> 
>     instance C Int b
> 
>     foo :: forall a b c d. (C a c, C b d, a ~ b) => a -> b -> c -> d
>     foo _ _ x = x
> 
>     coerce :: forall a b. a -> b
>     coerce = foo (5 :: Int) (5 :: Int)
> 
> This currently gets complaints about not being able to deduce c ~ d.
> However, actually reading things as genuine functional dependencies,
> there's nothing wrong with the logic:

I don't understand how this code would work under any circumstances.
At the very least, you are missing a context for coerce and the type
of foo would have to be ... => a -> b -> c -> c.  If two types are the
same, you are not allowed to declare them to be different.

Also, it's easy to add a method of some class to do the coercion,
while it's hard to emulate polymorphic types if you don't have them.
So I'd say the current behavior is more useful--allowing massive code
reduction in some cases, while I'm not yet convinced of the utility of
what you did above.

>     instance (MonadState s m) => MonadState s (T m)
>        ==>
>     forall s m. (MSDict s m -> MSDict s (T m))
> 
> And having access to
> 
>     forall s m. MSDict s (T m)
> 
> is not at all the same as having access to
> 
>     forall m. MSDict (forall s. s) (T m)

I don't understand the difference, but admittedly I don't totally
follow your dictionary syntax.  Recall the functional dependency goes
from right to left in this case:  MonadState s m | m -> s, and
certainly the type forall m s. m -> s is equivalent to forall m. m ->
(forall s. s).  It's only when the parentheses close before the last
argument that you need higher-rank types.  But I think I'm probably
misunderstanding your example.

> > If, instead of FunctionalDependencies, the extension were called
> > ChooseInstancesWithoutKnowingAllTypeVariables, would you still have
> > this objection?
> 
> No. In that case I would object that there are ad-hoc, unprincipled
> rules for resolving instances in GHC, and there should instead be some
> theoretical grounding to guide them. :)

Ah, we find agreement!  I, too, am all in favor of rules with
theoretical grounding.  The only thing I would add is that I don't
want to have to define N^2 instances for libraries like the mtl.

David