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 withDB or 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.
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
withFile block. 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 >>= print
Above is the first example of the region-based file IO. Instead of handles, we have Qs -- marked handles. They are created by the function withFile and used similarly to regular handles. A special IOM monad is a newtype away from the regular IO. The phantom type parameter of the IOM monad, like the s parameter of the ST monad, marks the region.
*IORegions98Test> :t reader
reader :: Q mark -> IOM mark [Char]
According to its inferred type, the reader takes 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 IOM computation and return its result: test3 below works. An attempt to leak IOM out of withFile may 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 Typeable and so the required instance Typeable mark cannot 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
The module 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 a
We wish to assure that the handle Q never 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 Q is qGetChar, yet the latter introduces the type IOM. If we make sure that neither IOM nor Q may appear in the type of the values produced by withFile, our goal is achieved. Constraining the type of the result of withFile to be an instance of Typeable does the trick: since IOM mark a and Q mark must be fully polymorphic with respect to mark to 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 IORegions98E does not however provide any IOM computation 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 withFile may safely close the handle at that point. The module IORegions98E should not normally be touched by the end user. Still, there may be a need for computations with Q other than 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.IORegions98Test.hs [3K]
IORegions98Test1.hs [2K]
extensive test code, including all the tests by Brandon Moore.
RGN monad 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.
RGN monad and the tests
Philippa Cowderoy: Monad.Reader IssueFour 2005-06-27. The ImpureThoughts column. Section ``Policing the State''
< http://www.haskell.org/tmrwiki/ImpureThoughts_2f2 >
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML