Operational semantics for monads

While randomly browsing around on Planet Haskell I’ve found a post on Heinrich Apfelmus‘ blog about something called “operational semantics” for monads. Found it very iluminating. Basically it’s a form to implement monads focusing not on defining the bind and return operators, but on what the monad is really supposed to do. It’s a view where a monad define a Domain Specific Language, that must be interpreted in order to cause it’s effects. It seems to me it’s exactly what is implemented in the monadprompt (Control.Monad.Prompt) package, although I’m not sure.

> {-# LANGUAGE GADTs #-}
> import Control.Monad
> import Data.Map (Map, fromList, unionWith)

The definition of a monad on this approach starts with a common interface given by the following data type and a singleton function:

> data Program m a where
>     Then   :: m a -> (a -> Program m b) -> Program m b
>     Return :: a -> Program m a
>
> singleton :: m a -> Program m a
> singleton i = i `Then` Return

Note that the types of the data constructors Then and Return are very similar (but not equal…) to the types of the monadic operations (>>=) and return. This identification of class functions with data constructors is recurring throughout this post. This data type is instanciated as a traditional monad as follows:

>instance Monad (Program m) where
>    return = Return
>    (Return a)    >>= f  = f a
>    (i `Then` is) >>= f  = i `Then` (\ x -> is x >>= f)

This is all we need! As an example let’s describe the implementation of the State Monad within this approach. This is exactly the first example given by Apfelmus on his post, disguised as a stack machine.

The operational approach to monads begins with recognizing what operations you want your monad to perform. A State Monad have a state, a return value and two function: one that allows us to retrieve the state as the return value, and one that allows us to insert a new state. Let’s represent this in the following GADT:

> data StateOp st retVal where
>     Get :: StateOp st st  -- retrieve current state as a returned value
>     Put :: st -> StateOp st ()  -- insert a new state

This are the operations needed on the State Monad, but the monad itself is a sequence of compositions of such operations:

> type State st retVal = Program (StateOp st) retVal

Note that the type synonim State st is a monad already and satisfy all the monad laws by construction. We don’t need to worry about implementing return and (>>=) correctly: they are already defined.

So far, so good but… how do we use this monad in practice? This types define a kind of Domain Specific Language: we have operations represented by Get and Put and we can compose them in little programs by using Then and Return. Now we need to write an interpreter for this language. I find this is greatly simplified if you notice that the construct

do x <- singleton foo
   bar x

can be translated as foo `Then` bar in this context. Thus, to define how you’ll interpret the later, just think what’s the effect you want to have when you write the former.

Our interpreter will take a State st retVal and a state st as input and return a pair: the next state and the returned value (st, retVal):

> interpret :: State st retVal -> st -> (st, retVal)

First of all, how should we interpret the program Return val ? This program just takes any state input and return it unaltered, with val as it’s returned value:

> interpret (Return val) st = (st, val)

The next step is to interpret the program foo `Then` bar. Looking at the type of things always helps: Then, in this context, have type StateOp st a -> (a -> State st b) -> State st b. So, in the expression foo `Then` bar, foo is of type StateOp st a, that is, it’s a stateful computation with state of type st and returned value of type a. The rest of the expression, bar, is of type a -> State st b, that is, it expects to receive something of the type of the returned value of foo and return the next computation to be executed. We have two options for foo: Get and Put x.

When executing Get `Then` bar, we want this program to return the current state as the returned value. But we also want it to call the execution of bar val, the rest of the code. And if val is the value returned by the last computation, Get, it must be the current state:

> interpret (Get `Then` bar) st = interpret (bar st) st

The program Put x `Then` bar is suposed to just insert x as the new state and call bar val. But if you look at the type of Put x, it’s returned value is empty: (). So we must call bar (). The current state is then discarded and substituted by x.

> interpret (Put x `Then` bar) _  = interpret (bar ()) x

We have our interpreter (which, you guessed right, is just the function runState from Control.Monad.State) and now it’s time to write programs in this language. Let’s then define some helper functions:

> get :: State st st
> get = singleton Get

> put :: st -> State st ()
> put = singleton . Put

and write some code to be interpreted:

> example :: Num a => State a a
> example = do x <- get
>              put (x + 1)
>              return x
>
> test1 = interpret example 0
> test2 = interpret (replicateM 10 example) 0

This can be runned in ghci to give exactly what you would expect from the state monad:

*Main> test1
(1,0)

*Main> test2
(10,[0,1,2,3,4,5,6,7,8,9])

The approach seems very convenient from the point of view of developing applications, as it’s focused on what are actions the code must implement and how the code should be executed. But it seems to me that the focus on the operations the monad will implement is also very convenient to think about mathematical structures. To give an example, I’d like to implement a monad for Vector Spaces, in the spirit of Dan Piponi (Sigfpe)’s ideas here, here and here.

A vector space \mathcal{V_F} is a set of elements \mathbf{x}\in\mathcal{V_F} that can be summed (\mathbf{x} + \mathbf{y} \in\mathcal{V_F} if \mathbf{x},\mathbf{y} \in \mathcal{V_F}) and multiplied elements of a field (\alpha\mathbf{x} if \alpha\in \mathcal{F} and \mathbf{x}\in\mathcal{V_F}). If we want this to be implemented as a monad then, we should, in analogy with what we did for the State Monad, write a GADT with data constructors that implement the sum and product by a scalar:

> data VectorOp field label where

>     Sum :: Vector field label
>         -> Vector field label
>         -> VectorOp field label

>     Mul :: field
>         -> Vector field label
>         -> VectorOp field label

> type Vector field label = Program (VectorOp field) label

and then we must implement a interpreter:

> runVector :: (Num field, Ord label) => Vector field label 
>                                     -> Map label field
> runVector (Return a) = fromList [(a, 1)]
> runVector (Sum u v `Then` foo) = let uVec = (runVector (u >>= foo))
>                                      vVec = (runVector (v >>= foo))
>                                  in unionWith (+) uVec vVec
> runVector (Mul x u `Then` foo) = fmap (x*) (runVector (u >>= foo))

The interpreter runVector takes a vector and returns it’s representation as a Map. As an example, we could do the following:

> infixr 3 <*>
> infixr 2 <+> 

> u <+> v = singleton $ Sum u v
> x <*> u = singleton $ Mul x u 

> data Base = X | Y | Z deriving(Ord, Eq, Show)

> x, y, z :: Vector Double Base
> x = return X
> y = return Y
> z = return Z

> reflectXY :: Vector Double Base -> Vector Double Base
> reflectXY vecU = do cp <- vecU
>                     return (transf cp)
>                         where transf X = Y
>                               transf Y = X
>                               transf Z = Z

and test this on ghci:

*Main> runVector $ x <+> y
fromList [(X,1.0),(Y,1.0)]

*Main> runVector $ reflectXY $ x <+> z
fromList [(Y,1.0),(Z,1.0)]

As Dan Piponi points out in his talk, any function acting on the base f :: Base -> Base is lifted to a linear map on the vector space Space field Base by doing:

> linearTrans f u = do vec <- u
>                      return (f vec)

More on this later. :)

