[Haskell-cafe] Announcing Halfs, a Haskell Filesystem

[Isaac Jones]

Halfs is a filesystem implemented in the functional programming
language Haskell. Halfs can be mounted and used like any other Linux
filesystem, or used as a library.  Halfs is a fork (and a port) of the
filesystem developed by Galois Connections.

We've created a virtual machine to make using Halfs extremely easy.
You don't need an extra partition or a thumb drive, or even Linux
(Windows and Mac OS can emulate the virtual machine).  For the
impatient, go to the quick start:
http://hackage.haskell.org/trac/halfs/wiki/QuickStart

The Halfs web page is here:
http://www.haskell.org/halfs/

Background:

In the course of developing a web server for an embedded operating
system, Galois Connections had need of a filesystem which was small
enough to alter to our needs and written in a high-level language so
that we could show certain high assurance properties about its
behavior. Since we had already ported the Haskell runtime to this
operating system, Haskell was the obvious language of choice. Halfs is
a port of our filesystem to Linux, with some modifications.

High assurance development is a methodology for creating software
systems that meet rigorously-defined specifications with a high degree
of confidence. That methodology comprises tools and practices. Its
goal is to produce such systems reliably and effectively, with an
ordinary degree of developer effort.

Haskell is particularly well-suited  to high assurance development. It
is a  high-level, fully-expressive, pure, functional  language, with a
powerful  type  system.  One  of  the obligations  of  high  assurance
development  is  the demonstration  of  strong correspondence  between
high-level executable models  and the eventual implementation. Haskell
supports  this directly:  it can  describe  systems all  the way  from
high-level  executable models through  to system  implementations. The
fact that Haskell is pure comes from its mathematical basis, and means
that,  by   default,  a  function   does  not  interfere   with  other
functions. The type  system is an automatic and  scalable proof engine
that  can encode  and  enforce desirable  properties. Together,  these
features allow  the correctness of complex systems  to be established,
making Haskell ideal for high assurance development.

The question was whether Haskell is well suited as the implementation
language for a filesystem, which involves fixed sized buffers, lots of
IO, and binary data structures. Though correctness is much more
important to us than performance, we hoped that a Haskell filesystem
would have acceptable performance, and that writing such low-level
code would not be awkward or error-prone.

We have developed a filesystem,  Halfs, which aims to answer the above
questions. One  may mount a Halfs  filesystem in Linux  using the FUSE
(Filesystem  in Userspace)  kernel  module. We  have  created two  new
monads, FSRead and FSWrite which  restrict the IO monad to reading and
writing operations respectively. For performance, Halfs uses efficient
mutable arrays for block IO, as well as caching for blocks and inodes.