Roll Your Own Window Manager: Part 1: Defining and Testing a Model

For the past few weeks the Spencer Janssen, Jason Creighton and I’ve been working on xmonad, a tiling window manager for X. The window manager is written in Haskell, and version 0.1 comes in at a light 490 lines of code.

It has been fun working on xmonad, and the result has been a very solid, reliable application, built very quickly. Some of the techniques we used to build xmonad aren’t widely known, so in this series of posts I’m going to describe how we did it. In particular, I’ll look at:

• Building custom data structures
• Using QuickCheck
• Exploiting monad transformers
• Leaning on type system guarantees
• The foreign function interface
• Cabal, Hackage, and library distribution

and how we’d go about rolling our own window manager!

Programming precision

The best programs feel like precision machines. Each component is well specified, and does one task simply and exactly. At their best, these programs have a beautiful, exact coherence. Such programs aren’t common, but when you’ve written one, you know it.

While not every program will turn out like this, we do have an idea what qualities the code must have to have that feeling of precision engineering:

• Referential transparency
• Flexibility and genericity
• Modularity and orthogonality
• Precise specification and testing

Code with these features is easy to hack on, to refactor, to tear apart and move around. The code feels like lego in your hands. It doesn’t go wrong when you tweak it, since you understand the code completely, once you understand it in isolation. There are no nasty corner cases to trip on, and you can adapt the code to new circumstances without losing your hard-won guarantees. Writing this kind of code makes programming a fufilling experience.

Programming languages, and their cultures, shape thought, and tend to encourage certain programming practices. Several languages emphasise production of code with the above qualities. One language in particular takes this idea of programming as precision engineering very seriously: Haskell.

By guaranteeing referential transparency (purity) by default, Haskell code starts life in the world in modular, isolated units with nice properties. In particular, equational reasoning just works, making refactoring easy. An expressive static type system adds to this by providing guaranteed genericity via parametric polymorphism, leading to code that is clearer, and that doesn’t fall apart when you change the data types in your program. The expressive type system helps further allowing the crafty programmer to specify programming constraints in types, leading to machine checked invariants enforced by the compiler (allowing, for example, the programmer to rule out certain functions from use).

Finally, to round out the story, we get precise specification and testing of program components using QuickCheck, which exploits purity and rich typing to generate test cases automatically, leading to semi-formal specification and checking of programs. QuickCheck sets up a feedback loop, where code written with an eye to its high-level properties, tends to become simpler, easier to understand and easier to reuse.

It is this interplay between language features like purity and polymorphism, leading to code with the qualities of precision engineering, that makes Haskell so addictive.

So, now, lets look at how we’d go about implementing a window manager in Haskell, while maintaining these qualities of purity, genericity, modularity and testability.

A window manager model

A window manager is basically a thin layer of glue code between the user’s keyboard and mouse, and the X Window graphics system. The user triggers events, the window manager interprets those events, calling X functions to produce effects in the graphics subsystem. There appears to be a lot of potentially gunky IO, and very little logic involved. Is there any hope for pure, composable code here?

A little thought, and it becomes clear that a window manager acts an interpreter. It reads a stream of commands from the user, which are interpreted as instructions to modify an internal model of the window system. Actually calling out to X (and modifying the display) falls out as simply rendering the internal model. What we have is a simple model-view-controller architecture, where all the important application logic is in the window system model.

The key design decision, then, is to build a correct model of the window system. By building the model as a purely functional data structure in Haskell, we will be able to automatically test the core logic of the window manager, and hopefully come up with a clean, orthogonal window manager api. The rest of the window manager will just be a thin IO layer over the core data structure operations. No core logic of the program will be mixed in with side-effecting code.

A simple tiling window manager

We will implement a simple fullscreen window manager in the style of xmonad or dwm, with multiple virtual workspaces. Each workspace will store a stack of windows. At any point only one window will be visible: the top-most window on the stack. Windows may appear on only one stack at any time. Keyboard control will be used to rotate the current stack, move windows to other workspaces, and switch focus to other workspaces. Here’s what the window system will look like:

An obvious data structure to represent this two-level workspace/window stack system is:

    data StackSet a =
        StackSet
            { current :: Int,          -- the current workspace
              stacks  :: Map Int [a]   -- map workspaces to window stacks
            } deriving Eq

