TypeFamilies vs. FunctionalDependencies & type-level recursion

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

At Wed, 15 Jun 2011 10:36:46 +0000,
Simon Peyton-Jones wrote:
> 
> The issue doesn't even arise with type families:
> 
> 	class MonadState m where
> 	  type State m :: *
> 
> 	instance MonadState m => MonadState (MaybeT m) where
> 	  type State (MaybeT m) = State m
> 
> So examples that fail the coverage condition in fundeps, but (as you argue) are ok because the context expresses the dependency, are sometimes just fine with type families.

Sorry, I guess that specific example works.  It's the other one (which
saves the programmer from having to define N^2 instances) that can
never work with type families.

> |  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
> 
> Why do you need the first instance?  Isn't the second sufficient for
> (StateT s m) as well?

No, because those are not the same get function.  In other words,
there's a Control.Monad.State.Class.get, and a
Control.Monad.Trans.State.Lazy.get function.  When you define the
recursive instance, you want the former, while when you define the
base case, you need the latter.  (Also, in the base case, you don't
want lift.)

Not only can I not see any way to avoid the N^2 instances with
TypeFamilies, but I can't imagine any extension ever making this
possible without threatening type safety.  (That's not saying much, of
course, given that we're dealing with the imagination of a
non-language-designer here.)

But this gets to the heart of the TypeFamilies limitation that caused
me to start this thread.  I want to be able to write code like this:

	class (Monad m) => MonadState m where
	    type MonadStateType m
	    get :: m (MonadStateType m)
	    put :: (MonadStateType m) -> m ()

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

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

but I see no hope of ever making this work, and the result if that we
have to have a separate instance for every pair of monad transformers.
One not very good suggestion would be to add something like:

	instance (Monad (t m), MonadTrans t, MonadState m) =>
            MonadState (t m) | (t m) /~ (StateT s m) where

Having closed, overlapping type families would also be a way to solve
the problem.

David