Surjective

Documentation

type Covers a = (a -> a) -> a

When the function given to surjective returns a value, it should call a covers function specifying a pattern. This pattern represents the subset of values which are considered "covered" by this case, so we can then make sure that all the values in the codomain are covered.

This covers function needs to take a pattern and a value (the value being returned), so we would like to write:

covers {pattern} {value}

But unfortunately, patterns are not first-class in Haskell. So instead we write:

covers $ \{pattern} -> {value}

And we use TemplateHaskell to replace that call with {value}. So covers appears to have type (a -> a) -> a.

surjective :: Q (TExp (Covers a -> b)) -> Q (TExp b)

Assert that an expression of type b covers all the values of type a. Typically, b is a function of the form ... -> a, so we are asserting that the function is "surjective", meaning that for every value in its ouput type, there is a combination of input values which will produce it. The idea is that if you add a new constructor to a data type, the compiler should warn you that your parser no longer cover all the outputs, in the same way that -Wincomplete-patterns warns you that your pretty-printer no longer cover all the inputs.

Here is a parsing function which is missing a case:

parseBool :: String -> Maybe Bool
parseBool = \case
  "true" -> Just True
  _      -> Nothing

And here is how to annotate the function using surjective so the compiler warns us about that missing case:

-- Warning: Pattern match(es) are non-exhaustive
-- In a case alternative: Patterns not matched: (Just False)
parseBool :: String -> Maybe Bool
parseBool = $$(surjective
  [||\covers -> \case
    "true" -> covers $ \(Just True) -> Just True
    _      -> covers $ \Nothing     -> Nothing
  ||])

That is, to check that an expression is surjective:

1. Pick a name, typically "covers", for the function which asserts that a particular pattern is covered.
2. For each output expression, choose the pattern which this output is considered to cover.
3. This is the weird part: wrap the output expression in a lambda and use the pattern in the binding position. Don't worry about partiality, this is just a syntactic trick to associate the pattern to the output expression. This will be rewritten to just the output expression.
4. Wrap your entire implementation in another lambda, using the name you picked for covers in the binding position. This is another syntactic trick, that lambda will be eliminated as well.
5. Wrap that lambda in a typed quotation [|| ... ||]. Make sure the TemplateHaskell language extension is enabled or you'll get a parse error.
6. Call surjective on the typed quotation, and splice the result back into your program using $$( ... ). The spliced-in code will contain an unused case expression covering all the patterns given to covers, so we will get a -Wincomplete-patterns warning if we forgot a case.

Since the transformation is entirely syntactic, surjective can be used to check other kinds of coverage conditions, not just surjectivity. For example, here we attempt to list all the values of type Maybe Bool, but we are missing a case:

listMaybeBools :: [Maybe Bool]
listMaybeBools = [Just True, Nothing]

Here is how to annotate the list using surjective so the compiler warns us about that missing case:

-- Warning: Pattern match(es) are non-exhaustive
-- In a case alternative: Patterns not matched: (Just False)
listMaybeBools :: [Maybe Bool]
listMaybeBools = $$(surjective
  [||\covers -> [ covers $ \(Just True) -> Just True
                , covers $ \Nothing     -> Nothing
                ]
  ||])