There are also Alias Types [1] and Typed Regions [2], a merging of regions, alias types, and linear types, to overcome the disadvantages of each.
Sandro [1] http://www.cs.cornell.edu/talc/papers/alias.pdf [2] http://citeseer.ist.psu.edu/monnier04typed.html Jonathan S. Shapiro wrote: > 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 _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
