Data.Eliminator.TH

One bullet point of #1

CHANGELOG.md

@@ -1,4 +1,8 @@
 ## next [????.??.??]
+* Introduce the `Data.Eliminator.TH` module, which provides functionality for
+  generating eliminator functions using Template Haskell. Currently, only
+  simple algebraic data types that do not use polymorphic recursion are
+  supported.
 * All eliminators now use predicates with `(~>)`.
 
 ## 0.1 [2017-07-02]

eliminators.cabal

@@ -24,8 +24,13 @@ source-repository head
 
 library
   exposed-modules:     Data.Eliminator
-  build-depends:       base       >= 4.10 && < 4.11
-                     , singletons >= 2.3  && < 2.4
+                       Data.Eliminator.TH
+  build-depends:       base             >= 4.10  && < 4.11
+                     , extra            >= 1.4.2 && < 1.7
+                     , singletons       >= 2.3   && < 2.4
+                     , template-haskell >= 2.12  && < 2.13
+                     , th-abstraction   >= 0.2.3 && < 0.3
+                     , th-desugar       >= 1.7   && < 1.8
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall -Wno-unticked-promoted-constructors

src/Data/Eliminator.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -38,6 +39,9 @@ module Data.Eliminator (
   , elimTuple7
   ) where
 
+import           Control.Monad.Extra
+
+import           Data.Eliminator.TH
 import           Data.Kind (Type)
 import           Data.List.NonEmpty (NonEmpty(..))
 import           Data.Singletons.Prelude
@@ -46,6 +50,8 @@ import           Data.Singletons.TypeLits
 
 import qualified GHC.TypeLits as TL
 
+import           Language.Haskell.TH.Desugar (tupleNameDegree_maybe)
+
 import           Unsafe.Coerce (unsafeCoerce)
 
 {- $eliminators
@@ -58,43 +64,19 @@ and as a result, the predicates must be applied manually with '(@@)'.
 The naming conventions are:
 
 * If the datatype has an alphanumeric name, its eliminator will have that name
-  with @elim-@ prepended.
+  with @elim@ prepended.
 
 * If the datatype has a symbolic name, its eliminator will have that name
   with @~>@ prepended.
 -}
 
-elimBool :: forall (p :: Bool ~> Type) (b :: Bool).
-            Sing b
-         -> p @@ False
-         -> p @@ True
-         -> p @@ b
-elimBool SFalse pF _  = pF
-elimBool STrue  _  pT = pT
-
-elimEither :: forall (a :: Type) (b :: Type) (p :: Either a b ~> Type) (e :: Either a b).
-              Sing e
-           -> (forall (l :: a). Sing l -> p @@ (Left  l))
-           -> (forall (r :: b). Sing r -> p @@ (Right r))
-           -> p @@ e
-elimEither (SLeft  sl) pLeft _  = pLeft  sl
-elimEither (SRight sr) _ pRight = pRight sr
-
-elimList :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
-            Sing l
-         -> p @@ '[]
-         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
-         -> p @@ l
-elimList SNil                      pNil _     = pNil
-elimList (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimList @a @p @xs xs pNil pCons)
+$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''NonEmpty, ''Ordering])
+$(deriveElimNamed "elimList" ''[])
+$(concatMapM (\n -> let Just deg = tupleNameDegree_maybe n
+                    in deriveElimNamed ("elimTuple" ++ show deg) n)
+             [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])
 
-elimMaybe :: forall (a :: Type) (p :: Maybe a ~> Type) (m :: Maybe a).
-             Sing m
-          -> p @@ Nothing
-          -> (forall (x :: a). Sing x -> p @@ (Just x))
-          -> p @@ m
-elimMaybe SNothing pNothing _ = pNothing
-elimMaybe (SJust sx) _ pJust  = pJust sx
+-- This is the grimy one we can't define using Template Haskell.
 
 -- | Although 'Nat' is not actually an inductive data type in GHC, we can
 -- pretend that it is using this eliminator.
