David Menendez:

This is something I've been wondering about for a while. Can you do that sort of thing with associated types?

As another example, consider this type class for composible continuation monads:

class Monad m => MonadCC p sk m | m -> p sk where newPrompt :: m (p a) pushPrompt :: p a -> m a -> m a withSubCont :: p b -> (sk a b -> m b) -> m a pushSubCont :: sk a b -> m a -> m b

You can use instances of this class to create backtracking monads, along these lines:

data Tree m a = HZero | HOne a | HChoice a (m (Tree m a)) newtype SR p m a = SR (forall ans. ReaderT (p (Tree m ans)) m a)

instance MonadCC p sk m => MonadPlus (SR p m)

With associated types, the MonadCC class becomes:

class Monad m => MonadCC m where type Prompt m a type SubCont m a b

newPrompt :: m (Prompt m a) pushPrompt :: Prompt m a -> m a -> m a withSubCont :: Prompt m b -> (SubCont m a b -> m b) -> m a pushSubCont :: SubCont m a b -> m a -> m b

Since |Prompt m| is determined by |m|, can we eliminate the prompt parameter from SR?

newtype SR' m a = SR' (forall ans. ReaderT (Prompt m (Tree m ans)) m a)

instance MonadCC m => MonadPlus (SR' m)

Yes, that's right.

That would presumably lead to SR' having the type

SR' :: (MonadCC m) => ReaderT (Prompt m (Tree m ans)) m a -> SR' m a

That doesn't seem like it should be a problem, since it's impossible to create a value of type |ReaderT (Prompt m (Tree m ans)) m a| unless m is an instance of MonadCC, but it also puts a context on a newtype data constructor, which isn't currently allowed.

If you go by the rules in the associated types paper, you need to put that context there. However, whether that context is really needed is the topic of an ongoing discussion. Without that sort of context, you can write programs where type errors are raised a bit later than if you have the context, but type safety doesn't seem to be affected by those contexts. The fact that newtype cannot have a context is an argument in favour of not requiring the context. As your example shows, associated types (in comparison to FDs) not only eliminate type arguments from classes, but also from data type declarations. IMHO this improves the readability of programs. Manuel