Existential Types and Monad Transformers

Question

Context: I'm trying to create a monad error that also tracks a list of warnings, something like this:

data Dangerous a = forall e w. (Error e, Show e, Show w) => Dangerous (ErrorT e (State [w]) a) 

i.e. Dangerous a is an operation leading to (Either ea, [w]) , where e is an exponential error and w is exponential.

The problem is that I apparently can't run this thing, mainly because I don't understand existential types very well. Note:

 runDangerous :: forall ae w. (Error e, Show e, Show w) => Dangerous a -> (Either ea, [w]) runDangerous (Dangerous f) = runState (runErrorT f) [] 

This does not compile because:

 Could not deduce (w1 ~ w) from the context (Error e, Show e, Show w) ... `w1' is a rigidtype variable bound by a pattern with constructor Dangerous :: forall ae w. (Error e, Show e, Show w) => ErrorT e (State [w]) a -> Dangerous a ... `w' is a rigid type variable bound by the type signature for runDangerous :: (Error e, Show e, Show w) => Dangerous a -> (Either ea, [w]) 

I'm lost. What is w1? Why can't we conclude that this is ~ w ?

Answer 1

Existential is probably not what you want here; There is no way to "observe" the actual types associated with e or w in the value of Dangerous a , so you are completely limited to the operations given to you by Error and Show .

In other words, the only thing you know about w is that you can turn it into a String , so it can just be a String (ignoring priority to simplify things) and the only thing you know about e is that you can turn it into a String , you can include a String in it, and you have a great value for it ( noMsg ). It is not possible to claim or verify that these types are the same as any other, so when you put them in Dangerous there is no way to restore any special structure that these types can have.

What the error message says is, in fact, your type for runDangerous claims that you can turn Dangerous into (Either ea, [w]) for any e and w that have corresponding instances. This is clearly wrong: you can only turn Dangerous into this type for one choice of e and w : the one with which it was created. w1 is just that your Dangerous type is defined by a variable of type w , as well as runDangerous , so GHC renames one of them to avoid name conflicts.

The type you need to provide runDangerous looks like this:

 runDangerous :: (forall e w. (Error e, Show e, Show w) => (Either ea, [w]) -> r) -> Dangerous a -> r 

which, given a function that takes a value of type (Either ea, [w]) for any variants of e and w , as long as they have the specified instances, and a Dangerous a , returns the result of this function. It's pretty hard to plunge!

The implementation is simple as

 runDangerous f (Dangerous m) = f $ runState (runErrorT m) [] 

what constitutes a trivial change to your version. If this works for you, great; but I doubt that an existential approach is the right way to achieve what you are trying to do.

Note that you will need {-# LANGUAGE RankNTypes #-} to express the type runDangerous . Alternatively, you can define another existential type of your result:

 data DangerousResult a = forall e w. (Error e, Show e, Show w) => DangerousResult (Either ea, [w]) runDangerous :: Dangerous a -> DangerousResult a runDangerous (Dangerous m) = DangerousResult $ runState (runErrorT m) [] 

and extract the result using case , but you have to be careful, or the GHC will start complaining that you allowed e or w escape - which is equivalent to trying to pass an insufficiently polymorphic function to another runDangerous form; that is, which requires more restrictions that e and w are outside of what the runDangerous type runDangerous .

Answer 2

Well, I think I realized that I was floundering after:

 data Failure = forall e. (Error e, Show e) => Failure e data Warning = forall w. (Show w) => Warning w class (Monad m) => Errorable m where warn :: (Show w) => w -> m () throw :: (Error e, Show e) => e -> m () instance Errorable Dangerous where warn w = Dangerous (Right (), [Warning w]) throw e = Dangerous (Left $ Failure e, []) 

( instance Monad Dangerous and data DangerousT too.)

This allows you to get the following code:

 foo :: Dangerous Int foo = do when (badThings) (warn $ BadThings with some context) when (worseThings) (throw $ BarError with other context) data FooWarning = BadThings FilePath Int String instance Show FooWarning where ... 

and then in the main module you can define custom instances of Show Failure , Error Failure and Show Warning and have a centralized way to format error messages, for example

 instance Show Warning where show (Warning s) = "WARNING: " ++ show s instance Show Failure where ... let (result, warnings) = runDangerous function in ... 

Which, in my opinion, is a pretty cool way to handle errors and warnings. I have a working module, something like this, now I'm leaving to polish it and possibly put it in a hack. Suggestions appreciated.