[Xmonad] statically checked non-empty layout lists

4 May 2007

      The new layout code introduces more chances for runtime errors than I'd
like. In particular, the Dynamic type, and the possibility of users
defining empty layout lists. 

Here's a cute approach, purely for instructive purposes, on statically
checked non empty layout lists for Config.hs:

Given a GADT for non-empty lists:

    data Empty
    data NonEmpty

    data List x y where
         Nil  :: List Empty x
         Cons :: x -> List y x  -> List NonEmpty x

    toList :: List t a -> [a]
    toList Nil          = []
    toList (Cons x y)   = x : toList y

    infixr 5 .:.
    (.:.) :: x -> List t x -> List NonEmpty x
    (.:.) = Cons

We can constrain:

    defaultLayouts :: List NonEmpty Layout

meaning that this becomes a statically checked error:

    defaultLayouts = Nil

resulting in:

    Config.hs:138:17:
        Couldn't match expected type `NonEmpty'
               against inferred type `Empty'
         Expected type: List NonEmpty Layout
         Inferred type: List Empty    Layout

While this is fine:

    defaultLayouts :: List NonEmpty Layout
    defaultLayouts = full .:. tall defaultDelta (1%2) .:. Nil

Cute huh?

-- Don

[Xmonad] statically checked non-empty layout lists

dons＠cse.unsw.edu.au