In part 1
of this series we looked at how to define the core of a window manager
for X in Haskell. This provided the core
logic of the xmonad tiling window
manager. The specification of the window manager as a data structure
and its accompanying API enabled us to write high level QuickCheck
properties to automatically test the window manager, leading to good
assurance that our implementation was correct. The window manager
modeled was a very simple full screen window manager, where the focused
window was always the only window visible.
In this article we reimplement the window manager core using a more
sophisticated data structure -- a "zipper" -- which will allow us to
track focus on each workspace automatically, by maintaining a cursor
into an updateable workspace tree. This data structure will
form the basis of a proper tiling window manager, where multiple windows
are visible on the screen simultaneously. By using a data structure
that tracks focus for us, we end up with much simpler code, and a
clearer understanding of how focus is manipulated by the window manager.
The problem with a finite maps
The original StackSet data structure, which modeled a
multiple-workspace fullscreen window manager, was quite simple:
data StackSet a =
StackSet
{ current :: Int,
stacks :: Map Int [a]
} deriving Eq
This is the obvious way to associate stacks of windows with workspaces: use a
lookup table to map workspace names (here just Int keys) to lists of
windows. We chose to use a finite map, a purely functional lookup table. In order to track the
current workspace, we store separately the key of the current workspace.
The simplicity of this data structure, however, limits its usefulness.
The problem with the StackSet as defined is that it only allows us to
track one focused window on each workspace: the window at the head of
each window list. This is fine for very simple fullscreen window
managers, as only one window is ever visible anyway. However, a true
tiling window manager, such as xmonad,
allows us tile many windows on the screen simultaneously, with focus
available to any window on the screen. The windows are tiled to the
screen like so:
In this picture, the current workspace contains 4 windows. The head of
the window list, window #1, is tiled first, and is given the largest
area. However, keyboard focus is actually on window #3. Our StackSet
data structure implemented as a Map is not able to handle arbitrary
focus as it stands. So the problem then is how best to extend the
StackSet type to handle tiling of workspaces, with arbitrary focus.
The naive approach: more tables
One solution is to augment the workspace type with an additional table:
data StackSet a =
StackSet
{ current :: Int,
stacks :: Map Int [a],
focus :: Map Int a
}
Now we maintain a separate mapping of workspaces, to the focused window
on each workspace. This is simple enough, and works in practice
(indeed, xmonad 0.1 does just this). However, there is a certain
awkwardness to it: by adding a new table we have obligated ourselves to
a second layer of bookkeeping. When focus changes we have two tables
to update and to keep consistent with each other.
The inelegance of this approach becomes apparent when we implement
functions that affect focus and will require manipulating both tables.
One such operation is 'delete'. For a basic fullscreen window manager,
where focus is always the head of the list, delete has an obvious
implementation. Given a window, a workspace and a StackSet, we can
remove an arbitrary window from the window manager by removing it from
the window list:
delete :: w -> i -> StackSet i w -> StackSet i w
delete win wrk ss = ss { stacks = M.adjust (delete win) wrk (stacks ss) }
So 'delete' on the focused window simply calls the 'delete' function of
the list library, and will move focus to the next element in the list.
However, allowing focus on any element in the list complicates the
logic -- we have two data structures to keep up to date:
delete :: w -> i -> StackSet i w -> StackSet i w
delete win wrk ss =
ss { stacks = M.adjust (delete win) wrk (stacks ss) }
, focus = M.update (\k -> if k == win then elemAfter k (stacks ss ! wrk)
else Just k) wrk
(focus ss)
}
So if we're deleting the currently focused element, then focus moves to
the element after the current element, otherwise focus is unchanged. The
definition of 'insert' also changes in a similar way, as inserting a window
should now insert to the right of the currently focused window.
In addition, the tracking of focus in a separate table means we need to make a
policy decision about where focus goes in the presence of insert and delete.
Under the simple workspace-as-list implementation, there was only one
possible implementation, now we can set focus anywhere, so we are forced
to state precisely what the behaviour should be. The obvious behaviour
is that: delete . insert should be the identity, and leave focus
unchanged. This would allows the user to delete transient popup windows,
without losing focus on the window they're working on. Ensuring this is
the case complicates the code still further.
All this extra work is very unsatisfying! More book keeping means more code,
and more chance for bugs. What we really need is a data structure that
tracks focus by design. So let's follow the functional programmer's
motto: write less, think more!
A Zipper for Trees
The zipper (pdf) is a lovely simple,
pure data structure first described by Huet. A zipper is basically a
cursor deep into a structure, allowing O(1) updates at the cursor site.
By recording a path from the root to the cursor it is possible to
navigate locally around the cursor site, while keeping track of the
entire structure. A zipper can also be considered as a delimited
continuation reified as data. In summary, it provides a natural
interface for operations on a distinguished position in a data
structure: exactly what we need for tracking focus in our window
manager.
Let us consider a simple zipper for the following tree data type (from
Huet's paper):
data Tree a = Item a | Node [Tree a]
A zipper for this structure gives us a currently focused node, along
with a path back up to a parent node, and to the left and right
siblings. We can implement this as:
data Path a = Top
| Point { left :: [Tree a]
, right :: [Tree a]
, up :: Path a }
data Cursor a = Cursor { it :: Tree a
, context :: Path a }
So, consider the tree representing the parse of the expression: (a * b) + (c * d):
expr :: Tree String
expr = Node [ Node [ Item "a", Item "*", Item "b"]
, Item "+"
, Node [ Item "c", Item "*", Item "d"] ]
We can visualise this tree as:
Now, we can focus on a particular element of this tree, for
example, the second "*" node, using a Cursor type. The following
zipper gives us the binary tree with focus set on the "*" node.
subexpr :: Cursor String
subexpr = Cursor
{ it = Item "*"
, context = Point
{ left = [Item "c"]
, right = [Item "d"]
, up = Point
{ left = [ Item "+"
, Node [ Item "a", Item "*", Item "b"] ]
, right = []
, up = Top } } }
Which we can visualise as a sort of unfolded tree, where the focused
item is the top of the tree (the green branch represents the path back
to the parent node):
It is as if we had picked up the tree by the "*" node, and let the other
branches hang down.
The zipper gives us a natural set of O(1) operations on the focused
node. To move focus to the left of the current node:
focusLeft :: Cursor a -> Cursor a
focusLeft c@(Cursor t p) = case p of
Point (l:ls) rs up -> Cursor l (Point ls (t:rs) up)
_ -> c
Applying 'focusLeft' to our subexpression relinks the local nodes,
shifting focus to the item 'c':
> focusLeft subexpr
Cursor { it = Item "c"
, context = Point
{ left = []
, right = [Item "*",Item "d"]
, up = Point
{ left = [Item "+",Node [Item "a",Item "*",Item "b"]]
, right = []
, up = Top } } }
Which yields the tree:
Notice that the 'up' parts of the tree haven't changed -- the changes
were local to the current subexpression, causing focus to cycle left.
We can also move focus back up the tree to the parent, by following the
'up' path:
focusUp :: Cursor a -> Cursor a
focusUp c@(Cursor t p) = case p of
Top -> c
Point ls rs up -> Cursor (Node (reverse ls ++ t : rs)) up
Moving up the tree collapses the cursor path.
> focusUp subexpr
Cursor { it = Node [Item "c",Item "*",Item "d"]
, context = Point
{ left = [Item "+",Node [Item "a",Item "*",Item "b"]]
, right = []
, up = Top } }
Other important operations on the cursor are 'insert' and 'delete'. Now
that we have a precise notion of focus, we can specify the behaviour of
focus when inserting a new node quite precisely. Either we insert to the
left of the current node, and move focus to this new node:
insertLeft :: Tree a -> Cursor a -> Cursor a
insertLeft a c@(Cursor t p) = case p of
Top -> undefined
Point ls rs up -> Cursor a (Point ls (t:rs) up)
Or we insert to the right:
insertRight :: Tree a -> Cursor a -> Cursor a
insertRight a c@(Cursor t p) = case p of
Top -> undefined
Point ls rs up -> Cursor a (Point (t:ls) rs up)
Lovely! Our data structure gives us an exact account of how focus
changes during an insert operation, with no extra book keeping.
From here we should be able to map focus in the window manager, onto
operations on the cursor position in the zipper, directly implementing
the window manager policies we decide on.
'delete' is slightly more complex: we need to consider when deleting the
current node whether to move focus to the left or right, or if the node
is empty, to move focus up the tree:
delete :: Cursor a -> Cursor a
delete (Cursor _ p) = case p of
Top -> undefined
Point ls (r:rs) up -> Cursor r (Point ls rs up)
Point (l:ls) [] up -> Cursor l (Point ls [] up)
Point [] [] up -> Cursor (Node []) up
We see again how the data structure forces us to think about the
behaviour of focus during critical operations, and also gives us simple,
clear operations. Let's see now how to use this cursor data type to our
window manager.
A Zipper for a Window Manager
Clearly there is a possibility of adapting the zipper-based focus mechanism to
our window manager problem. However, rather than there being just one
point of focus in a tree, we actually have 'n' focused windows to track:
one on each virtual workspace. Additionally, we need to track which
workspace is currently on screen -- yet another focus point.
One simplification though, is that rather than having a tree of
arbitrary depth, a window manager is a fixed height two level tree, with
a fixed 'n' branches from the top level.
All this suggests that we actually have a two-level zipper! Firstly, the top
level of the window manager tree, the StackSet type, is just a flat zipper, or
cursor, onto the focused workspace:
data StackSet a =
StackSet { current :: Workspace a
, prev :: [Workspace a]
, next :: [Workspace a] }
A workspace itself is just a numeric tag, and a stack of windows:
data Workspace a = Workspace { tag :: Int, stack :: Stack a }
Finally, a window stack on a workspace is a flat zipper giving us a
cursor onto the currently focused window, or the empty stack:
data Stack a = Empty
| Node { focus :: a
, left :: [a]
, right :: [a] }
Mmm... data structures are fun in Haskell. And we have a polymorphic
window manager to boot: the StackSet is polymorphic in the window type.
Note that our Stack and StackSet data types are really degenerate 1
level zippers, as they only provide operations to traverse left or
right. We have no need to move focus up or down a two level tree.
We can visualise the window manager implemented as a zipper-based
StackSet this way:
In this picture we have a window manager managing 6 virtual workspaces.
Workspace 4 is currently on screen. Workspaces 1, 2, 4 and 6 are
non-empty, and have some windows. The window currently receiving
keyboard focus is window 2 on the workspace 4. The focused windows on
the other non-empty workspaces are being tracked though, so when we view
another workspace, we will know which window to set focus on. Workspaces
3 and 5 are empty.
With this structure, rather than a set of tables, we have a natural
account of the behaviour of window focus during window manager
operations. From the picture alone, we can see how we can ensure
operations affect, for example, the current workspace only -- such
operations will affect only the current node of the workspace zipper.
It is also obvious how shifting window focus in the window manager
corresponds to shifting the cursor point on the current window zipper.
By using a data structure that tracks focus in this way, we hope to
avoid annoying book keeping code, leading to a simpler implementation of
our window manager, and, importantly, making it easier to ensure that
the implementation of our window manager matches the specified behaviour.
Keep it simple!
A zipper API for the window manager
Let's now consider a natural API for this data structure:
new :: Int -> StackSet a
peek :: StackSet a -> Maybe a
index :: StackSet a -> [a]
focusLeft, focusRight :: StackSet a -> StackSet a
insert :: a -> StackSet a -> StackSet a
delete :: -> StackSet a -> StackSet a
There are some additional operations we'd like to support, which operate
on the workspace level:
viewLeft, viewRight :: StackSet a -> StackSet a
shift :: Int -> StackSet a -> StackSet a
Now to implement this interface for our zipper-based StackSet.
A zipper implementation of a window manager
First, we can construct a new, empty window manager, with 'n'
workspaces, using a list comprehension to unfold the Empty workspace
list:
new :: Int -> StackSet a
new n | n > 0 = StackSet t [] rs
where
(t:rs) = [ Workspace i Empty | i <- [0 ..n1]]
The data structure requires us to state which workspace has initial
focus, so we pick the head of the list: Workspace 0. Good -- the more
policy that is obviously determined by the data structure, the less
thinking we have to do!
Extracting the currently focused window is requires us to find the
current workspace, then find the current window. We can use Haskell's
record access syntax for this:
peek s = case stack (current s) of
Empty -> Nothing
Node t _ _ -> Just t
However, since almost all operations are on the current workspace, we
can abstract out this access pattern into a higher order function --
'with' -- which will take a default value to return in case of 'Empty,
and a function to apply to a non-empty stack. It is like the function
'maybe' for Stacks, and can be written as:
with :: b -> (Stack a -> b) -> StackSet i a s -> b
with d f s = case stack (current s) of
Empty -> d
v -> f v
Yielding the much nicer:
peek :: StackSet a -> Maybe a
peek = with Nothing (return . focus)
The lesson here is to refactor and abstract repetitive logic, so you get
it right once, and then gain from simpler, more domain-specific code.
Higher-order functions forever!
We can implement 'index' with similar ease:
index :: StackSet i a s -> [a]
index = with [] $ \(Node t ls rs) -> reverse l ++ t : rs
Modifying the window manager
As we see, read-only access is easy. Modifying the window manager is
more interesting. For this we'll want to provide a 'modify' higher-order
function, similar to 'with', to abstract out the process of
replacing the current workspace with a modified version:
modify :: Stack a -> (Stack a -> Stack a) -> StackSet i a s -> StackSet i a s
modify d f s = s { current = (current s) { stack = with d f s } }
This just applies 'with' to the current workspace, and uses record
update syntax to replace the current workspace, returning a modified
StackSet. We can now implement the focus-changing functions. Firstly,
focusLeft and focusRight. Both shift focus to the window immediately to
the left or right of the cursor, or if we're at the end of the stack,
they wrap focus:
focusLeft, focusRight :: StackSet i a s -> StackSet i a s
focusLeft = modify Empty $ \c -> case c of
Node _ [] [] -> c
Node t (l:ls) rs -> Node l ls (t:rs)
Node t [] rs -> Node x xs [t] where (x:xs) = reverse rs
focusRight = modify Empty $ \c -> case c of
Node _ [] [] -> c
Node t ls (r:rs) -> Node r (t:ls) rs
Node t ls [] -> Node x [t] xs where (x:xs) = reverse ls
The implementation is straight forward, except for the wrapping case.
Indeed, all operations are O(1), except for when we wrap, which is O(w),
('w' is the number of windows on the screen). We see here how the
cursor-style data structure leads to a simple implementation of focus
shifting in a window manager, and helps us think more clearly about the
corner cases for focus movement. Pick the right data structures, and the
algorithms will be obvious!
We can implement insertLeft and insertRight, which insert a window to the left
or right of focus, and move focus there. The cases to consider for insert are:
- Inserting into an empty workspace, yields a workspace with a single focused window.
- Inserting into a non-empty workspace moves the current window to the left
or right, and sets focus to the inserted window.
Yielding the obvious implementation:
insertLeft, insertRight :: a -> StackSet i a s -> StackSet i a s
insertLeft a = modify (Node a [] []) $ \(Node t l r) -> Node a l (t:r)
insertRight a = modify (Node a [] []) $ \(Node t l r) -> Node a (t:l) r
Again, we get a policy for free stating where focus moves on insert,
avoiding tedious bookkeeping, and gaining strong assurances from the
simpler code. The data structure hints at the natural policy our window
manager should adopt.
We now consider how to delete the current window, and we will try to
specify precisely where window manager focus goes on delete. Remember:
tiling window managers need to have predictable behaviour, to be usable,
so the more behaviour we can precisely specify, the more predictable our
window manager will be.
There are four cases to consider:
- delete on an Empty workspace leaves it Empty;
- otherwise, try to move focus to the right;
- otherwise, try to move focus to the left;
- otherwise, a workspace with 1 element becomes Empty.
We implement this as:
delete :: StackSet a -> StackSet a
delete = modify Empty $ \c -> case c of
Node t ls (r:rs) -> Node r ls rs
Node t (l:ls) [] -> Node l ls []
Node _ [] [] -> Empty
And that's it. The code just follows from the spec, and the core window
manager's implementation, with correct focus behaviour, falls out of the
data structure.
Operations on workspaces
Navigating through virtual workspaces uses the level 1 zipper:
data StackSet a =
StackSet { current :: Workspace a
, prev :: [Workspace a]
, next :: [Workspace a] }
The implementation is obvious, and follows the 'focus' functions on stacks:
viewLeft :: StackSet a -> StackSet a
viewLeft (StackSet t (l:ls) rs) = StackSet l ls (t:rs)
viewLeft t = t
viewRight :: StackSet a -> StackSet a
viewRight (StackSet t ls (r:rs)) = StackSet r (t:ls) rs
viewRight t = t
The next, and hardest function to implement, is 'shift'. shift moves the
currently focused window to workspace 'n', leaving the current workspace
focused on a new window, and with a new window focused on workspace 'n'.
We can implement it as a little `script' using the primitives defined
already, by folding the sequence of operations over our StackSet. One
interesting point to note is that allowing indexing of workspaces
requires us to perform sanity checks on the index value. If 'shift' only
moved to the left or right workspaces, no bounds checking would be
needed. Local operations are more natural for zippers.
shift :: Int -> StackSet a -> StackSet a
shift new s
| new >= 0 && new < max_workspaces && new /= old = maybe s go (peek s)
| otherwise = s
where
old = tag (current s)
go w = foldl ($) s
[ delete
, view new
, insertLeft w
, view old ]
The 'go' script performs delete, view, insert, and view calls, and the
'view' function is a generalisation of viewLeft/viewRight to traverse to
an arbitrary workspace 'n'. To do this, it has to work out which
direction to travel, given the current workspace tag, and the desired
workspace:
view :: Int -> StackSet a -> StackSet a
view i s@(StackSet (Workspace n _) _ _)
| i >= 0 && i < max_workspaces = foldr traverse s [1.. abs (in)]
| otherwise = s
where
traverse _ = if signum (in) >= 0 then viewRight else viewLeft
And that's it. Let's now look at using QuickCheck to ensure we have the
implementation right, and that our API makes sense.
QuickCheck Your Window Manager
The first thing to check is that the data invariants of the StackSet
type hold for arbitrary StackSets QuickCheck generates. For the data
structure we have defined, we no longer need to check for focus being
valid -- the data structure won't let us focus on a window not on the
current workspace! However there is one property not ensured directly by
the data structure: uniqueness. It is required that no window appear more
than once in the window manager. We can check that operations don't
violate this rule with the following property:
type T = StackSet Char
invariant (x :: T) = nub ws == ws
where
ws = [ focus t : left t ++ right t
| w <- current s : prev s ++ next s
, let t = stack w, t /= Empty ]
Now we can check each operation on StackSets preserves this invariant:
prop_new (n :: Positive Int) =
invariant $ new (fromIntegral n)
prop_focusLeft (n :: NonNegative Int) (x :: T) =
invariant $ foldr (const focusLeft) x [1..n]
prop_insertLeft n (x :: T) =
invariant $ insertLeft n x
prop_delete (x :: T) =
invariant $ maybe x (\i -> delete i x) (peek x)
And so forth. Everything looks good so far:
$ runhaskell tests/Properties.hs
new: invariant : OK, 100 tests.
focusLeft: invariant : OK, 100 tests.
insertLeft: invariant : OK, 100 tests.
delete: invariant : OK, 100 tests.
Higher level properties
Rather than go through the basic properties tested in the last article,
let's now look at stronger properties. In particular, we will check that
particular operations are 'local' to the area of the data structure they
work on -- that they do not change parts of the StackSet (and thus the
screen!) they shouldn't, and secondly, we will check particular policies
regarding the movement of focus in the window manager.
A simple property to check is that moving focus on the current virtual
workspace never touches the hidden workspaces. It is purely local to the
workspace in focus:
prop_focus_local (x :: T) = hidden (focusRight x) == hidden x
This says that the hidden workspaces are entirely unchanged by the
movement of window focus on the current workspace. 'hidden' is
straightforward:
hidden (x :: T) = [ w | w <- prev x ++ next x ]
Similarly, insert and delete should be local. They should not change anything
other than the current workspace:
prop_insert_local (x :: T) i = hidden x == hidden (insertLeft i x)
prop_delete_local (x :: T) = hidden x == hidden (delete x)
And QuickCheck agrees with us. Good! We are starting to build up some
confidence that our window manager model behaves the way a window
manager should.
Another interesting property to check is that shifting focus is
reversible. That is, if you move focus to the left window, you can move
it back again by moving focus to the right. The obvious implementation
is:
prop_focus_right (x :: T) = focusRight (focusLeft x) == x
However, if we run this, we find:
focus right/left : Falsifiable after 0 tests:
StackSet { current = Workspace { tag = 0, stack = Node { focus = 'n'
, left = []
, right = "d"} }
, prev = []
, next = [ Workspace { tag = 1, stack = Empty }
, Workspace { tag = 2, stack = Node { focus = 'e'
, left = ""
, right = "" } } ] }
What happened? If we look at the current workspace, we see that it has
no windows to the left of the currently focused element: "left = []",
which means
that focusLeft will cause a wrapping, which rests the distribution of
windows to the right of the focused element. So while a window
distribution with left, focused and right of:
[] 'n' ['d']
and:
['d'] 'n' []
will have the same window ordering modulo wrapping behaviour of focus,
they do not compare as equal when tested by QuickCheck. We thus need to
first normalise the window distribution. We choose to be right-biased
here:
normal = modify Empty $ \c -> case c of
Node t ls rs -> Node t [] (rs ++ reverse ls)
Which yields the property:
prop_focus_right (x :: T) = normal (focusRight (focusLeft x)) == normal x
Which does indeed hold.
Testing where focus goes
Finally, we can check that inserting and deleting a window leaves us with the
original StackSet unmodified, including where focus is set:
prop_insert_delete n (x :: T) = delete n (insertLeft n x) == x
prop_delete_insert (x :: T) =
case peek x of
Nothing -> True
Just n -> insertLeft n (delete x) == x
And QuickCheck again confirms this:
insert is reversible : OK, 100 tests.
delete is reversible : OK, 100 tests.
Wonderful! Having a data structure that tracks focus automatically gives us
simple, clean semantics for the behaviour of focus when windows pop up and are
deleted. In fact, all our properties are now able to assert the behaviour of
focus will be unchanged, or will be changed in precisely specified ways, as
equality on StackSets now means equality on workspaces, including focus. This
is exactly what we require for an elegant and predictable implementation of a
tiling window manager.
Conclusion
By moving more information into our pure data structure, we are able to
make stronger statements about the behaviour of our code, on that
information. By using a purely functional data structure, and
QuickCheck, we can encode these statements as QuickCheck properties, and
have them tested automatically. Finally, by using a data structure
which more closely models the domain we're looking at, the
implementation becomes simpler, cleaner and more obviously correct, and
with a strong, statically typed data structure, we get behaviour for
free that previously required dynamic checking. The data type described
here is the core of a branch of the xmonad window manager.
The zipper version of xmonad is running on my laptop as I write, and
plans are to merge it into the main xmonad branch soon. Perhaps the
most interesting result is that xmonad is now 50 lines shorter! By
moving more logic (explicit focus handling) into the pure StackSet data
structure, most of the event handling code is now just a shallow wrapper
over the StackSet api. Smarter data structures, less code. It's all good!
Thanks goes to Wouter Swiestra for the original idea of using a zipper
to implement focus-tracking in the xmonad, and to Spencer Janssen, Jason
Creighton and David Roundy for several discussions about the subtleties
of focus behaviour.
For further information on the lovely zipper data type, see:
/home ::
/haskell ::
permalink ::
rss
2007-05-01
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,
stacks :: Map Int [a]
} 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.
empty :: Int -> StackSet a
peek :: StackSet a -> Maybe a
push :: a -> StackSet a -> StackSet a
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:
rotate :: Direction -> StackSet a -> StackSet a
view :: Int -> StackSet a -> StackSet a
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:
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..n1] (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:
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)
n <- choose (0,sz1)
ls <- vector sz
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:
prop_empty n = n > 0 ==> all null (M.elems (stacks x))
where x = empty n :: T
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:
prop_view_idem (x :: T) r =
let i = fromIntegral $ r `mod` sz
sz = size x
in view i (view i x) == (view i x)
prop_delete_idem i (x :: T) = delete i x == delete i (delete i x)
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
m = fromIntegral $ r `mod` (size x)
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.
/home ::
/haskell ::
permalink ::
rss