How to define an instance of Monad "m a" with "a" in Typeclass Show?

Question

I would like to define a monad instance with container M as a monad and with the contained type a , which must be a member of the Show class. This restriction (which a is a member of Show ) must be provided by the type system.

I tried this, but M , unfortunately, has no right. View:

 data M = forall a. Show a => M a instance Monad M where return x = M x 

All other attempts to achieve this encounter the following problem: Since Monad is a constructor class, I do not have explicit access to type a contained element (s), so I can't limit it.

Does anyone know this solution without defining a new Monad class?

Answer 1

Well, it’s actually possible to restrict type constructor parameters in a sense using GADTs:

 data M a where M :: (Show a) => a -> M a 

Unfortunately, this will not help you here. In a sense, this actually makes the situation worse, because instead of having a Monad instance without restriction, it becomes impossible to write an instance at all.

If you look at the constructor type signature above, it clearly resembles return - which shows why what you are doing is fundamentally impossible. The type to return is: (Monad m) => a -> ma , and as always unrelated type variables are implicitly quantified at the outermost level, so you can read this as "for all possible types of a and all possible types of m that are instances from Monad , given a value of type a , you can build a value of type ma ". The phrase "for everyone" is quite literal - the return type does not just use a type variable, it actively states that any type a must be allowed.

So, in short, no. There is no way to do what you want, because the standard Monad class explicitly indicates the opposite.

Answer 2

You may not be able to accomplish exactly what you are asking for, but another possibility for your particular monad is to provide an action that clearly does what you are thinking of doing with Show . That is, suppose you have:

 data M a = {- ... -} instance Monad M where -- notice: no Show constraint {- ... -} 

Then you can additionally perform some actions:

 report :: Show a => M a -> M a 

I can’t come up with an example of using this template with Show , but I know a similar example where you can require an Ord constraint. The setup is that you would like to make a monad that is non-deterministic (for example, [a] ) but has no duplicates (for example, Set a ). Removing duplicates requires some context, such as Eq or Ord , but we cannot require this on every operation return / >>= . Therefore, instead, we require the user to explicitly indicate the points where duplicates should be combined:

 newtype Setlike a = Setlike { toList :: [a] } instance Monad Setlike where return x = Setlike [x] Setlike xs >>= f = [y | x <- xs, let Setlike ys = fx, y <- ys] collapse :: Ord a => Setlike a -> Setlike a collapse = Setlike . Data.Set.toList . Data.Set.fromList . toList 

This can be used like this:

 valuesOfInterest = collapse $ do v1 <- allValues v2 <- allValues doSomethingInteresting v1 v2 

Then, even if some pairing of v1 and v2 leads to the same value of interest, this value will appear only once as a result.

Some similar trick is probably possible for your use case.

Answer 3

Not. This is not possible, although it is easy to explain. Look at the signature like return :

 return :: Monad m => a -> ma 

The signature cannot change, so your monad must accept any type of content. Since the class type itself does not mention the type of content, there is no way to enforce restrictions on it.

One thing you can do is write this restriction for all the functions it needs and reset the global restriction. The soundness of the system is still guaranteed if you can prove the existence of the Show constraint only when necessary.

Answer 4

This is possible with some extreme blende. See the rmonad package for an implementation. However, it is probably not worth it.

Why do you need a Show restriction? It would be easier to simply provide a Show constraint at this point, then it will naturally propagate where necessary.