Regions offer an attractive alternative to both manual allocation of resources and garbage collection. Unlike the latter, region-based resource management makes resource disposal and finalization predictable. We can precisely identify the program points where allocated resources are freed and finalization actions are run. Like other automatic resource managements schemes, regions statically assure us that no resource is used after it is disposed of, no resource is freed twice, and all resources are eventually deallocated.
Monadic Regions can manage resources other than memory, as explained by Brandon Moore: ``I'm assuming you understand how the type on
runST and the
STRef operations ensure that, even though you can smuggle out an
STRef in the result from
runST , you will never be able to use it again. The idea was to do the equivalent thing with databases: use fancy types to ensure that handle can only be used inside to origination
withCursor or whatever, and the bracketing function can release the resource on the way out, without worrying about it being used again.'' In a follow-up, Benjamin Franksen concurred: ``I think this is an extremely good idea. I have been very frustrated with finalizers because of their limitations (can't rely on them being called at all), so have (reluctantly) been using the unsafe bracket version. Making it safe via a type system trick is really the way to go.''
The paper by Fluet and Morrisett describes monadic regions, their calculus, and the type- and meaning-preserving translation to a variant of System F. The authors mention as future work providing a
RGN monad for Haskell programmers. We show exactly this monad in Section Heavy-weight implementation of region calculus , which however relies on heavy type-class trickery. A simpler, and still complete, solution exists, especially suitable for IO regions and ensuring the validity of file handles: Lightweight monadic regions .
With some limitations, File and Database IO regions can be implemented already in Haskell98 with a common extension for rank-2 types (existentials). This technique has indeed been used in Takusen, to provide precisely the assurances that Brandon Moore wanted. One may hope this assured approach to File IO would be more widely used.
Brandon Moore, Benjamin Franksen: Db and STRef. Messages posted on the Haskell-Cafe mailing list, Jan 15-16 2006.
Takusen: a DBMS access library built around a left-fold enumerator
withFileblock. Many handles can be open simultaneously; the type system enforces the proper nesting of their regions. The technique has no run-time overhead and induces no run-time errors. Unlike the other implementation of monadic regions, only the basic extension (rank-2 types, aka existentials) is needed. No new type classes are introduced. The technique underlies safe database interfaces of Takusen.
The simplicity of the implementation comes with a limitation: although an inner region can use resources allocated in outer regions, an inner region cannot allocate such outer-region resources. That is, an inner region can read from a file handle opened in an outer region, but cannot itself create such file handles. An inner region therefore is not allowed to return any file handles. We also cannot store file handles in reference cells. These limitations have been overcome in another, also simple implementation of IO regions. The latter does require type classes, however.
test0 = withFile "/etc/motd" (const $ return True) reader q = do c1 <- qGetChar q c2 <- qGetChar q return [c1,c2] test1 = withFile "/etc/motd" reader test1r = runIOM test1 >>= printAbove is the first example of the region-based file IO. Instead of handles, we have
Qs -- marked handles. They are created by the function
withFileand used similarly to regular handles. A special
IOMmonad is a newtype away from the regular IO. The phantom type parameter of the IOM monad, like the
sparameter of the
STmonad, marks the region.
*IORegions98Test> :t reader reader :: Q mark -> IOM mark [Char]According to its inferred type, the
readertakes a marked handle and yields an IO computation with the same mark. If we try to leak the handle, we get a type error:
test2 = runIOM (withFile "/etc/motd" (\q -> return q)) Inferred type is less polymorphic than expected Quantified type variable `mark' escapes In the first argument of `runIOM', namely `(withFile "/etc/motd" (\ q -> return q))'We certainly can perform an
IOMcomputation and return its result:
test3below works. An attempt to leak
withFilemay seem successful:
test4'is accepted by the type checker. It cannot be run however, see
test4'r; the error message betrays the implementation, which relies on the fact that only monomorphic types may be instances of
Typeableand so the required
instance Typeable markcannot be created. The source code contains a number of tests, many of which have been suggested by Brandon Moore.
test3 = withFile "/etc/motd" (\q -> (qGetChar q)) -- OK test4' () = join $ withFile "/etc/motd" (\q -> return (qGetChar q)) test4'r = runIOM (test4' ()) No instance for (Typeable mark) arising from use of `test4''
We may open several file handles. Their regions may nest, the handles of the parent regions can be used in any descendant region:
-- Now we add the type signature, just to show that we can do that reader2 :: Q mark -> Q mark -> IOM mark String reader2 q1 q2 = do c1 <- qGetChar q1 c2 <- qGetChar q2 return [c1,c2] test5 = withFile "/etc/motd" (\q1 -> withFile "/etc/motd" (\q2 -> reader2 q1 q2)) test5r = runIOM test5 >>= print
IORegions98E with a limited export is the kernel of trust of our implementation. The module defines
newtype IOM marks a = IOM (IO a) -- data constructor is not exported newtype Q mark = Q Handle -- data constructor is not exported withFile :: Typeable a => FilePath -> (Q mark -> IOM mark a) -> IOM mark a qGetChar :: Q mark -> IOM mark Char runIOM :: (forall mark. IOM mark a) -> IO aWe wish to assure that the handle
Qnever escapes from its region. The handle can escape if it is incorporated into the result of
withFile. The type of that result must then mention the type of
Q. The only computation that eliminates the type
qGetChar, yet the latter introduces the type
IOM. If we make sure that neither
Qmay appear in the type of the values produced by
withFile, our goal is achieved. Constraining the type of the result of
withFileto be an instance of
Typeabledoes the trick: since
IOM mark aand
Q markmust be fully polymorphic with respect to
markto be usable for
runIOM, these types cannot be instances of
Typeable, because of the polymorphism. The handle may also escape its region if it is stored in a reference cell. The module
IORegions98Edoes not however provide any
IOMcomputation for reference cells. And if it had, the type of the storable values would have been similarly constrained to be
Typeable. Since we are assured that no computation with the marked handle can occur after we leave
withFile, the implementation of
withFilemay safely close the handle at that point. The module
IORegions98Eshould not normally be touched by the end user. Still, there may be a need for computations with
qGetChar. Since the functions within the module have unrestricted access to unmarked handles, special care is required when adding more definitions to the trusted kernel. The programmer must not leak unmarked handles and must not close handles. To force closing a handle, one should throw an exception.
extensive test code, including all the tests by Brandon Moore.
Because file handles and similar resources are scarce, we want to not just assure their safe use but further deallocate them soon after they are no longer needed. Relying on Fluet and Morrisett's calculus of nested regions, we contribute a novel, improved, and extended implementation of the calculus in Haskell, with file handles as resources.
Our library supports region polymorphism and implicit region subtyping, along with higher-order functions, mutable state, recursion, and run-time exceptions. A program may allocate arbitrarily many resources and dispose of them in any order, not necessarily LIFO. Region annotations are part of an expression's inferred type. Our new Haskell encoding of monadic regions as monad transformers needs no witness terms. It assures timely deallocation even when resources have markedly different lifetimes and the identity of the longest-living resource is determined only dynamically.
For contrast, we also implement a Haskell library for manual resource management, where deallocation is explicit and safety is assured by a form of linear types. We implement the linear typing in Haskell with the help of phantom types and a parameterized monad to statically track the type-state of resources.
Joint work with Chung-chieh Shan.
Chung-chieh Shan. Slides of the talk at the Haskell Symposium, September 25, 2008. Victoria, Canada.
< http://www.cs.rutgers.edu/~ccshan/capability/region-io-talk.pdf >
Safe file IO in a single region: the library and test code for Section 2 of the paper, the warm-up. We satisfy all requirements but the timeliness: all open handles remain open until the whole single region is finished; the longest-living safe handle prevents closing of all the others. This code essentially implements the
ST s monad, only with safe handles instead of references. We introduce naive regions, which cannot share handles. We improve upon them later.
Nested regions using explicit witness terms: the library and test code for Section 3 of the paper. This is the implementation of FRGN by Fluet and Morrisett (ICFP04), adjusted for the application domain: IO and Handles rather than memory allocation and pointers. The implementation relies on term-level witnesses of region inclusion (subtyping).
Nested regions as monad transformers: the library and test code for Sections 4 and 5 of the paper. This is the final solution: lightweight monadic regions with type-level--only enforcement of the region discipline.
Alternative: tracking type-state in a parameterized monad, Section 6 of the paper. The more general solution in
multi-handle-io.hs supports recursive computations in the parameterized monad. Surprisingly, that requires regions.
RGNmonad for Haskell programmers. The code below does exactly that.
The code gives the first example of the total type comparison predicate, which can handle even non-ground types and quantified type variables.
RGNmonad and the tests
Philippa Cowderoy: Monad.Reader IssueFour 2005-06-27. The ImpureThoughts column. Section ``Policing the State''
The question of statically tracking locks whose acquisition and release depends on a statically unknown value was posed by Naoki Kobayashi. The present code was written as a response. For clarity, the code uses two locks and a toy version of HList. The introductory locking program looks as follows:
tlock2 = do l <- lget lock lock1 x <- return (read l) lput (show (x+1))We read a line from the standard input, lock
lock1, parse the line and print something. The inferred type
LIO q (Insert (Lock N1) q) ()tells that
tlock2finishes with the lock
N1still held. To be precise, the state of locks at the end of
tlock2differs from the initial state
qby the addition of
Lock N1. Here
LIO p q ais a parameterized monad, carrying the initial
pand the final
qtype states, along with the result type
aof the computation. The
RebindableSyntaxextension of GHC lets us use the convenient
do-notation. Attempting to run the computation,
runLIO tlock2, gives a type error: the type checker complaints that
Lock N1is not released.
The second example shows the conditional lock manipulations. Depending on user input, one of two locks is acquired; one of two locks is later released. We statically ensure that the acquired lock is released -- although we cannot statically tell which lock that will be.
rtcl3 = runLIO $ do l <- lget brand_bool ((read l) > (0::Int)) (\b bnot -> do clock b lock1 clock bnot lock2 lput l cunlock b lock1 cunlock bnot lock2)We read a number and check if it is is positive. We acquire
lock1if it is, and
lock2if it is not. The locks are released on the opposite condition,
b. The function
brand_boolproduces the unique set of two complementary `keys'. A lock locked with one key must be unlocked with the other. We may lock with both keys, making the lock held unconditionally. When we run the code, we see that depending on the input value, either lock
N1is acquired and released, or lock
N2. The lock safety holds in either case. If we forget a
cunlockstatement, predicate the release on a wrong condition, or try to release a lock unconditionally, the type checker will complain that it is unable to prove lock safety. The safety indeed would be violated in some executions of the code.
The example illustrates enforcing sophisticated resource usage constraints in a mature, well-supported language, relying on the existing type system and type inferencing. All types have been inferred. The code used a particular form of constraint-based typing (type families) and a particular way of solving them. Type function applications are reduced when their arguments become sufficiently instantiated so that a definitional case may be selected.
One is reminded of the adage that the dependent-type checker cannot test for the value of dynamic input. The type checker can assure that the programmer does not forget such a test.
Fun with type functions
In ``Reflections on the work of C. A. R. Hoare.'' ed. A. W. Roscoe, Cliff B. Jones, and Ken Wood. Springer, 2010. pp. 303-333.
Joint work with Simon Peyton Jones and Chung-chieh Shan.
< http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/#fun >
The paper explains a simple version of the lock safety problem.
Variable (type)state `monad'
Lightweight static capabilities
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML