haskell -- rank n constraints? (or, monad transformers and Data.Suitable)

Question

I'm trying to write something that appears to be analagous to "rank 2 types", but for constraints instead. (Or, maybe it's not correct to assume changing -> in the definition of "rank 2 types" to => is meaningful; please edit the question if you think up better terminology).

setup

First, the Suitable typeclass (from Data.Suitable, the base of rmonad) can be used to denote types of values which can be used. In this question, I'll use

Suitable m a

to denote that value a can be used as a value for some functions of the monad m (in particular, if m is a DSL, then its values are usually a which are suitable), for example

class PrintSuitable m where
    printSuitable :: Suitable m a => a -> m ()

See the top comment for RMonad [ link ] and its source for an example of how to use Suitable. For example, one could define Suitable m (Map a b), and print the number of elements in the map.

question

goal: Now, I have a monad transformer MyMonadT, and want to make MyMonadT m a PrintSuitable instance whenever m is a PrintSuitable instance.

rank 2 constraints motivation: The issue is that the type a is introduced with regard to the printSuitable function, i.e. does not appear in the class signature. Since one can only add constraints to the class signature (additional constraints to an instance function implementation are illegal), it makes sense to say something about all a in the class signature (line 2 below).

Below shows the intended code.

instance (PrintSuitable m, MonadTrans t,
        (forall a. Suitable (t m) a => Suitable m a), -- rank 2 constraint
        ) => PrintSuitable (t m) where

    printSuitable = lift ...

-- MyMonadT doesn't change what values are Suitable, hence the rank 2 expression,
-- (forall a. Suitable (t m) a => Suitable m a) should hold true
data instance Constraints (MyMonadT m) a =
    Suitable m a => MyMonadT_Constraints
instance Suitable m a => Suitable (MyMonadT m) a where -- the important line
    constraints = MyMonadT_Constraints

instance MonadTrans MyMonadT where ...
-- now, MyMonadT m is a PrintSuitable whenever m is a PrintSuitable

-- the manual solution, without using MonadTrans, looks roughly like this
instance PrintSuitable m => PrintSuitable (t m) where
    printSuitable a = withResConstraints $ \MyMonadT_Constraints -> ...

the constraint indicated says that anything that's suitable in (t m) is suitable in m. But, of course, this isn't valid Haskell; how could one encode a functional equivalent?

Thanks in advance!!!

Answer 1

Doing what you asked for

If you look in my constraints package on hackage, there is

Data.Constraint.Forall

That can be used to create quantified constraints, and using inst with the other constraint combinators from the package and by making a helper constraint to put the argument in the right position, you can directly encode what you are asking for.

A description of the reflection machinery is on my blog.

http://comonad.com/reader/2011/what-constraints-entail-part-1/

http://comonad.com/reader/2011/what-constraints-entail-part-2/

However, this requires a bleeding edge GHC.

For many cases you can often ape this by making a rank 2 version of your particular constraint though.

class Monoid1 m where
    mappend1 :: m a -> m a -> m a
    mempty1 :: m a

but in your case you want not only a rank 2 constraint but a constraint implication.

Using the machinery from that package we could make

class SuitableLowering t m where
   lowerSuitability :: Suitable (t m) a :- Suitable m a

Then you can use

instance (PrintSuitable m, SuitableLowering t m) => PrintSuitable (t m) where

and use expr \\ lowerSuitability to manually bring into scope the Suitable m a instance in a context where you know Suitable (t m) a.

But this is a really dangerous way to express an instance, because it precludes you ever making something is of kind (* -> *) -> * -> * an instance of PrintSuitable in any other way and may interfere with defining your base case if you aren't careful!

Doing what you need

The right way to do this is to give up on defining a single instance that covers all cases, and instead define a printSuitableDefault that could be used for any appropriate transformer.

Assuming the existence of RMonadTrans as mentioned in Daniel's response

class RMonadTrans t where
    rlift :: Suitable m a => m a -> t m a

we can define:

printSuitableDefault :: (RMonadTrans t, Suitable m a) => a -> t ()
printSuitableDefault = ...

instance PrintSuitable m => PrintSuitable (Foo m) where
  printSuitable = printSuitableDefault

instance PrintSuitable m => PrintSuitable (Bar m) where
  printSuitable = printsuitableDefault

You aren't likely to have too many rmonad transformers, and this ensures that if you want to make one print a different way you have that flexibility.

Doing what you need slightly more nicely under a bleeding edge compiler

Under 7.3.x (current GHC HEAD) or later you can even use the new default declarations to make this a little less painful.

class RMonad m => PrintSuitable m where
   printSuitable :: a -> m ()
   default printSuitable :: (RMonadTrans t, RMonad n, Suitable n a, m ~ t n) => 
     a -> t n ()
   printSuitable = <the default lifted definition>

then the instances for each transformer can just look like:

instance PrintSuitable m => PrintSuitable (Foo m)
instance PrintSuitable m => PrintSuitable (Bar m)

and you can define your nice printSuitable base case for some retricted monad without worries about overlap.

Answer 2

I don't think MonadTrans will be of use here, since lift requires m to be a Monad. Can you work with

class RMonadTrans t where
    rlift :: Suitable m a => m a -> t m a

instance (RMonadTrans t, Suitable m a) => Suitable (t m) a where
    constraints = ???