Existential types and monad transformers
-
27-03-2021 - |
Question
Context: I'm trying to produce an error monad that also keeps track of 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 resulting in (Either e a, [w])
where e
is a showable error and w
is showable.
The problem is, I can't seem to actually run the thing, mostly because I don't understand existential types all that well. Observe:
runDangerous :: forall a e w. (Error e, Show e, Show w) =>
Dangerous a -> (Either e a, [w])
runDangerous (Dangerous f) = runState (runErrorT f) []
This doesn't 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 a e 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 e a, [w])
I'm lost. What's w1? Why can't we deduce that it's ~ w
?
Solution
An existential is probably not what you want here; there is no way to "observe" the actual types bound to e
or w
in a Dangerous a
value, so you're 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 might as well just be a String
(ignoring precedence to simplify things), and the only thing you know about e
is that you can turn it into a String
, you can turn String
s into it, and you have a distinguished value of it (noMsg
). There is no way to assert or check that these types are the same as any other, so once you put them into a Dangerous
, there's no way to recover any special structure those types may have.
What the error message is saying is that, essentially, your type for runDangerous
claims that you can turn a Dangerous
into an (Either e a, [w])
for any e
and w
that have the relevant instances. This clearly isn't true: you can only turn a Dangerous
into that type for one choice of e
and w
: the one it was created with. The w1
is just because your Dangerous
type is defined with a type variable w
, and so is runDangerous
, so GHC renames one of them to avoid name clashes.
The type you need to give runDangerous
looks like this:
runDangerous
:: (forall e w. (Error e, Show e, Show w) => (Either e a, [w]) -> r)
-> Dangerous a -> r
which, given a function which will accept a value of type (Either e a, [w])
for any choices of e
and w
so long as they have the instances given, and a Dangerous a
, produces that function's result. This is quite hard to get your head around!
The implementation is as simple as
runDangerous f (Dangerous m) = f $ runState (runErrorT m) []
which is a trivial change to your version. If this works for you, great; but I doubt that an existential is the right way to achieve whatever you're trying to do.
Note that you'll need {-# LANGUAGE RankNTypes #-}
to express the type of runDangerous
. Alternatively, you can define another existential for your result type:
data DangerousResult a = forall e w. (Error e, Show e, Show w) =>
DangerousResult (Either e a, [w])
runDangerous :: Dangerous a -> DangerousResult a
runDangerous (Dangerous m) = DangerousResult $ runState (runErrorT m) []
and extract the result with case
, but you'll have to be careful, or GHC will start complaining that you've let e
or w
escape — which is the equivalent of trying to pass an insufficiently polymorphic function to the other form of runDangerous
; i.e. one that requires more constraints on what e
and w
are beyond what the type of runDangerous
guarantees.
OTHER TIPS
Ok, I think I figured out what 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
help too.)
This allows you to have 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 your main module you may define custom instances of Show Failure
, Error Failure
, and Show Warning
and have a centralized way to format your 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've got a working module that's something like this, now I'm off to polish it up and maybe put it on hackage. Suggestions appreciated.