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!!!

Interlocutrix

What is the question? Assuming that you get some compiler error, could you post it? – Aesthetics

@jmg, yes, one can't write the code above, the "rank 2 constraint" is not Haskell. I want to find a way to encode such things. Sorry this is a somewhat complicated question; if you find a way to simplify it, please tell me. The above is a slight simplification of an actual use case, perhaps not an ideal toy problem. – Interlocutrix

then it would be good to here more about what you want to express and why it is not possible without the constraint kind extension. I still did not really grasp what you want to express. – Aesthetics

@jmg, edited... edited again... does that help? – Interlocutrix

Is it an option to make PrintSuitable a two-parameter class? – Mycobacterium

The reasons for not having a 2-parameter class are the same as with rmonad. You get mired if you have a function a -> b, want to write a -> m b, etc. (you'll probably get a better explanation by trying to write the Set rmonad without Suitable.) – Interlocutrix

Just curious: I've noticed you're asking a lot of questions about various forms of type-level hackery. Are you just testing the limits of the language, or are you building something with this? (It sounds like you're shooting yourself in the foot with an overly complicated design). – Respirator

@hammar, Thanks for asking, I am writing a DSL for a research project -- trying to encode reusable optimizations via monad transformers and program synthesis (I'm part of the synthesis group under Ras Bodik at UC Berkeley). A few code samples for an informal "presentation" / discussion are here: goo.gl/z3jvl . At some point, I'd love to get some design feedback; shamefully, I haven't read previous work on using monad transformers for DSLs, so I've probably made a number of design mistakes. In particular, I think I need to learn about data families... – Interlocutrix

This is now possible with QuantifiedConstraints, for example MonadTrans tr just got an implication constraint for a superclass: class (forall m. Monad m => Monad (tr m)) => MonadTrans tr – Totaquine

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.

Past

Thanks for the answer edit (I wasn't following the first links); too bad this question has gotten pushed down the stack. I'll give it a shot & accept it soon. cheers. – Interlocutrix

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 = ???

Mycobacterium

That's a very nice suggestion, but doesn't work in this case: I need to get a Suitable m a from a Suitable (t m) a. The key difference is that rlift is applied to outputs from monads lower in the stack (m instead of MyMonadT m), whereas I need to lower inputs. – Interlocutrix

Ah, I see. To be able to use m's printSuitable, you must convince the compiler that whenever there's a Suitable (t m) a instance, there's necessarily a Suitable m a instance around. Hmm. – Mycobacterium

Answer 3

A related thing is that you can define an instance:

{-# LANGUAGE FlexibleInstances, FlexibleContexts, 
UndecidableInstances, MultiParamTypeClasses #-}
module Foo where

import Control.Monad.Trans

class Suitable m a where
    foo :: m a -> Int

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

instance (PrintSuitable m, MonadTrans t, Suitable (t m) a) => Suitable m a where
    foo = const 5

instance (PrintSuitable m, MonadTrans t) => PrintSuitable (t m) where
    printSuitable = undefined

So you don't need the constraint. Will that help?

Rang

Thanks, but this doesn't look like quite what I'm interested in... I'm using the Data.Suitable library. The question will be fixed in a sec. cheers. – Interlocutrix