Why is this not a case of the restricted monad limitation?

  • A+
Category:Languages

In the following code snippet I initially believed to have a restricted monad error (I forgot to add the Monad m => in the instance Monad (Transform m a) definition). Having read quite a bit about restricted monads I wonder why this here happens to be ok:

{-# LANGUAGE GADTs #-}  data Next a where     Todo :: a -> Next a     Done :: Next a  instance Functor Next where     fmap f Done = Done     fmap f (Todo a) = Todo (f a)  data Transform m a b = Monad m => Transform ( m(Next a) -> m(Next b) )  instance Functor (Transform m a) where     fmap f (Transform ta) = Transform tb where         tb ma = ta ma >>= return . (fmap f)  instance Applicative (Transform m a) where     pure = return     mf <*> ma = do         f <- mf         a <- ma         return (f a)  instance Monad m => Monad (Transform m a) where     return b = Transform (t b) where                         t b _ = return $ Todo b     (Transform t) >>= f = Transform (/ma -> do              a <- ma         case a of             Done -> return Done             --Todo a' -> ...         ) 

The example is rather contrived, I stripped away all irrelevant bits. (The actual problem at hand is related to this.) The crucial part is the Monad m restriction in Transform.

I don't quite see how this is different from the often-cited canonical Set-as-a-monad example, which does exhibit the restricted monad limitation.

 


Transform is not a restricted monad.

Look at Set. Set is monadic in its one argument, except said argument needs to be Ord. That is, Set is a monad on the subcategory of Hask where all the objects are in Ord.

But Transform is not a monad in the first place. Transform :: (* -> *) -> * -> * -> *, but Monad applies to things of kind * -> * (if you're going to go full category theorist, monads in general are endofunctors and should roughly have kind k -> k for some k, but Transform doesn't really fit that wider template either). The thing that is a monad is Transform m a when m is a monad. Transform m a is monad on all of Hask, as long as m is also a monad. You see the difference? Transform m a given Monad m operates on every type there is. But there is nothing I can put in the blank to make "Set given ___ operates on every type there is", because the restriction is going on the parameter that Set is monadic in, while Transform m a does not have a restriction on the type it is monadic in, but on one of the types that makes it up.

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: