are Monads with slightly stricter types in instances still Monads?

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? 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 * The Goto Monad - sequential computation that allows restarts of the computation at arbitrarily set labels within it 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.] 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. Thanks, Julien

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.
participants (2)
-
Bryan Donlan
-
Julien Oster