Monadic Regions

• jfp06.pdf (with Greg Morrisett; To appear in the Journal of Functional Programming)

  Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, and proving their soundness is non-trivial. This paper shows that the complication is in principle unnecessary. In particular, we show that plain old parametric polymorphism, as found in Haskell, is all that is needed. We substantiate this claim by giving a type- and meaning-preserving translation from a variation of the region calculus of Tofte and Talpin to a monadic variant of System F with region primitives whose types and operations are inspired by (and generalize) the ST monad of Launchbury and Peyton Jones.

• icfp04.pdf (with Greg Morrisett; Appeared at ICFP'04; 20040920-ICFP04.ppt)

  Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, so proving their soundness is non-trivial. This paper shows that the complication is in principle unnecessary. In particular, we show that plain old parametric polymorphism, as found in Haskell, is all that is needed. We substantiate this claim by giving a type- and meaning-preserving translation from a region-based language based on core Cyclone to a monadic variant of System F with region primitives whose types and operations are inspired by (and generalize) the ST monad of Launchbury and Peyton Jones.

• techrpt.pdf (Cornell University Technical Report; TR2004-1936)

  Drawing together two lines of research (that done in type-safe region-based memory management and that done in monadic encapsuation of effects), we give a type-preserving translation from a variation of the region calculus of Tofte and Talpin into an extension of System F augmented with monadic types and operations. Our source language is a novel region calculus, dubbed the Single Effect Calculus, in which sets of effects are specified by a single region representing an upper bound on the set. Our target language is F^RGN, which provides an encapsulation operator whose parametric type ensures that regions (and values allocated therein) are neither accessible nor visible outside the appropriate scope.

• 20040224-NEPLS.ppt (Presentation at the New England Programming Languages and Systems Symposium Series (NEPLS))

  The region calculus, first introduced by Tofte and Talpin, has a fairly complicated type-and-effects system that is used to ensure that pointers into deallocated storage are never dereferenced. In a separate line of research, Launchbury and Peyton-Jones introduced monads as a mechanism by which imperative (and otherwise "effectful") constructs can be safely integrated into pure functional languages. We demonstrate that the type system of the region calculus can be encoded in the polymorphic lambda calculus augmented with monadic types and operations. The encoding is based upon a generalization of the ST monad and likewise presents an encapsulation operator whose parametric type ensures that regions (and values allocated therin) are neither accessible nor visible outside the appropriate scope.

• space04.pdf (Appeared at SPACE'04; 20040112-SPACE04.ppt)

  Drawing together two lines of research (that done in type-safe region-based memory management and that done in monadic encapsuation of effects), we give a type-preserving translation from a variation of the region calculus of Tofte and Talpin into an extension of System F augmented with monadic types and operations. Our source language is a novel region calculus, dubbed the Single Effect Calculus, in which sets of effects are specified by a single region representing an upper bound on the set. Our target language is F^RGN, which provides an encapsulation operator whose parametric type ensures that regions (and values allocated therein) are neither accessible nor visible outside the appropriate scope.