This declares a new Haskell data structure, a StackSet. It holds elements of some type ‘a’ (i.e. windows), in a two-level structure. Each screen stores a simple stack of windows, and we can use a simple list, [a], for this. Which virtual workspace holds which window stack is tracked with a finite map, connecting workspace indicies to window stacks. The data structure is polymorphic in its elements, which allows us to enforce, in the type of window system functions, that they may not depend on particular window types. Effectively, the type system will guarantee that the StackSet will be a window manager only: it won’t be possible to write StackSet code that directly manipulates the contents of windows. By abstracting over the particular elements stored in the StackSet, we’ll also be able to more easily test the structure.

Our window manager model has two other invariants that must hold at all times: that the ‘current’ workspace must always refer to a valid index, and that no window may ever appear more than once in the StackSet. We will come back to this function later as our first QuickCheck property.

The API

We can now just write down in pseudocode (well, let’s just use actual Haskell code), precisely what operations our window manager will support.

    -- Constructing a new window system, given the number of workspaces to use
    empty  :: Int -> StackSet a

    -- Extract the currently visible window, or nothing if the workspace is empty
    peek   :: StackSet a -> Maybe a

    -- Bring a new window under management, or raise it if already managed
    push   :: a -> StackSet a -> StackSet a

    -- Delete a window from the system
    delete :: a -> StackSet a -> StackSet a

There are some additional operations we’d like to support, involving shifting focus, moving windows to new workspaces, and the like:

    -- Move focus to the next or previous window in the current stack
    rotate :: Direction -> StackSet a -> StackSet a

    -- Transfer focus to another workspace
    view   :: Int -> StackSet a -> StackSet a

    -- Move the current window to a new workspace
    shift  :: Int -> StackSet a -> StackSet a

Completing our Haskell model of the window system is now just a matter of filling in the blanks.

Constructing a window system model

Let’s walk through the implementation of this API. First thing, some imports:

    {-# OPTIONS -fglasgow-exts #-}

    module TinyWM where

    import Data.Maybe   
    import Data.Map (Map)
    import qualified Data.Map as M
    import qualified Data.List as L

The first line is an options pragma. We’ll use pattern guards, which are a GHC extension (to be added for Haskell’), since they enable more concise pattern matching. We’ll import Map and List qualified, so we can reuse some names from those modules for our own purposes.

Now, implementing ’empty’ is easy:

    empty :: Ord a => Int -> StackSet a
    empty n = StackSet { current = 0, stacks  = ws }
      where
          ws = M.fromList (zip [0..n-1] (repeat []))

That is, given a number of workspaces (say, 9), build up that many empty workspaces in the StackSet. Focus is set to workspace at index 0. The Ord constraint is needed for StackSet elements, since we’re using a Map underneath. Construction of an empty StackSet has O(n) complexity, on the number of workspaces.

Next up is ‘peek’. Given a StackSet, extract the element on the top of the current workspace stack. If there’s no window on the current screen, return Nothing instead. We can do this in O(log n) time, using Data.Map.lookup to find the current stack, and then pattern match on the stack to get the top element:

    peek :: Ord a => StackSet a -> Maybe a
    peek w | Just (x:_) <- M.lookup (current w) (stacks w) = Just x
           | otherwise                                     = Nothing

Note the use of pattern guards to perform the lookup and head-extraction, leaving a nice fall through case for Nothing.

Now we’ll define ‘push’, which, given a new window, brings it under management by our window manager. If the window is already managed, on any stack, we move it to the top of the stack (which will also bring it into focus).

    push :: Ord a => a -> StackSet a -> StackSet a
    push k w = insert k (current w) w

Ok, that was cheating ;-) We defined ‘push’ as ‘insert’ on the current stack. Here’s how we actually do an ‘insert’:

    insert :: Ord a => a -> Int -> StackSet a -> StackSet a
    insert w n old = new { stacks = M.adjust (w:) n (stacks new) }
        where new = delete w old

That’s using Haskell record syntax. First thing is to completely ‘delete’ our window, ‘k’, from the StackSet, yielding a new, modified StackSet, ‘new’. We then use Data.Map’s update function to push the new window onto the top of the current stack. By deleting first we ensure we never accidentally duplicate a window we’re already managing, maintaining our uniqueness invariant.

So how do we delete a window from the StackSet:

    delete :: Ord a => a -> StackSet a -> StackSet a
    delete k w = maybe w del $ L.find ((k `elem`) . snd) (M.assocs (stacks w))
      where
        del (i,_) = w { stacks = M.adjust (L.delete k) i (stacks w) }