@@ -108,79 +90,3 @@ elimNat snat pZ pS =
     0        -> unsafeCoerce pZ
     nPlusOne -> withSomeSing (pred nPlusOne) $ \(sn :: Sing k) ->
                   unsafeCoerce (pS sn (elimNat @p @k sn pZ pS))
-
-elimNonEmpty :: forall (a :: Type) (p :: NonEmpty a ~> Type) (n :: NonEmpty a).
-                Sing n
-             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ (x :| xs))
-             -> p @@ n
-elimNonEmpty (sx :%| sxs) pNECons = pNECons sx sxs
-
-elimOrdering :: forall (p :: Ordering ~> Type) (o :: Ordering).
-                Sing o
-             -> p @@ LT
-             -> p @@ EQ
-             -> p @@ GT
-             -> p @@ o
-elimOrdering SLT pLT _   _   = pLT
-elimOrdering SEQ _   pEQ _   = pEQ
-elimOrdering SGT _   _   pGT = pGT
-
-elimTuple0 :: forall (p :: () ~> Type) (u :: ()).
-              Sing u
-           -> p @@ '()
-           -> p @@ u
-elimTuple0 STuple0 pTuple0 = pTuple0
-
-elimTuple2 :: forall (a :: Type) (b :: Type)
-                     (p :: (a, b) ~> Type) (t :: (a, b)).
-              Sing t
-           -> (forall (aa :: a) (bb :: b).
-                      Sing aa -> Sing bb
-                   -> p @@ '(aa, bb))
-           -> p @@ t
-elimTuple2 (STuple2 sa sb) pTuple2 = pTuple2 sa sb
-
-elimTuple3 :: forall (a :: Type) (b :: Type) (c :: Type)
-                     (p :: (a, b, c) ~> Type) (t :: (a, b, c)).
-              Sing t
-           -> (forall (aa :: a) (bb :: b) (cc :: c).
-                      Sing aa -> Sing bb -> Sing cc
-                   -> p @@ '(aa, bb, cc))
-           -> p @@ t
-elimTuple3 (STuple3 sa sb sc) pTuple3 = pTuple3 sa sb sc
-
-elimTuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type)
-                     (p :: (a, b, c, d) ~> Type) (t :: (a, b, c, d)).
-              Sing t
-           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d).
-                      Sing aa -> Sing bb -> Sing cc -> Sing dd
-                   -> p @@ '(aa, bb, cc, dd))
-           -> p @@ t
-elimTuple4 (STuple4 sa sb sc sd) pTuple4 = pTuple4 sa sb sc sd
-
-elimTuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type)
-                     (p :: (a, b, c, d, e) ~> Type) (t :: (a, b, c, d, e)).
-              Sing t
-           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e).
-                      Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee
-                   -> p @@ '(aa, bb, cc, dd, ee))
-           -> p @@ t
-elimTuple5 (STuple5 sa sb sc sd se) pTuple5 = pTuple5 sa sb sc sd se
-
-elimTuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type)
-                     (p :: (a, b, c, d, e, f) ~> Type) (t :: (a, b, c, d, e, f)).
-              Sing t
-           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f).
-                      Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff
-                   -> p @@ '(aa, bb, cc, dd, ee, ff))
-           -> p @@ t
-elimTuple6 (STuple6 sa sb sc sd se sf) pTuple6 = pTuple6 sa sb sc sd se sf
-
-elimTuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type)
-                     (p :: (a, b, c, d, e, f, g) ~> Type) (t :: (a, b, c, d, e, f, g)).
-              Sing t
-           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g).
-                      Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg
-                   -> p @@ '(aa, bb, cc, dd, ee, ff, gg))
-           -> p @@ t
-elimTuple7 (STuple7 sa sb sc sd se sf sg) pTuple7 = pTuple7 sa sb sc sd se sf sg