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

[David Menendez]

(I've moved this from haskell' to haskell-cafe, because it's more a
question about associated types than about resolving the MPTC dilemma.)

Bulat Ziganshin writes:

> Hello Manuel,
>
> MMTC> My statement remains:  Why use a relational notation if you can 
> MMTC> have a functional one?
> 
> how about these examples?
> 
> MMTC>   class Monad m => RefMonad m where
> MMTC>     type Ref m :: * -> *
> 
> can i use `Ref` as type function? for example:
> 
> data StrBuffer m = StrBuffer (Ref m Int)
>                              (Ref m String)
>                              

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)

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.

Sure, it's still possible to do this:

    instance MonadCC m => MonadPlus (SR (Prompt m) m)
    
but that doesn't feel like a big win.
-- 
David Menendez <zednenem at psualum.com> | "In this house, we obey the laws
<http://www.eyrie.org/~zednenem>      |        of thermodynamics!"