TypeFamilies vs. FunctionalDependencies & type-level recursion

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

At Tue, 14 Jun 2011 19:21:38 -0400,
Dan Doel wrote:
> 
> If this is really about rules for selecting instances unambiguously
> without any regard to whether some parameters are actually functions
> of other parameters, then the name "functional dependencies" is pretty
> poor.

Maybe "functional dependencies" is a poor name.  I'm not going to
argue it's a good one, just that the extension is quite useful.
Despite what the name suggests, it is most useful to think of
"| a b -> c d" as meaning "any method that uses types a and b does not
need to use types c and d for the compiler to determine a unique
instance".  Once you start thinking of fundeps that way (and always
keep in mind that contexts play no role in instance selection), then I
think it gets a bit easier to reason about fundeps.

> I know the actual implementation is, too. But it's because of the
> limited way in which fundeps are used. If I'm not mistaken, if they
> were modified to interact with local constraints more like type
> families (that is, correctly :)), then soundness would be a concern
> with these examples.

I don't think so.  Because fundeps (despite the name) are mostly about
instance selection, incoherent fundeps won't violate safety.  Your
program may incoherently chose between methods in multiple instances
that should be the same instance, but at least each individual method
is type safe.  With type families, you can actually undermine type
safety, and there's no cheating way to fix this, which is why I think
TypeFamilies could by very dangerous when combined with dynamic
loading.

> I understand why the instance resolution causes these to be different
> in Haskell. I think the first one is a bad definition by the same
> criteria (although it is in practice correct due to the constraint),
> but UndecidableInstances turns off the check that would invalidate it.

Though I realize you are unlikely ever to like lifting the coverage
condition, let me at least leave you with a better example of why
Undecidable instances are useful.  Suppose you want to define an
instance of MonadState for another monad like MaybeT.  You would need
to write code like this:

	instance (MonadState s m) => MonadState s (MaybeT m) where
	    get = lift get
	    put = lift . put

This code fails the coverage condition, because class argument
(MaybeT m) does not contain the type variable s.  Yet, unlike the
compiler, we humans can look at the type context when reasoning about
instance selection.  We know that even though our get method is
returning an s--meaning really "forall s. s", since s is mentioned
nowhere else--there is really only one s that will satisfy the
MonadState s m requirement in the context.  Perhaps more importantly,
we know that in any event, if the code compiles, the s we get is the
one that the surrounding code (calling get or put) expects.

Now if, in addition to lifting the coverage condition, you add
OverlappingInstances, you can do something even better--you can write
one single recursive definition of MonadState that works for all
MonadTrans types (along with a base case for StateT).  This is far
preferable to the N^2 boilerplate functions currently required by N
monad transformers:

	instance (Monad m) => MonadState s (StateT s m) where
	    get = StateT $ \s -> return (s, s)

	instance (Monad (t m), MonadTrans t, MonadState s m) =>
            MonadState s (t m) where
	        get = lift get
	        put = lift . put

This is not something you can do with type families.  So while
UndecidableInstances and OverlappingInstances aren't very elegant, the
fact that they can reduce source code size from O(N^2) to O(N) is a
good indication that there is some unmet need in the base language.

David