[Haskell-cafe] are Monads with slightly stricter types in instances still Monads?

[Bryan Donlan]

Julien Oster wrote:
> Hello,
> 
> The type of the monadic bind function in the Monad class is
> 
> Monad m => m a -> (a -> m b) -> m b
> 
> Now, would it be possible to create a monad with a slightly stricter 
> type, like
> 
> StrictMonat m => m a -> (a -> m a) -> m a
> 
> and, accepting that all steps of the computation would be bound to 
> operate on the same type, would this be without any undesirable 
> implications?

It's possible, but it would be difficult to work with, I think. You 
wouldn't be able to do anything in the monad which takes any argument or 
returns any value other than type a, obviously, which would make things 
unwieldy to work with.

You could define:

class TypedMonadishThing m where
   returnS :: a -> m a
   bindS   :: m a -> (a -> m a) -> m a

But this bears little resembelance to Monad, as it's impossible to 
define join in it - join being a part of the fundamental theoretical 
structure of monads:
join :: Monad m => m (m a) -> m a


> For the sake of understanding monads better, I tried to write several 
> custom monads which may or may not be useful. Among those were:
> 
>  * The Tracker Monad - tracks every result of every step of the
>    sequential computation in a (normal, stricly typed) list inside
>    of the monad

This sounds a bit like the Writer monad...

>  * The Goto Monad - sequential computation that allows restarts of
>    the computation at arbitrarily set labels within it

And this a bit like Cont :)

> 
> But Haskell doesn't like those. Rightly so, because the bind function 
> would have the stricter type mentioned above.
> 
> [Otherwise the Tracker monad would have to store values of different 
> types in its list and the Goto monad would encounter restarts at labels 
> that process different types of the value than what has been computed so 
> far. Both doesn't make sense.]

The Writer monad (import Control.Monad.Writer) avoids the problem in 
your Tracker monad by explicitly annotating when you want to emit some 
output, with the tell function:
tell :: (MonadWriter w m, Monoid w) => w -> m ()

You can always add an annotation to catch the output of a function as well:
watch :: (MonadWriter [r] m) => m r -> m r
watch m = do
   result <- m
   tell [result]
   return result

You can run a monad like this with:
runWriter :: Writer w a -> (a, w)



And Cont (Control.Monad.Cont) avoids the problems with types by 
explicitly annotating the continuation with the type it expects:
callCC :: (MonadCont m) => ((a -> m b) -> m a) -> m a

You could use this as in:
foo = callCC $ \exitEarly -> do
   -- complex computation
   when someCondition $ exitEarly result

Cont's a bit tricky though, your computation is also annotated with its 
/final/ result, so:
runCont :: Cont r a -> (a -> r) -> r
runCont . callCC :: ((a -> Cont r b) -> Cont r a) -> (a -> r) -> r

You could run the above foo like:
runCont foo id
where id is a function run on the final result of the continuation.

> 
> I still have to prove wether those two monads follow the monadic laws at 
> all, but that's part of my exercise. But let's say they follow the laws 
> (I'm pretty sure that at least the Tracker monad does), is there 
> anything else that would prevent the stricter typing from being legal or 
> useful? Maybe I'm missing something simple.
> 
> And would I still be able to use Haskell's "do" syntax? My first guess 
> is yes, because it really just seems to translate into normal syntax.

You might be able to trick the desugarer into accepting it by:
import Prelude hiding (Monad(..))

but this is probably not what you want. The types of everything to the 
left of a <- in such a do syntax would need to be the same.