Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
) instanceGeneric
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:
- Use
produceFirst
instead ofmsum
- 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'
. - Use
&:
to combine constructors, rather than list notation. - Explicitly state you are
finish
ed. - Add a call to
makeExhaustive
on our original data type.
- con :: Name -> Q Exp
- (&:) :: (Functor f, Length code ~ (n + Length xs)) => f (Construction n x) -> NP (ConstructorApplication f code) xs -> NP (ConstructorApplication f code) (x ': xs)
- finish :: NP f '[]
- produceM :: (code ~ Code a, Generic a, Applicative f) => NP (ConstructorApplication f code) code -> [f a]
- produceFirst :: (code ~ Code a, Generic a, Alternative f) => NP (ConstructorApplication f code) code -> f a
- produceAll :: (code ~ Code a, Generic a, Alternative f) => NP (ConstructorApplication f code) code -> f [a]
- makeExhaustive :: Name -> Q [a]
- type ConstructorApplication f code = Injection (NP I) code -.-> K (f (NS (NP I) code))
- data Construction :: Nat -> [*] -> *
- type family Length (a :: [k]) :: Nat where ...
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 } $(con
'Record) :: String -> Int -> Char -> Construction 1 '[String, Int, Char]
For more examples of con
, see the module documentation at the top of this page.
Combining Constructions
(&:) :: (Functor f, Length code ~ (n + Length xs)) => f (Construction n x) -> NP (ConstructorApplication f code) xs -> NP (ConstructorApplication f code) (x ': xs) infixr 3 Source #
Combine multiple Construction
s into a list of constructions for a data
type. This function is a lot like :
for lists, but the types carry
considerably more information.
The type n
is used to carry the index of the constructor in the list of
constructors in the data type, while xs
is a list of types that are the
fields of that constructor.
The constraint on this function forces &:
to be used to produce in-order
constructors. It may help to see this function through an example:
Given data Bool = True | False
, we have two constructors. True
has index
1, while the code for this data type has length 2 (as there are two
constructors in total). Therefore after using the True
constructor we have to
use one more constructor. When we construct using False
we are done, as the
only way to satisfy the equation 2 + x = 2
is to provide x = 0
-- the empty
list.
Assert that you have now used all constructors and are finished. If you've made mistake, be prepared for a rather impressive type error!
Producing Data
produceM :: (code ~ Code a, Generic a, Applicative f) => NP (ConstructorApplication f code) code -> [f a] Source #
Build a list of computations, one for each constructor in a data type.
produceFirst :: (code ~ Code a, Generic a, Alternative f) => NP (ConstructorApplication f code) code -> f a Source #
Keep attempting to construct a data type until a constructor succeeds. The
first constructor to successfully be constructed (in the order defined in the
original data type) will be returned, or empty
if all constructions fail.
produceAll :: (code ~ Code a, Generic a, Alternative f) => NP (ConstructorApplication f code) code -> f [a] Source #
Produce all successful constructions of a data-type. If any constructors
fail, they will not be included in the resulting list. If all constructors
fail, this will return pure
[]
.
Utilities
makeExhaustive :: Name -> Q [a] Source #
Signify that you will be performing exhaustive construction of a specific data type:
data Expr = ETrue | EFalse makeExhaustive ''Expr
makeExhaustive
doesn't introduce any new symbols into scope, but it forces an
environment change, allowing you to write $(con 'ETrue)
. If you are already using
other Template Haskell routines (such as makeLenses
) then you can omit this call.
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 ConstructorApplication
s, 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
.