Tuesday, September 30, 2014

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.

Labels: ,

8 Comments:

At October 01, 2014 9:05 pm , Anonymous Anonymous said...

newtype DijkstraT s m a = DijkstraT { runDijkstraT :: forall r. ((a, s) -> m r) -> s -> m r }

toStateT :: (Monad m) => DijkstraT s m a -> StateT s m a
toStateT m = StateT (runDijkstraT m return)

fromStateT :: (Monad m) => StateT s m a -> DijkstraT s m a
fromStateT m = DijkstraT (runStateT m >=>)

 
At October 01, 2014 11:26 pm , Blogger James Cheney said...

Yes, that's roughly what I thought too. Though I'm not sure I have a good explanation concerning why the "m" goes there, other than that's what seems to make possible to define operations that look like they form a monad. Still need to check...

Also, clearly, using (a,s) rather than (s,a) makes things a little slicker (and makes it really obvious that the map from State to Dijkstra is just a CPS conversion!)

 
At October 01, 2014 11:37 pm , Anonymous Anonymous said...

http://pastebin.com/f2bdx9DE

 
At October 02, 2014 9:41 am , Anonymous Anonymous said...

By the way, it's a left Kan extension (not a CPS transform.)

newtype Lan cat a b = Lan { runLan :: forall r. cat b r -> cat a r }

_Lan :: (Category cat) => Iso' (cat a b) (Lan cat a b)
_Lan = iso (\ab -> Lan (. ab)) (\m -> runLan m id)

(where the "iso" function and "Iso'" type are imported from the lens package.)

 
At October 02, 2014 10:22 am , Blogger James Cheney said...

Ah, I stand corrected. That explains why DijkstraT should be what it is.

 
At October 02, 2014 11:01 am , Blogger James Cheney said...

Actually, are you sure about that? I'm definitely not an expert on Kan extensions, but the type you give for Lan above is not the same as in Edward Kmett's Kan extensions library:

https://github.com/ekmett/kan-extensions/blob/master/src/Data/Functor/Kan/Lan.hs

However, I guess you are referring to a more general notion that instantiates to the above.

 
At October 02, 2014 1:01 pm , Anonymous Anonymous said...

The definition in the kan-extensions package is for instances of the "Functor" class.

We are working with instances of the "Profunctor" class.

Try the profunctors package (also by Edward Kmett).

 
At October 02, 2014 1:37 pm , Blogger James Cheney said...

Thanks for the clarification!

 

Post a Comment

Subscribe to Post Comments [Atom]

Links to this post:

Create a Link

<< Home