Looking Out To Sea

This is part 2 of a series of posts looking at the paper Lightweight Static Capabilities by Kiselyov and Shan. Part 1 can be found here.

The next section of the paper is more theoretical. The authors introduce two notional languages, Strict and Lax, and their typing mechanisms. Strict has a “fancy” type system which specifies two list types (List and List+) and only the latter type can be deconstructed with head and tail functions. The List+ type can only be created by a special nonempty conversion, which cannot be applied to empty lists.

The Lax language has no such advanced typing facility and will happily accept nonempty(nil) as a legal construct. This language is more like a traditional functional language with a possibly-empty list type. In terms of typable operations Strict defines a smaller set than Lax, and every legal Strict program is a legal Lax program too. The authors define a mapping from Strict to Lax programs to allow embedding a statically safe program in Haskell, ML, etc.

This embedding is ultimately what we always attempt to do when programming. The set of things which the compiler will accept is necessarily larger than the set of things which will get us the right answer. Type systems aim to constrain the “acceptable” set slightly though there is still plenty of scope for bugs. :-) Some programming languages make it easier to write programs which are dangerously but subtly wrong. Using the full capabilities of a language like C all the time is incredibly foolhardy: not every situation demands pointer arithmetic. If we can use the type system to wall off “dangerous” code then all the better. Another example is the use of IO actions or unsafe* operations in Haskell. These are often used only where necessary in the former case, or walled off in an opaque module in the latter case. This walling-off allows us to concentrate our verification efforts to areas which can cause the most problems.

The resulting “embedded” code is the trusted kernel mentioned in the previous post. The reduction rules defined for Strict and Lax are contained in this kernel. The reduction rules for the non-empty list case are:

head (nonempty (cons E1 E2)) -> E1
tail (nonempty (cons E1 E2)) -> E2
indeed nil E1 E2             -> E1
indeed (cons E E') E1 E2     -> E2 (nonempty (cons E E'))

The first two rules define the operation of head and tail on a non-empty list. These operations aren’t defined for empty lists. The second two rules show how the non-empty type is constructed if the list is truly non-empty. Notice the similarity between indeed and Haskell’s maybe function (with arguments rearranged):

indeed :: List a -> b -> (FullList a -> b) -> b
maybe :: Maybe a -> b -> (a          -> b) -> b

The maybe function forces the user to deal with all cases in the option type by requiring functions and default values for each case. The indeed function goes one step further by not allowing any other way to take apart the list type — in order to use head and tail you have to convert the List to a FullList and only indeed can do that.

In the spirit of the maybe function for Maybe types and the either function for Either types it would seem sensible to have a list function for List types, which would take a function for each case suggested by a list. After a bit of reflection I think this is the fold, or rather maybe and either are specific folds.

Which all suggests that the toy example provided (reversing a linked list) can be safely recreated using a fold. If we look again at the safe version defined in the previous post we see two cases we have to deal with:

reverse :: List a -> List a -> List a
reverse xs acc = case full xs of
            Nothing -> acc
            Just ls -> reverse (tail ls) (cons (head ls) acc)

Stripping away all the plumbing stuff that’s going on here, we have two vital bits:

1. The return of the accumulator when the list is no longer non-empty, ie is empty.
2. Consing the head of the list onto the accumulator at each stage that the list is non-empty.

Step 1 is done automatically by the fold: it lets you iterate over values without being concerned about them running out. Step 2 is just the cons operation we know, with the order of arguments reversed. To actually reverse a list we supply an empty accumulator.

reverse in = foldl combiner acc in
  where combiner xs x = cons x xs
        acc = []

We know we can define this simple function as a one-liner but not all functions are as simple. The next section looks at array indexing operations. The motivating example this time is binary search over arrays — checking that all indexing operations remain in-bounds and that these constraints are ensured by the type system. By contrast with list reversal a binary search deals with several separate elements (the array, the lower and upper index) which cannot be hidden completely if we are to allow general array operations.