Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Existential types and monad transformers

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?

like image 696
So8res Avatar asked Dec 22 '11 18:12

So8res


2 Answers

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 Strings 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.

like image 60
ehird Avatar answered Sep 19 '22 22:09

ehird


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.

like image 40
So8res Avatar answered Sep 19 '22 22:09

So8res