For an ADT type, such as,
data Exp = Num Int | App Char Exp deriving (Show)
In Haskell we have case expressions to deconstruct values, and they have exhaustiveness checking. We have
case e of Num i -> ..
and then GHC can warn us that we forgot the
App case. Well what about the opposite, to have exhaustiveness checking when we're constructing values of type
This gist demonstrates a simple syntactic extension to achieve this. Here it is. We can write out a way to construct the type, case-by-case:
expr = $(onto [| do [Num i | i <- read . (: ) <$> digit] [App f x | f <- alphaNum, x <- expr] |])
Meaning, to construct the
Num i expression, draw
i from the monadic action. If that case fails, try the next one
(<|>) is used for this alternating.
This parser works as expected:
> parse expr "" "fg1" Right (App 'f' (App 'g' (Num 1)))
Now here's the good bit, if we comment out or forget the
or we add a new constructor to our data type, we get:
onto-demo.hs:19:5: warning: The following cases have not been covered: Exp.App
This template haskell extension could be made into a GHC source plugin, or added to GHC as an extension.
The abuse of the
do-notation is coincidental. Some other syntax could be used.
The name comes from the "onto mapping", i.e.
∀y ∈ B,∃x ∈ A,f(x) = y
f has an output for every element of set B, mapped from some value in set A.