Difficulty using supermonad with MSFs

[ivanperez-keera]

Hi

I have a version of a reactive framework that works ok with different kinds of effects/indexed-like monads. This is based on [1].

I'm trying to make some things work with the API provided by supermonad, and using constrained monads. I find the separation between Bind and Return appealing, and I've found the notion of indexed and graded monads useful in a specific domain.

I'm having trouble compiling this version with constrained monads, though. Hope you can tell me if I'm doing something wrong (or if something could be done better). Sample code:

The basic type just takes an input and returns, in a monadic context, an output and a continuation.

import Control.Supermonad.Constrained.Prelude

newtype MSF m a b = MSF { step :: a -> m (b, MSF m a b) }

For example, applying a transformation point-wise is straightforward. With monads, it would be:

arrM :: Monad m => (a -> m b) -> MSF m a b
arrM f = MSF $ \a -> f a >>= \b -> return (b, arrM f)

However, for constrained monads, signatures get more sophisticated:

arrM :: (Return m, Bind m m m, BindCts m m m b (b, MSF m a b), ReturnCts m (b, MSF m a b)) => (a -> m b) -> MSF m a b
arrM f = MSF $ \a -> do
  b <- f a
  return (b, arrM f)

But that works. Composition is the thing that's not working. I've commented the signature, because it does not type-check. It assumes there may be an intermediate monad n0 and an intermediate result may be of that type.

-- compM  ::  forall m1 m2 m3 a b c
--        .   ( Return m1, Return m2, Return m3, Bind m1 m2 m3, Bind m3 m3 m3, Bind m2 m2 m2, Bind m1 m1 m1, ReturnCts m3 (c, MSF m3 a c))
--        =>  MSF m1 a b
--        ->  MSF m2 b c
--        ->  MSF m3 a c
compM (MSF msf1) (MSF msf2) = MSF $ \a -> do
  (r1, msf1') <- (msf1 a)        -- :: m1 (b, MSF m1 a b)
  (r2, msf2') <- (msf2 r1)       -- :: m2 (c, MSF m2 b c)
  return (r2, compM msf1' msf2') -- :: m3 (c, MSF m3 a c)

Stupidly enough, this works in Idris, and requires (Return m3, Bind m1 m2 m3, Bind m2 m2 m2).

I'm compiling with the right flags: -fplugin Control.Supermonad.Plugin -dynamic -dcore-lint.

I suspect it may have to do with the default associativity of bind, but I'm not sure.

Do you know what may be going on here?

[1] http://github.com/ivanperez-keera/dunai

[ivanperez-keera]

Ok... somehow this works with the signature:

compM  ::  ( Bind m1 m2 m3
           , Bind m2 m2 m2
           , Return m3
           , Return m2 
           , ReturnCts m3 (c, MSF m3 a c)
           , BindCts m1 m2 m3 (b, MSF m1 a b) (c, MSF m3 a c)
           , ReturnCts m2 (c, MSF m3 a c)
           , BindCts m2 m2 m2 (c, MSF m2 b c) (c, MSF m3 a c))
       =>  MSF m1 a b
       ->  MSF m2 b c
       ->  MSF m3 a c

I may have been doing something wrong before.