Skip to content

Instantly share code, notes, and snippets.

@chrisdone chrisdone/0README.md
Last active Feb 6, 2019

Embed
What would you like to do?
Onto syntax for exhaustive construction of a data type

Motivation

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 Exp?

Solution

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 App. The Alternative class's (<|>) 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 App line, 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.

Naming

The name comes from the "onto mapping", i.e.

∀y ∈ B,∃x ∈ A,f(x) = y

the function f has an output for every element of set B, mapped from some value in set A.

{-
Expansion is:
onto-demo.hs:(21,5)-(23,49): Splicing expression
onto
[| do [Num i_agJM | i_agJM <- read . (: []) <$> digit]
[App f_agJN x_agJO | f_agJN <- alphaNum, x_agJO <- expr] |]
======>
((GHC.Base.<|>)
(do i_agLg <- ((read . (GHC.Types.: [])) <$> digit)
pure (Num i_agLg)))
(do f_agLh <- alphaNum
x_agLi <- expr
pure ((App f_agLh) x_agLi))
-}
{-# LANGUAGE TemplateHaskell #-}
import Text.Parsec
import Text.Parsec.String
import Onto
import Exp
expr :: Parser Exp
expr =
$(onto
[|do [Num i | i <- read . (: []) <$> digit]
[App f x | f <- alphaNum, x <- expr]|])
module Exp where
data Exp = Num Int | App Char Exp
deriving (Show)
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}
module Onto where
import Control.Applicative
import Control.Monad
import Data.List
import Language.Haskell.TH
import Language.Haskell.TH.Ppr
onto :: Q Exp -> Q Exp
onto getE = do
e <- getE
case e of
DoE stmts -> do
cases <- mapM getCase stmts
case cases of
[] -> error "No cases."
(x:xs) -> do
info <- reify (caseConstructor x)
case info of
DataConI _ _ ty -> do
tyinfo <- reify ty
case tyinfo of
TyConI (DataD _cxt _n _tvs _mk cons _derivs) ->
let getConses =
\case
NormalC name _ -> [name]
RecC name _ -> [name]
InfixC _ name _ -> [name]
ForallC _ _ con -> getConses con
GadtC names _ _ -> names
RecGadtC names _ _ -> names
conses = concatMap getConses cons
in do case filter
(\cons ->
not
(elem cons (map caseConstructor (x : xs))))
conses of
[] -> pure ()
missing ->
reportWarning
("The following cases have not been covered: " ++
intercalate ", " (map pprint missing))
pure
(foldl
(\acc x ->
AppE (AppE (VarE '(<|>)) acc) (caseToExp x))
(caseToExp x)
xs)
_ -> error "Should be an ADT."
_ ->
error
("Invalid or unknown data constructor " ++
show (caseConstructor x))
_ -> error "Case list should be of the form: do c1; c2; c3"
data Case =
Case
{ caseConstructor :: Name
, caseSlots :: [Exp]
, caseStmts :: [Stmt]
}
caseToExp :: Case -> Exp
caseToExp c =
DoE
(caseStmts c ++
[NoBindS (AppE (VarE 'pure) (foldl AppE (ConE (caseConstructor c)) (caseSlots c)))])
getCase :: Stmt -> Q Case
getCase =
\case
NoBindS e ->
case e of
CompE stmts ->
case reverse stmts of
(NoBindS consE:(reverse -> binds)) -> do
(cons, slots) <-
case consE of
ConE name -> pure (name, [])
AppE {} -> pure (flattenApplication consE)
stmts <-
mapM
(\case
ParS _ -> error "Parallel binds not supported."
x -> pure x)
binds
pure
(Case
{ caseConstructor = cons
, caseSlots = slots
, caseStmts = stmts
})
_ -> error "The case should begin with the form [Cons e1 e2 ... ]"
_ ->
error "Each case should be of the form [Cons e1 e2 | stmt1, stmt2, ... ]"
flattenApplication
:: Exp -> (Name,[Exp])
flattenApplication = go []
where go args (AppE f x) = go (x : args) f
go args (ConE n) = (n,args)
go args _ = error "Expected constructor in case e.g. Just x"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.