HTML generated by org-mode 6.34c in emacs 23

About these ads
Post a comment or leave a trackback: Trackback URL.

Comments

  • Anonymous  On August 27, 2010 at 08:24

    Nice post. I found two little bugs, though:
    1) Data.Map clashed with prelude, so you would want to say something like
    > import Data.Map(Map, fromList, unionWith)

    2) Your types don’t match up. I’m pretty sure you meant to write
    > Then :: m a -> (a -> Program m b) -> Program m b
    in your “Program” data type

  • wren ng thornton  On August 27, 2010 at 18:26

    For vector spaces in general you’ll need to distinguish multiplication of vectors ( :: V F -> V F -> V F) vs scaling vectors (.*> :: F -> V F -> V F or F -> V F). Thus, you should reflect this asymmetry in the names of the multiplicative operations. Also, you need to define an identity element for vector addition; this is in Dan’s Vector, so you’ll probably want it in your VectorOp as well. Also also, Num isn’t a field, it’s a ring; you want Fractional for fields.
    :)

    • wren ng thornton  On August 27, 2010 at 18:28

      Hmm. It seems my type signatures got eaten:

      <*> :: V F -> V F -> V F
      .*> :: F -> V F -> V F
      <*. :: V F -> F -> V F

  • イルビゾンテ 店舗  On July 30, 2013 at 13:27

    Hola! I’ve been reading your web site for a while now and finally got the courage to go ahead and give you a shout out from Houston Tx! Just wanted to say keep up the good job!

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: