Dijkstra monads

Dijkstra monads in monadic computation
Bart Jacobs
CMCS 2014

This paper discusses a monad for predicate transformers (dubbed the Dijkstra monad in an earlier paper by Swamy et al. that is now also on my reading list). This post is an attempt to express a very, very small part of the ideas of the paper in Haskell, to try to make some sense of them.


Recall the standard State monad which we might define in Haskell as follows:

data State s a = State {runState :: s -> (a,s)}

instance Monad (State s) where
  return a = State (\s -> (a,s))
  m >>= f = State (\s -> let (a,s') = runState m s in
                         runState (f a) s')

The "plain" Dijkstra monad as discussed by Swamy et al. (according to Jacobs) is a predicate transformer.  I'll write it as follows:

data Dijkstra s a = 
  Dijkstra {wp :: forall omega. 
                  ((s,a) -> omega) -> 
                  (s -> omega)}

I'm quantifying over the "return" type of the observation - it could eventually be instantiated to Bool or any other type.  We can equip this with monad operations as follows:

instance Monad (Dijkstra s) where
  return a = Dijkstra (\f s -> f (s,a))
  m >>= f = Dijkstra (\g -> wp m (\(s,a) -> 
                            wp (f a) g s))
             
The return operation simply runs the predicate with the given return value and same state.  The bind operation computes the weakest precondition for a sequence of operations by computing the weakest precondition of the first operation, starting from the postcondition we get by computing the weakest precondition of the second operation, given parameter a and the final postcondition g.

Jacobs observes hat there is a monad morphism from State s to Dijkstra s, expressible in Haskell as follows:

h :: State s a -> Dijkstra s a
h m = Dijkstra (\f s -> 
         let (a,s') = runState m s in 
         f(s',a))

That is, given a stateful computation, we define a predicate transformer that runs the computation and observes the results.

Conversely, we can map Dijkstra s to State s.

k :: Dijkstra s a -> State s a
k m = State (\s -> wp m (\(s',a) -> (a,s')) s)

Given a predicate transformer, we define a stateful computation by using the weakest precondition of the "postcondition" $\lambda (s',a). (a,s')$.  This gives us a function $s \to (a,s)$ which we can apply to the initial state $s$ to get the result state $(a,s')$.  

Note that since we quantify over all possible observations of the state in the type of wp, we can pass in a "predicate" that simply returns the final return value and state, as required for State (this would not have been possible if the Dijkstra monad return type had been hard-wired to Bool!)  In Jacobs' paper, the Dijkstra monad maps "predicates" over $S \times A$ to predicates over $S$, and if we naively interpret predicate over X as X -> Bool we wouldn't have been able to define k.

Jacobs' main argument seems to be that the Dijkstra monad is a general formalism that could be applicable in a range of settings, not just the state monad and weakest precondition setting; he gives the outlines of examples including nondeterminism, probabilistic, and quantum computation.

In particular, we could consider predicate transformers for computations that have some observable state as well as effects in some other monad.  Jacobs discusses a more general setting than the one I describe above, where we can map monads of the form StateT s m to a variant of the Dijkstra monad, but one that doesn't explicitly refer to the underlying monad m; instead, the operations live in a larger semantic space that doesn't say much about the invariants on the maps.

I have some (probably at most half-baked) thoughts about how to adapt the above story to this setting to define a "Dijkstra monad transformer" that relates to StateT as Dijkstra above relates to State.  This may be explored in a future post.