System.SafeHandles

http://okmij.org/ftp/Haskell/regions.html#light-weight

Lightweight monadic regions

The Abstract of the paper

We present Haskell libraries that statically ensure the safe use of resources such as file handles. We statically prevent accessing an already closed handle or forgetting to close it. The libraries can be trivially extended to other resources such as database connections and graphic contexts.

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.

Handle-based IO with the assured open/close protocol, see README This file contains the Security kernel. See SafeHandlesTest.hs for tests. This is the final solution: lightweight monadic regions with only type-level enforcement of region discipline

Documentation

data IORT s m v

The IO monad with safe handles and regions (SIO) is implemented as the monad transformer IORT (recursively) applied to IO.

Each region maintains the state listing all open handles assigned to the region. Since we already have IO, it is easy to implement the state as a mutable list (IORef of the list) and make this reference a pervasive environment. We could have used implicit parameters or implicit configurations to pass that IORef around. Here, we use ReaderT.

Instances

Monad m => Monad (IORT s m)

RMonadIO m => RMonadIO (IORT s m)

type SIO s = IORT s IO

data SHandle m

Our (safe) handle is labeled with the monad where it was created

runSIO :: (forall s. SIO s v) -> IO v

newRgn :: RMonadIO m => (forall s. IORT s m v) -> m v

There is no explicit close operation. A handle is automatically closed when its region is finished (normally or abnormally).

liftSIO :: Monad m => IORT s m a -> IORT s1 (IORT s m) a

Lift from one IORT to an IORT in a children region... IORT should be opaque to the user: hence this is not the instance of MonadTrans

newSHandle :: RMonadIO m => FilePath -> IOMode -> IORT s m (SHandle (IORT s m))

Create a new handle and assign it to the current region One can use liftIORT (newSHandle ...) to assign the handle to any parent region.

shDup :: RMonadIO m => SHandle (IORT s1 (IORT s m)) -> IORT s1 (IORT s m) (SHandle (IORT s m))

Duplicate a handle, returning a handle that can be used in the parent region (and can be returned from the current region as the result). This operation prolongs the life of a handle based on a _dynamic_ condition. If we know the lifetime of a handle statically, we can execute liftSIO (newSHandle ...) to place the handle in the corresponding region. If we don't know the lifetime of a handle statically, we place it in the inner region, and then extend its lifetime by reassigning to the parent region based on the dynamic conditions.

data IOMode

Constructors

ReadMode

WriteMode

AppendMode

ReadWriteMode

Instances

Enum IOMode

Eq IOMode

Ord IOMode

Read IOMode

Show IOMode

Ix IOMode

shGetLine :: (MonadRaise m1 m2, RMonadIO m2) => SHandle m1 -> m2 String

Safe-handle-based IO... The handle is assigned to the current region or its ancestor. So, we have to verify that the label of the handle is the prefix (perhaps improper) of the label of the monad (label of the region).

shPutStrLn :: (MonadRaise m1 m2, RMonadIO m2) => SHandle m1 -> String -> m2 ()

shIsEOF :: (MonadRaise m1 m2, RMonadIO m2) => SHandle m1 -> m2 Bool

shThrow :: RMonadIO m => Exception -> m a

It seems however that IOErrors don't invalidate the Handles. For example, if EOF is reported, we may try to reposition the file and read again. That's why in Posix, EOF and file errors can be cleared.

shCatch :: RMonadIO m => m a -> (Exception -> m a) -> m a

shReport :: RMonadIO m => String -> m ()

Useful for debugging

sNewIORef :: RMonadIO m => a -> m (IORef a)

make IORef available with SIO, so we may write tests that attempt to leak handles and computations with handles via assignment

sReadIORef :: RMonadIO m => IORef a -> m a

sWriteIORef :: RMonadIO m => IORef a -> a -> m ()