Home

Lightweight Monadic Regions

Oleg Kiselyov and Chung-chieh Shan. Lightweight Monadic Regions. Haskell'08.
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...

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.

I am starting to think we need a department for effect systems and related topics (though we managed without a monads department!)...

You'll probably want to read the code, so go ahead. The code makes it plain which features of the type system are needed to achieve the end result.

By Ehud Lamm at 2008-08-06 16:57 | Functional | Software Engineering | Type Theory | other blogs | 10886 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

You can only learn what you almost understand already...

...and though I don't almost understand Haskell, I do appreciate the overall goal of static type checking for resource management. Using the results of the defined code is not that difficult - I can follow that part well enough, so I would assume that programmers could be given libraries for various chores until they get more comfortable with the underlying mechanism. IOW, we all use libraries that we don't fully understand but still manage to get results.

Just a thought, but i was wondering if the mechanism was general enough to enforce further substructure. For example, files many times have structure that can be defined - e.g., an XML schema. The example given is making sure that the sequence of open-read/write-close is followed. Can one also get more granular and say that particular types of read/write operations have to follow a sequence?

By Chris Rathman at Wed, 2008-08-06 19:03 | login or register to post comments

Hmm, it sounds like session

Hmm, it sounds like session types could achieve that, if you model the I/O as a messaging protocol.

By naasking at Wed, 2008-08-06 19:48 | login or register to post comments

Syntax Overload

Having read both papers at the site, "Lightweight Monadic Regions" and "Position: Lightweight static resources", one cannot but admire the authors' ingenuity. It is very clever, indeed. Having said that, the clarity of their approach is seriously hindered by Haskell's language syntax. For instance, the natural number 5 must be represented as something like U (U B1 B0) B1! Also, type-level programming in this style leaves a lot to be desired.

Perhaps it is time to revisit Haskell's syntax for type-level programming?

By Pal-Kristian Engstad at Thu, 2008-08-07 23:08 | login or register to post comments

Agreed

Agreed on all counts. But it is definitely safe to say that LtU officially admires the authors' ingenuity!

By Matt Hellige at Fri, 2008-08-08 04:32 | login or register to post comments

Good resource management

Deterministic resource management can be easily done with higher-order functions.

let file name f =
  let handle = file_open name in
    f handle;
    file_close handle
;;

file "foo.txt" (fun h -> file_write h "bar")

That way, you're always sure you close what you open.

By Mathias Gaunard at Sun, 2008-08-10 15:52 | login or register to post comments

The file handle can escape

The file handle can escape the function's scope in a language with mutable state (like ML), so you can still invoke an operation on a closed file handle. Proper monadic encapsulation, as in this paper, prevents such invalid uses.

By naasking at Sun, 2008-08-10 16:13 | login or register to post comments

Even if you aren't worried

Even if you aren't worried about leaking handle out of this context, this scheme isn't general enough to cover all cases. There's no way this will ever produce: open A, open B, close A, close B.

By Matt M at Sun, 2008-08-10 19:16 | login or register to post comments

LIFO resource management

Of course: it's LIFO.
Open A, Open B, close B, close A.

It's really similar to what you get using destructors, scope-bound resource management, and RAII, which are the recommended way to program in C++.

By Mathias Gaunard at Sun, 2008-08-10 22:27 | login or register to post comments

LIFO

It's a nice idiom if it fits, but sometimes it doesn't. How does it help you manage network connections on a server?

BTW. I find the use of side effects in constructors and destructors to be pretty ugly, but will refrain from making a comparison to the recommended way to eat soup with a fork.

By Matt M at Sun, 2008-08-10 22:51 | login or register to post comments