[Haskell-cafe] are Monads with slightly stricter types in
instances still Monads?
Bryan Donlan
bd.haskell at uguu.us
Tue Jan 30 14:51:47 EST 2007
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.
More information about the Haskell-Cafe
mailing list