FP Lunch

After I failed to typeset some fancy lhs2tex for the blog (it says the latex is too complicated) here is just a short summary what I talked about last Friday.

In his very readable tutorial Tackling the awkward squad Simon explains and discusses Haskell’s IO features which are encapsulated in the IO monad. He uses a simple process calculus, inspired by he pi calculus, to give an operational semantics to Haskell’s IO. I have been looking at an alternative: defining the meaning of IO within Haskell itself. This has the advantage that we already know Haskell and how to reason about Haskell programs. I also hope that following this line we can add IO to Epigram.

Following Simon’s example I introduce IO in several steps:

• First I introduce stream IO. Interestingly the type myIO is a variant of the food processor we have seen recently, introduced by Hank and Conor. See myIOStr.hs
• Next we turn our attention to IORefs, see myIORef.hs. Note that I only do IORef Int, doing it more polymorphically involves some standard generic programming technology, not relevant here. How do we combine IORefs and streams? It is the coproduct of the two monads (see Neil’s paper), which in this case has a particularly simple form.
• Finally, we implement Concurrent Haskell with forkIO and MVars, see myIOMVar.hs. Here runIO gets an additional parameter a scheduler represented as a stream of Booleans. Also the return type of runIO has to take account of the possibility that the process becomes deadlocked.

The scheduler can also be used to introduce the simulation preorder, given p,q::MyIO a we say that p < q (p can simulate q), iff there is a function f::[Bool] -> [Bool] s.t. for any scheduler s we have that runIO s p = runIO (f s) q. The symmetric closure of < is called bisimulation and is a useful congruence when reasoning about IO, i.e. we consider IO as the quotient of MyIO wrt to bisimulation.

Yesterday there were a few talks on Datatype Generic Programming. Bruno Oliveira talked about Conor’s applicative functors. Ralf Laemmel showed how Google’s MapReduce Programming Model can be captured succinctly in Haskell. I gave an idea of how the two could be related.

One of the nice properties of applicative functors is that they are closed under composition. As and are applicative, so is:

Using this dictionary, both Ralf’s interpretation of Google’s map and reduce correspond to the ‘apply’ of the applicative functor Dict k. Unfortunately, the correspondence wasn’t as nice as you might expect. I needed a few minor tweaks here and there to get things to fit together. The intermediate grouping operation can also be written using the traversal functions in Conor’s library.

It was clear that there is still some work to be done. Paraphrasing Graham, “If you find that the theory doesn’t match the implementation, you should probably rethink the implementation”.

The zipper is a useful data structure for navigating around tree-like structures in an efficient manner. I gave an introduction to the zipper, by starting with a simple type of trees

and then showing how to arrive at the following definitions:



Conor then explained the connection with differentiation, and also showed how to use the zipper to write an efficienct function that returns the mirror image of a tree. The lunch concluded with Nicolas Oury, who is visiting from France, explaining some of his work on simplifying the use of pattern matching in the Coq system.

The upgrade to WordPress 2 is (almost) complete on this and our sister sites. Hopefully you’ll find it a bit easier to use, and if not at least the admin is prettier. Most things remain the same outwardly. Lawks.