And that’s the only slightly tricky bit. First ‘find’ the stack of the window we want to to delete. Then remove the window from the given stack, in the Map, using the Map ‘adjust’ function. We could simplify this by storing a reverse map of windows back to their stacks (at the cost of complicating our bookkeeping a little). If the window is not found, we return the StackSet unmodified.

How about functions that manipulate focus and workspaces? One such function is ‘shift’, which moves the window currently in focus to the top of the stack of some other workspace. We can implement that as:

    shift :: (Ord a) => Int -> StackSet a -> StackSet a
    shift n w = maybe w (k -> insert k n w) (peek w)

It just peeks the window on the current stack, and relies on ‘insert’ to move it to a new workspace, ensuring it is deleted from the current workspace.

Another key function is ‘rotate’, which changes which window on the current stack is in focus. The semantics should be:

    intial window stack: [5,6,7,8,1,2,3,4]

    rotate EQ   -->  [5,6,7,8,1,2,3,4]
    rotate GT   -->  [6,7,8,1,2,3,4,5]
    rotate LT   -->  [4,5,6,7,8,1,2,3]

We can implement this behaviour as:

    rotate :: Ordering -> StackSet a -> StackSet a
    rotate o w = w { stacks = M.adjust rot (current w) (stacks w) }
      where
        rot [] = []
        rot xs = case o of
            GT -> tail xs ++ [head xs]
            LT -> last xs : init xs
            _  -> xs

Easy, so given a direction to rotate (specified by the Ordering argument), either move the head of the stack to the bottom, or move the bottom of the stack to the top. If the stack is empty, it is unchanged.

Finally, moving focus to a new workspace is simply:

    view :: Int -> StackSet a -> StackSet a
    view n w | M.member n (stacks w) = w { current = n }
             | otherwise             = w

And that’s it, the core logic of our window manager is specified. Let’s fire up QuickCheck to make sure it works!

QuickCheck your window manager

QuickCheck is an automatic testing library for Haskell. Generic properties are specified for functions, relationships between functions, and connections between implementations and models. We can now spec out the properties that hold for our window manager core.

