[Haskell-cafe] Re: Associated types and data constructors (was: the MPTC Dilemma (please solve))

[Manuel M T Chakravarty]

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