After a discussion with a colleague, I am going back to look at the Monads idea again. I don't think that putting mutability into BitC was a mistake. General-purpose programmers aren't going to adopt monads any time soon, and there are many kinds of static program analysis that are possible and useful in a system that has state.
That said, there are *some* kinds of analysis for which state makes things very difficult. We have claimed in the past that the monads idiom makes authoring and maintaining things like kernels unreasonably difficult. The House project, to my mind, was not a serious counterexample to this statement. The seL4 project, however, is a counterexample that needs to be viewed seriously. I have also been reading John Hughes' "Functional Pearls" note on the interactions between monads and global variables, and I am just starting his later work on Arrows. What I want to do in my next few notes is investigate two options for getting from where we are (static checking feasible) to where we need to be (software verification feasible). At present, I see three ways to go: monads, state threading, and linear types. For those who may not know, some explanations: State threading is an idea from ACL2 (probably from previous sources -- if anybody knows, please correct me). The idea is to impose the following restriction on the language: At any point where a variable is updated (assigned), no outstanding reference to that variable remains live. When this restriction holds, we can (conceptually -- the goal is to avoid this in practice) rewrite the program so that this assignment is not an assignment, but is rather a binding to a newly-introduced program variable. This allows us to reason about the program as if it were purely functional. The nice thing about the scheme is that *because* the old value is not live, the location storing the old value can be reused by the implementation, and the code emitted is conventionally stateful code. In ACL2, this idea is captured in the notion of a "State Object" (STOBJ). The state object contains all of the system state, and is passed around as an extra argument to all stateful procedures. These procedures are obligated to honor certain syntactic restrictions. The effect of these syntactic restrictions is to ensure the "dead after update" restriction. The ACL2 technique does not address local variables, but it could be. In the end, ACL2 converts the program into a "state passing style" (by analogy to continuation passing style). Having done so, it then notices "holy crud, we're always passing the same state pointer, so we can make the state pointer a global and remove the extra argument". Monads are a variant on this idea. Instead of enforcing the restriction through syntactic rules, a monad enforces it through the type system (not surprising: Haskell is centrally organized around types). The monad approach is both stronger and weaker than ACL2 state threading. Stronger because it allows local state. Weaker because it does not deal well with composite objects and because it tends to propagate the Monad types rather further than it has to. Linear Types basically ensure that there is only one live reference to an object at a time. This idea has significant value, but in my opinion it is too restrictive for our purposes as general-purpose programmers. shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