We’ll stick all the properties in a new module, importing our window manager core as TinyWM, and the QuickCheck modules:

    {-# OPTIONS -fglasgow-exts #-}

    import TinyWM

    import Text.Show.Functions
    import Test.QuickCheck

    import Data.Maybe
    import Data.Map (Map)
    import qualified Data.Map as M
    import qualified Data.List as L

Generating random window manager states

QuickCheck generates random test data for our functions, using the Arbitrary type class. For this article, I’ll be using QuickCheck 2, the experimental branch, as it offers some convenient features over the standard QuickCheck. The core code is the same, however. The first step is to write an instance of Arbitrary for the StackSet type. QuickCheck will use this to generate random window system states (i.e. random StackSet data structures), and then test our properties against these random states. If the random test generator is sufficiently comprehensive, we’ll have a pretty good idea that the code is correct.

To generate random StackSets we’ll take the approach of generating random lists of windows, and using this to populate a StackSet.

    instance (Ord a, Arbitrary a) => Arbitrary (StackSet a) where
        arbitrary = do
            sz <- choose (1,20)     -- pick a random number of workspaces
            n  <- choose (0,sz-1)   -- choose one to be in focus
            ls <- vector sz         -- generate random window stacks for each workspace
            return $ fromList (fromIntegral n,ls)

    instance (Ord a, CoArbitrary a) => CoArbitrary (StackSet a) where
        coarbitrary s = coarbitrary (toList s)

The details of the QuickCheck Arbitrary instances are best followed up by reading the source for QuickCheck. Essentially, we randomly choose a size, ‘sz’, from 1 to 20 for the number of workspaces. We pick a workspace, n, to be in focus, and then generate ‘sz’ random lists, using ‘vector’. ‘fromList’ then constructs a StackSet from this list of random lists. The CoArbitrary instance will let us generate random functions on StackSet, which might be fun.

‘fromList’ on StackSet, which builds a StackSet from a list of lists, can be defined by folding insert over the lists. ‘toList’ just flattens the Map structure back to a list:

    fromList :: Ord a => (Int, [[a]]) -> StackSet a
    fromList (o,xs) = view o $
        foldr ((i,ys) s ->
            foldr (a t -> insert a i t) s ys)
                (empty (length xs)) (zip [0..] xs)

    toList  :: StackSet a -> (Int,[[a]])
    toList x = (current x, map snd $ M.toList (stacks x))

We can have a look at the StackSets generated with this Arbitrary instance using ‘verboseCheck’ from QuickCheck version 1, or inserting a ‘trace’ into our Arbitrary instance for QuickCheck 2. When run on a simple property, using the ‘quickCheck’ method, we can see the different StackSets being generated:

    *Main> quickCheck (x -> x == (x :: StackSet Int))
    StackSet {current = 2, stacks = fromList [(0,[]),(1,[]),(2,[])]}
    StackSet {current = 2, stacks = fromList [(0,[0]),(1,[]),(2,[-1])]}
    StackSet {current = 0, stacks = fromList [(0,[2])]}
    StackSet {current = 0, stacks = fromList [(0,[0,3,2]),(1,[-3]),(2,[])]}
    StackSet {current = 0, stacks = fromList [(0,[-1,2,-2]),(1,[]),(2,[-3,-4]),(3,[1]),(4,[])]}
    StackSet {current = 0, stacks = fromList [(0,[1,-3,-2]),(1,[0]),(2,[-1,-4])]}
    StackSet {current = 0, stacks = fromList [(0,[])]}
    StackSet {current = 2, stacks = fromList [(0,[1,3]),(1,[]),(2,[2,-6,-7,-3,-2])]}
    ...
    +++ OK, passed 100 tests.

Cool! Random window system states, with good coverage (there’s a nice mixture of small and large workspaces, and empty stacks. And happily, x == x holds too. When writing Arbitrary generators for complex types, it is is important to always confirm that the generator is producing good coverage of the inhabitants of your type.

Simple testing: equality on StackSets

Now, given a random generator for StackSets, we can test some simple properties. Let’s first double-check the derived equality functions for StackSet makes sense. Rather than instantiate our StackSet with X system windows, we can rely on the polymorphic type of StackSet, and its functions, to ensure that the api works for any element type, without depending on a particular concrete element type in any way. This means we can then simply test the api using Int elements in the StackSet, rather than actual X windows, thank to the type system guarantees.

Given random StackSet’s of Int, we can, for example, check the reflexivity of equality on StackSets, by simply writing:

    prop_eq_refl (a :: T) = a == a

This better be true, or something bad is happening! To check it, we can fire up ghci, and run the ‘quickCheck’ function:

    $ ghci Properties.hs

    *Main> quickCheck prop_eq_refl
    +++ OK, passed 100 tests.

Now, what about some other properties of a true equality: symmetry, transitivity, and substitution:

    prop_eq_symm (a :: T) b   = a == b ==> b == a

    prop_eq_tran (a :: T) b c = a == b && b == c ==> a == c

    prop_eq_subs (a :: T) b f = a == b ==> f a == f b
        where
            _ = f :: T -> T

Ok. This looks nice. Notice, in particular, the substitution property says, if we have two StackSets, a and b, that are equal, applying some random function, f, to ‘a’ yields the same result as applying it to ‘b’. Yes: QuickCheck generates random functions on StackSets for us! (and yay for referential transparency, while we’re here).

We can add some more properties, and run them all together, with a little driver:

main = do
    let runT s a = do print s; a

    runT "Eq" $ do
        quickCheck prop_eq_refl
        quickCheck prop_eq_symm
        quickCheck prop_eq_tran
        quickCheck prop_eq_subs

Running these from the command line as:

    $ runhaskell Properties.hs
    "Eq"
    +++ OK, passed 100 tests.
    *** Gave up! Passed only 0 tests.
    *** Gave up! Passed only 0 tests.
    *** Gave up! Passed only 1 tests.

What happened? No tests failed, but QuickCheck gave up (after generating 500 test cases) for the new properties. The problem with the new tests is that they require identical StackSets to be generated, but our random generator doesn’t do that very often, with the result that not enough useful test data satisifed the ‘a == b’ constraint. We could modify the generator to produce more duplicates, but this doesn’t seem very interesting. Let’s instead look at testing window manager functions!

Automatic window manager testing

So the question is: what high level properties does our window manager have? If we look at the api, and think about the desired behaviour, there are some obvious nice properties that should hold. The first one being our StackSet invariants:

• Each window occurs on only one workspace, and only once in a given stack
• The index of the currently focused workspace should always be a valid workspace.

We can specify this invariant as a Haskell function:

    invariant :: StackSet a -> Bool
    invariant w = inBounds w && noDuplicates w 
        where
            inBounds x      = current x >= 0 && current x < sz
                where sz = size (stacks x)

            noDuplicates ws = nub xs == xs
                where xs = concat . elems . stacks $ ws

And now we can check this invariant holds for every StackSet generated by QuickCheck, and again, that it holds after applying functions from our window manager api, to modify StackSets:

    prop_invariant x = invariant x

    prop_empty    n          = n > 0 ==> invariant $ empty n
    prop_view     n (x :: T) =           invariant $ view n x
    prop_rotate   n (x :: T) =           invariant $ rotate n x
    prop_push     n (x :: T) =           invariant $ push n x
    prop_delete   n (x :: T) =           invariant $ delete n x

    prop_shift    n (x :: T) = n >= 0 && n < size x
                                     ==> invariant $ shift n x

    prop_insert   n i (x :: T) = i >= 0 && i < size x
                                     ==> invariant $ insert n i x

Ok, let’s run this, and see if our functions are maintaining the invariant:

    $ runhaskell Properties.hs
    "invariant"
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    *** Gave up! Passed only 23 tests.
    *** Gave up! Passed only 32 tests.

Great! They all pass, though the additional constraints on shift and insert (that indicies are in bounds), mean that less tests were generated than we’d like. But the invariant seems to hold, so now lets look at properties that hold for the basic window manager api.

Firstly, the ’empty’ function should build a window manager state such that:

• All workspaces are empty
• Focus is on the workspace with index 0.

We can state these rules with the properties:

    -- empty StackSets have no windows in them
    prop_empty n = n > 0 ==> all null (M.elems (stacks x))
        where x = empty n :: T

    -- empty StackSets always have focus on workspace 0
    prop_empty_current n = n > 0 ==> current x == 0
        where x = empty n :: T

Running these, our ’empty’ function appears to be ok:

    $ runhaskell Properties.hs
    "empty"
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.

More complex properties

What properties are maintained by ‘push’, the act of bringing a new window under management? Obviously, if a window is pushed, it should now be a member of the StackSet somewhere. We’ll define an auxillary predicate, ‘member’, which checks a given window is found somewhere in the StackSet. With this, we can state the property that ‘push’ makes a window a member of the StackSet:

    prop_push  i n = n > 0 ==> member i (push i x) 
        where x = empty n :: T

And QuickCheck indeed confirms this.

A related property is, if we have an operation ‘pop’, which deletes the top window of the current stack, pop . push should be the identity. That is:

• Creating and immediately deleting a window leaves the window system unchanged.

So this should hold:

    prop_push_pop (x :: T) i = pop (push i x) == x

Running this and we get:

    "push"
    *** Failed! Falsifiable (after 5 tests and 1 shrink):     
    StackSet {current = 0, stacks = fromList [(0,[3,4,2]),(1,[-2])]}
    2

Ah ha! What happened? We attempted to push, and then delete, window ‘2’ from our StackSet. But QuickCheck found a case, after 5 tests, where this didn’t leave us with the original state.

The corner case we forgot about was when the window ‘2’ was already in the StackSet. Pushing it would then just move it to the current stack, but not add it to the StackSet. A pop then removes it altogether, leaving us with a StackSet with one less window than we started with. This is actually the correct behaviour (since ‘push’ should raise a window if it is already under management). So we must refine our property to be:

    prop_push_pop (x :: T) i = not (member i x) ==> pop (push i x) == x

And indeed, this now holds. QuickCheck makes us think more about our code.

Idempotent everything

A number of functions in the api should be idempotent. That is, many functions, when applied twice to a StackSet, have the same result as if they were applied only once — which is often quite intuitive. Such functions seem to be very common, and idempotency is a useful property to keep in mind when developing an api: what happens if I run this function twice in a row? Will that do anything strange?

Our window manager should have a number of idempotent operations. For example: focusing a window once, is the same as focusing it several times; deleting a window twice is the same as deleting it only once:

    -- shifting workspace is idempotent
    prop_view_idem (x :: T) r =
        let i = fromIntegral $ r `mod` sz
            sz = size x
        in view i (view i x) == (view i x)

    -- deletion is idempotent
    prop_delete_idem i (x :: T) = delete i x == delete i (delete i x)

    -- push is idempotent
    prop_push_idem i (x :: T) = push i x == push i (push i x)

And QuickCheck confirms that these hold.

Many window manager operations are trivially reversible

What about properties to do with moving windows around? There are some properties about the reversibility of focus shifting. We should be able to move focus around the current window stack, and expect to reach our original window layout by reversing the steps we took. Let’s state those properties:

    prop_rotate_rotate1 (x :: T) = rotate LT (rotate GT x) == x

That is, shifting focus by one step is reversible. We can also shift all the way down a stack and we should end up with focus back where we started:

    prop_rotate_all (x :: T) = foldr (_ y -> rotate GT y) x [1..n] == x
      where 
        n = height (current x) x

And QuickCheck says our window manager model obeys this. Another property states that moving windows across workspaces is reversible:

• Moving a window from workspace A to workspace B, and back, should be the same as if it were never moved.

We implement moving of windows to new workspaces with ‘shift’, and actual changing focus with ‘view’. That is, ‘view . shift’, moves a window, and changes focus to a new workspace. We can state this property as:

    prop_shift_reversible r (x :: T) =
            (view n . shift n . view m . shift m) x == x
       where
            n  = current x                        -- the current workspace
            m  = fromIntegral $ r `mod` (size x)  -- another random workspace

Running this property, and it fails!

    $ runhaskell Properties.hs
    "shift"
    *** Failed! Falsifiable (after 9 tests and 1 shrink):  
    0
    StackSet {current = 1, stacks = fromList [(0,[-1,-8,1,-7,5,0,7]),(1,[])]}

What happened. We see the currently focused workspace was #1, which is []. Ah… so we tried to move a window from an empty workspace 1, onto workspace 0. This does nothing. We then moved the window on top of workspace 0 over to workspace 1. The final state would be:

    StackSet {current = 1, stacks = fromList [(0,[-8,1,-7,5,0,7]),(1,[-1])]}

Not where we started. So in fact, our inversible rule only holds if there was a window to move in the first place. We can augment our property with a predicate, ‘height’ that checks a workspace is non-empty:

    prop_shift_reversible r (x :: T) =
       height n x > 0 ==> 
            (view n . shift n . view m . shift m) x == x

When we run this, all is well:

    $ runhaskell Properties.hs
    "shift"
    +++ OK, passed 100 tests.

Nice, our window manager model seems to be making sense!

Running the lot

We can now run all our properties, and subject the window manager to thousands of tests:

    $ runhaskell Properties.hs
    "Eq"
    +++ OK, passed 100 tests.
    *** Gave up! Passed only 1 tests.
    *** Gave up! Passed only 0 tests.
    *** Gave up! Passed only 2 tests.
    "invariant"
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    *** Gave up! Passed only 31 tests.
    *** Gave up! Passed only 18 tests.
    "empty"
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    "push"
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    "delete"
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    "peek"
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    "rotate"
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    "view"
    +++ OK, passed 100 tests.
    +++ OK, passed 100 tests.
    "shift"
    +++ OK, passed 100 tests.

Conclusion

We’ve looked at how to build a custom purely functional data structure in Haskell, to implement the core logic of a real world window manager, and then how to specify and test key high-level properties of the api. The result is a precise, simple, and well understood window manager model.

The window manager model described in this article is actually running on my laptop as I write: it is the xmonad window manager. And it just works! By specifying high level properties the window manager should have, as QuickCheck code, we have been able to automatically verify that xmonad is behaving correctly, while radically modifying it. The code has stayed clean, small and well understood. In fact, QuickCheck informed the window manager behaviour: the semantics of ‘promote’ (moving a window into focus) was changed to have simpler properties, as we have found several times that simpler QuickCheck properties tend to result in simpler, more intuitive behaviour from the user’s point of view.

In the next article we’ll look at how to wrap the core logic and data structure of our window manager in an IO skin that intercepts X events, and maps them onto our window manager api. We’ll also consider how to render our StackSet window manager model to the graphics subsystem, via X calls.

References

The code and QuickCheck properties are available below, and I used QuickCheck 2, and GHC 6.6 to implement the system.

• Source for the StackSet window manager model (raw)
• Source for the QuickCheck properties (raw)
• QuickCheck 2
• The xmonad window manager, the actual window manager described in this article.