Onto syntax for exhaustive construction of a data type

0README.md

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.

demo.hs

{-

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]|])

Exp.hs

module Exp where
data Exp = Num Int | App Char Exp
  deriving (Show)

Onto.hs

{-# 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"