Instantly share code, notes, and snippets. chrisdone/0README.md Last active Feb 6, 2019

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"