[xmonad] Compile-time verification of keymaps

[Gwern Branwen]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

So today I edited into my xmonad.hs a binding to the Isohunt.com
XMonad.Actions.Search engine for convenience. I naturally chose xK_i
for the bound key. When I reloaded, I was surprised to see that mod-i
failed to do as it was supposed to.

Trying it again, it brought up irssi. That was when I realized mod-i
had already been bound in my xmonad.hs, to runOrRaise for irssi, and
that the irssi binding happened to be later in the list and so it
quietly overwrote the Isohunt binding. After picking a new & unused
key, I began reflecting on this.

Certainly, this is expected behavior if you're familiar with Data.Map.
fromList will do that - a list may have multiple values for a single
key (such as xK_i) and the last value wins. But I think in an
xmonad.hs, the context is somewhat different. There the semantics are
somewhat different. We use 'M.fromList [stuff, more stuff, and the
rest]' syntax because Haskell supports list syntax, and it makes life
easier on the user to use such a common method.

But do we *really* mean to say that it is a sensible thing to bind the
same key to multiple contradictory definitions? It just so happens
that [xK_i isohunt, xK_i irssi] is equivalent to a destructive update
style of 'i = isohunt; i = irssi' when fed through the Map functions.

So I thought to myself that maybe there was some static way of
specifying a list without duplicates we could use in xmonad.hs. It
would be nice to know that one cannot run xmonad.hs with inconsistent
sets of bindings*. This checking would, even better, be done at
compile-time so one could verify this by simply loading in GHCi (good
for everyone who routinely reloads in Emacs or Vim).

How to do this? Someone in #haskell suggested extensible records, but
that sounds quite difficult. Another approach would be to scrap the
static requirement, and simply provide the user a redefined 'fromList'
which runs something like 'let x = map fst list in nub x == x' and
does something if there are duplicates (calls error, spawns xmessage,
etc.)

I decided to try a variant of the latter at compile-time, using
Template Haskell. I got fairly far with the help of mmorrow, but I
didn't actually succeed.

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)

iEYEAREKAAYFAkkgYvgACgkQvpDo5Pfl1oLE3gCgkuHMlUO1+YT4oEFLzhHqmeuB
QA4An3X72j1z+StumSOmnTXlTJhHeTft
=fBDz
-----END PGP SIGNATURE-----

The idea is that one should be able to do something like this in xmonad.hs
> '{-# LANGUAGE TemplateHaskell #-}
> import XMonad.Utils.VerifyKeys
> ....
> myKeys conf@(XConfig {modMask = m}) = M.fromList $(uniqueTupleListQ [ -- rebind standard actions
>             ((m .|. shiftMask,xK_p), shellPrompt greenXPConfig)
>           , ((m,              xK_d), raiseBrowser) ] )

VerifyKeys looks something like this:

> {-# LANGUAGE TemplateHaskell #-}
> module XMonad.Utils.VerifyKeys where
>
> import Data.List(nub)
> import qualified Data.Map
> import Language.Haskell.TH.Lib
> import Language.Haskell.TH.Syntax
>
> uniqueTupleListQ :: (Eq a, Lift a, Lift b) => [(a, b)] -> ExpQ
> uniqueTupleListQ xs = let ys = map fst xs
>                      ns = nub ys
>                   in case ys == ns of
>                       False -> fail "uniqueTupleListQ: List has conflicting entries."
>                       True  -> lift xs

The idea is that since we know the keymap at compile-time, we pass it,
before it gets turned into a Map (and the relevant information lost),
we analyze the list. 'fail' aborts the compilation if the list is bad.
You can easily test this out in a different module with some simple
expressions:

> keymap1, keymap2 :: [(Char, String)]
> keymap1 = $(uniqueTupleListQ [('a', "foo"), ('b', "bar")] )
> keymap2 = $(uniqueTupleListQ [('a', "foo"), ('b', "bar"), ('c', "bar"), ('a', "quux")] )

Compiling, this gives us something like this:

> [1 of 2] Compiling Tmp              ( Tmp.hs, Tmp.o )
> [2 of 2] Compiling Main             ( xmonad.hs, xmonad.o )
> Loading package base ... linking ... done.
> Loading package array-0.1.0.0 ... linking ... done.
> Loading package packedstring-0.1.0.0 ... linking ... done.
> Loading package containers-0.1.0.1 ... linking ... done.
> Loading package pretty-1.0.0.0 ... linking ... done.
> Loading package template-haskell ... linking ... done.
>
> xmonad.hs:113:12: uniqueTupleListQ: List has conflicting entries.

Line 133 is keymap2. If we remove '('a', "quux")', which conflicts
with the very first entry, we get:

> [1 of 2] Compiling Tmp              ( Tmp.hs, Tmp.o )
> [2 of 2] Compiling Main             ( xmonad.hs, xmonad.o )
> Loading package base ... linking ... done.
> Loading package array-0.1.0.0 ... linking ... done.
> Loading package packedstring-0.1.0.0 ... linking ... done.
> Loading package containers-0.1.0.1 ... linking ... done.
> Loading package pretty-1.0.0.0 ... linking ... done.
> Loading package template-haskell ... linking ... done.
> Linking foo ...

Now, this seems to be exactly what we want, doesn't it? But ultimately
I had to admit failure. Template Haskell has a number of restrictions
and omissions that make it unfeasible to use.

For starters: If we apply uniqueTupleList to an actual keymap (like
mine), we discover that uniqueTupleList's constraints are unworkable.
Per the type sig, we need 'Lift b', the second half of each tuple in
the key list. But XMonad requires b to be a X (), and X () is not
instantiated for Lift**. Were it, we would still need Lift instances
for Word64 and also CUInt.

Lift instances probably wouldn't be too hard to write. The real
killer, from an xmonad.hs perspective, is the module restrictions.
Fundamentally, one *cannot* use inside a $() anything defined in the
same file. {modMask = m}? Nope. greenXPConfig? Nope. 'term =
XMonad.terminal conf'? Nope. And so on. It is a minimal set of
bindings indeed which only makes use of literals and imported
functions.

So until Template Haskell improves, that avenue seems to be out.

I'm not sure where to go from here. Had Template Haskell worked out,
the path would've been easy, a matter of having users make a
relatively small modification to their xmonad.hs, and perhaps avoiding
entirely TH syntax.

Does anyone have a better approach, or is this a foolish thing to want
static safety in? ksf suggested that Yi has a combinator approach to
keybindings which could solve it, but I am unsure how that works or
could be adapted for XMonad.***

* Obviously the consistency is only valuable _in_ a specific Map; if
we insisted that all Maps be consistent, then we couldn't override the
default Map with our own.
** I may be misinterpreting the type error; possibly we actually need
Lift for (X())
*** I'm cc'ing yi-devel since I suspect the topic may be of interest.

--
gwern