exhaustive-1.1.8: Compile time checks that a computation considers producing data through all possible constructors

Control.Exhaustive

Description

exhaustive is a library that guarantees that when building a parser, or some other computation that produces data, all possible constructors in a data type are considered. You can think of this library as providing a symmetry to GHC's built in -fwarn-incomplete-patterns compile time warning, although this library is stricter in that it produces compile time errors if a constructor is omitted.

Usage of this library is intended to be straightforward, though admittedly the types might have you think the opposite! To understand this library, an example may be helpful.

To begin with, consider a simple data type for a "boolean expressions" language:

import qualified GHC.Generics as GHC

data Expr
= ETrue
| EFalse
| EIf Expr Expr Expr
deriving (Eq, GHC.Generic)
instance Generic Expr

Note that we have to make our data type an instance of both GHC.Generics.Generic and Generics.SOP.Generic, though this only requires boiler-plate code.

Next, we would like to build a parser for this language. Let's assume that we have access to a parsec-like library, where we have one basic combinator:

Ordinarily, we would write our parser as

parseExpr :: Parser Expr
parseExpr = msum [ETrue <$symbol "True" ,EFalse <$ symbol "False"
,EIf <$> symbol "if" *> parseExpr <*> symbol "then" *> parseExpr <*> symbol "else" *> parseExpr ] However, nothing is making sure that we actually considered all constructors in Expr. We could just as well write parseExpr :: Parser Expr parseExpr = msum [ETrue <$ symbol "True"
,EFalse <$symbol "False"] Although this is significantly less useful! Using exhaustive, we can get exhaustivity checks that we are at least considering all constructors: makeExhaustive ''Expr parseExpr :: Parser Expr parseExpr = produceFirst$
$(con 'ETrue) <$ symbol "True" &:
$(con 'EFalse) <$ symbol "False" &:
$(con 'EIf) <$> (symbol "if" *> parseExpr)
<*> (symbol "then" *> parseExpr)
<*> (symbol "else" *> parseExpr) &:
finish

As you can hopefully see, exhaustive requires only minimal changes to an existing parser. Specifically, we need to:

1. Use produceFirst instead of msum
2. Wrap each constructor application with the Template Haskell function con. Note that you also need to quote the name of the constructor with a single '.
3. Use &: to combine constructors, rather than list notation.
4. Explicitly state you are finished.
5. Add a call to makeExhaustive on our original data type.
Synopsis

# Specifying Individual Constructions

con builds a Construction for a single constructor of a data type. Unfortunately, as this function is used via Template Haskell, the type is not particularly informative -- though you can think of the produced function having roughly the same type as the original constructor. To clarify this, it's helpful to look at the type of con applications:

$(con 'Nothing) :: Construction 1 '[]$(con 'Just) :: a -> Construction 2 '[a]

data Record = Record { a :: String, b :: Int, c :: Char }

# Implementation details

The following are implementation details, but exported to improve documentation.

type ConstructorApplication f code = Injection (NP I) code -.-> K (f (NS (NP I) code)) Source #

A ConstructorApplication is a lifted function (in the terms of generics-sop) that instantiates a particular constructor of a data type, possibly using the side-effects provided by f.

To create and use ConstructorApplications, use &:.

data Construction :: Nat -> [*] -> * Source #

A Construction is an internal representation of a data type constructor. This type is indexed by a natural number, which represents the constructor number, and the list of types of fields of this constructor.

To create a Construction, use con.

type family Length (a :: [k]) :: Nat where ... Source #

Compute the length of a type level list.

Equations

 Length '[] = 0 Length (x ': xs) = 1 + Length xs