Kleisli Arrows of Outrageous Fortune

Kleisli Arrows of Outrageous Fortune

When we program to interact with a turbulent world, we are to some extent at its mercy. To achieve safety, we must ensure that programs act in accordance with what is known about the state of the world, as determined dynamically. Is there any hope to enforce safety policies for dynamic interaction by static typing? This paper answers with a cautious ‘yes’.

Monads provide a type discipline for effectful programming, mapping value types to computation types. If we index our types by data approximating the ‘state of the world’, we refine our values to witnesses for some condition of the world. Ordinary monads for indexed types give a discipline for effectful programming contingent on state, modelling the whims of fortune in way that Atkey’s indexed monads for ordinary types do not (Atkey, 2009). Arrows in the corresponding Kleisli category represent computations which a reach a given postcondition from a given precondition: their types are just specifications in a Hoare logic!

By way of an elementary introduction to this approach, I present the example of a monad for interacting with a file handle which is either ‘open’ or ‘closed’, constructed from a command interface specfied Hoare-style. An attempt to open a file results in a state which is statically unpredictable but dynamically detectable. Well typed programs behave accordingly in either case. Haskell’s dependent type system, as exposed by the Strathclyde Haskell Enhancement preprocessor, provides a suitable basis for this simple experiment.

I discovered this Googling around in an attempt to find some decent introductory material to Kleisli arrows. This isn't introductory, but it's a good resource. :-) The good introductory material I found was this.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

For posterity...

... the non-googlized version of that introductory material url is this.

Thanks!

I've updated both links so as not to redirect.

Conor McBride is known for

Conor McBride is known for his terrible puns, but the introductory section of this article is the most spectacular work of his I've seen to date. I hope that he has not given us too much of a good thing...

The corresponding video

from the Eugene Summer School: http://www.cs.uoregon.edu/research/summerschool/summer10/video/OPLSS10-22-4.mp4

Swierstra's Hoare State Monad?

How does this compare to Swierstra's work on the Hoare State Monad [paper] [slides: 1 2]? I've only skimmed McBride's paper so far, but it looks fairly similar. Swierstra's work uses Coq instead of preprocessed Haskell and does not address IO expressly, but the connection between the IO and State monads is well-known: ISTM seems that his approach should go through.

Hoare Logic and Monads

Of course there are similarities between Wouter's work and mine, in that both connect Hoare-style reasoning and monads. There are also significant differences in approach, as I hope might become evident after more than a skim.

In his paper, Wouter works in the fine old verificationist tradition, attaching logical superstructure to the state monad as we know it, using Coq's Program tactic, one of Matthieu Sozeau's excellent contributions, as a verification condition generator. Your regular

State a = s -> a * s
being a Monad in sets-and-functions, gets annotated with conditions
Pre : s -> Prop
Post : s -> a -> s -> Prop
Note that dependent types are used only to form propositions, and only in the reasoning layer. An ordinary state monad program is written with an annotated type, proof obligations are generated, and the difficult ones are discharged with human assistance. It's textbook stuff, with a lovely example.

I work in Haskell, with no logical superstructure. Rather, I use dependent datatypes to create logical infrastructure for the program operations themselves. In particular, I index sets by the 'state of the world': the kind {s} -> * contains type-formers which express properties of a state in type s, but at the same time carry significant dynamic data. This 'state' is not a piece of dynamic store, mutated only by the monadic computation itself; rather it's a static model of possible knowledge about the world, potentially prone to external interference. I use these state-indexed types as data-bearing pre- and post-conditions. Your monadic functions have types like

forall s. p {s} -> m q {s}

where m is a monad on the category of s-indexed types with index-respecting functions, representing some notion of reachability. The type says 'from any state where p holds, you can reach a state where q holds'. In effect, the very definition of a monad for an indexed type gives you a kind of Hoare logic. This property is not specific to monads for mutable store: it's an observation about monads for 'predicates', period.

Meanwhile, I chose an example based on IO exactly because IO does not really behave as predictably as state transforming functions for RealWorld. Indeed, the point is to express the static unpredictability of operations like 'open file': we cannot guarantee statically that they succeed, but we can guarantee statically that we will find out dynamically whether they succeed, and that there will be one bit of data which is known to bear that meaning.

Of course, in a proof assistant like Coq, one could take a 'logical superstructure' view of the same phenomena. My point is that one can achieve at least some improvements of basic hygiene without recourse to a proof assistant, just by baking a little more structure into the program types themselves. Moreover, the 'logical infrastructure' approach is accessible, even with the limited dependent types of Haskell.

Taking a broader view, there is no conflict between logical infrastructure and superstructure. A good programming and proof environment will need to give effective support to both, and the flexibility to move the slider between them to the sweet spot.