diff --git a/CHANGELOG.md b/CHANGELOG.md index 7cb3e13..42f494e 100644 --- a/CHANGELOG.md +++ b/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] diff --git a/eliminators.cabal b/eliminators.cabal index d52966c..24b339c 100644 --- a/eliminators.cabal +++ b/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 diff --git a/src/Data/Eliminator.hs b/src/Data/Eliminator.hs index c61d77b..6b85015 100644 --- a/src/Data/Eliminator.hs +++ b/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 diff --git a/src/Data/Eliminator/TH.hs b/src/Data/Eliminator/TH.hs new file mode 100644 index 0000000..34aed3e --- /dev/null +++ b/src/Data/Eliminator/TH.hs @@ -0,0 +1,264 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE Unsafe #-} +{-| +Module: Data.Eliminator.TH +Copyright: (C) 2017 Ryan Scott +License: BSD-style (see the file LICENSE) +Maintainer: Ryan Scott +Stability: Experimental +Portability: GHC + +Generate dependently typed elimination functions using Template Haskell. +-} +module Data.Eliminator.TH ( + -- * Eliminator generation + -- $conventions + deriveElim + , deriveElimNamed + ) where + +import Control.Applicative + +import Data.Char (isUpper) +import Data.Foldable +import qualified Data.Kind as Kind (Type) +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Maybe +import Data.Singletons.Prelude + +import Language.Haskell.TH +import Language.Haskell.TH.Datatype +import Language.Haskell.TH.Desugar (tupleNameDegree_maybe, unboxedTupleNameDegree_maybe) + +{- $conventions +TODO: snappy intro + +The naming conventions are: + +* If the datatype has an alphanumeric name, its eliminator will have that name + with @elim-@ prepended. + +* If the datatype has a symbolic name, its eliminator will have that name + with @~>@ prepended. + +TODO: Conventions for order of arguments + +TODO: The boatloads of extensions you'll need to use this + +TODO: Restrictions (can't use data families, GADTs, or polymorphic recursion, +must have Sing instance, etc.) +-} + +-- | @'deriveElim' dataName@ generates a top-level elimination function for the +-- datatype @dataName@. The eliminator will follow these naming conventions: +-- The naming conventions are: +-- +-- * If the datatype has an alphanumeric name, its eliminator will have that name +-- with @elim@ prepended. +-- +-- * If the datatype has a symbolic name, its eliminator will have that name +-- with @~>@ prepended. +deriveElim :: Name -> Q [Dec] +deriveElim dataName = deriveElimNamed (eliminatorName dataName) dataName + +-- | @'deriveElimNamed' funName dataName@ generates a top-level elimination +-- function named @funName@ for the datatype @dataName@. +deriveElimNamed :: String -> Name -> Q [Dec] +deriveElimNamed funName dataName = do + info@(DatatypeInfo { datatypeVars = vars + , datatypeVariant = _ -- TODO: Reject data family instances + , datatypeCons = cons + }) <- reifyDatatype dataName + predVar <- newName "p" + singVar <- newName "s" + let elimN = mkName funName + dataVarBndrs = catMaybes $ map typeToTyVarBndr vars + promDataKind = datatypeType info + predVarBndr = KindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type)) + singVarBndr = KindedTV singVar promDataKind + caseTypes <- traverse (caseType dataName predVar) cons + let returnType = predType predVar (VarT singVar) + bndrsPrefix = dataVarBndrs ++ [predVarBndr] + allBndrs = bndrsPrefix ++ [singVarBndr] + elimType = ForallT allBndrs [] + (ravel (singType singVar:caseTypes) returnType) + qelimDef + | null cons + = do singVal <- newName "singVal" + pure $ FunD elimN [Clause [VarP singVal] (NormalB (CaseE (VarE singVal) [])) []] + + | otherwise + = do caseClauses + <- itraverse (\i -> caseClause dataName elimN + (map tyVarBndrName bndrsPrefix) + i (length cons)) cons + pure $ FunD elimN caseClauses + elimDef <- qelimDef + pure [SigD elimN elimType, elimDef] + +caseType :: Name -> Name -> ConstructorInfo -> Q Type +caseType dataName predVar + (ConstructorInfo { constructorName = conName + , constructorVars = _ -- TODO: Reject GADTs + , constructorFields = fieldTypes }) + = do vars <- newNameList "f" $ length fieldTypes + let returnType = predType predVar + (foldl' AppT (ConT conName) (map VarT vars)) + mbInductiveType var varType = + let inductiveArg = predType predVar (VarT var) + in mbInductiveCase dataName varType inductiveArg + pure $ foldr' (\(var, varType) t -> + ForallT [KindedTV var varType] + [] + (ravel (singType var:maybeToList (mbInductiveType var varType)) t)) + returnType + (zip vars fieldTypes) + +caseClause :: Name -> Name -> [Name] -> Int -> Int + -> ConstructorInfo -> Q Clause +caseClause dataName elimN bndrNamesPrefix conIndex numCons + (ConstructorInfo { constructorName = conName + , constructorFields = fieldTypes }) + = do let numFields = length fieldTypes + singVars <- newNameList "s" numFields + singVarSigs <- newNameList "sTy" numFields + usedCaseVar <- newName "useThis" + caseVars <- ireplicateA numCons $ \i -> + if i == conIndex + then pure usedCaseVar + else newName ("_p" ++ show i) + let singConName = singDataConName conName + mkSingVarPat var varSig = SigP (VarP var) (singType varSig) + singVarPats = zipWith mkSingVarPat singVars singVarSigs + + mbInductiveArg singVar singVarSig varType = + let prefix = foldAppType (VarE elimN) + $ map VarT bndrNamesPrefix + ++ [VarT singVarSig] + inductiveArg = foldExp prefix + $ VarE singVar:map VarE caseVars + in mbInductiveCase dataName varType inductiveArg + mkArg f (singVar, singVarSig, varType) = + foldExp f $ VarE singVar + : maybeToList (mbInductiveArg singVar singVarSig varType) + rhs = foldl' mkArg (VarE usedCaseVar) $ + zip3 singVars singVarSigs fieldTypes + pure $ Clause (ConP singConName singVarPats : map VarP caseVars) + (NormalB rhs) + [] + +-- TODO: Rule out polymorphic recursion +mbInductiveCase :: Name -> Type -> a -> Maybe a +mbInductiveCase dataName varType inductiveArg + = case unfoldType varType of + headTy :| _ + -- Annoying special case for lists + | ListT <- headTy + , dataName == ''[] + -> Just inductiveArg + + | ConT n <- headTy + , dataName == n + -> Just inductiveArg + + | otherwise + -> Nothing + +-- | Construct a type of the form @'Sing' x@ given @x@. +singType :: Name -> Type +singType x = ConT ''Sing `AppT` VarT x + +-- | Construct a type of the form @p '@@' ty@ given @p@ and @ty@. +predType :: Name -> Type -> Type +predType p ty = InfixT (VarT p) ''(@@) ty + +-- | Generate a list of fresh names with a common prefix, and numbered suffixes. +newNameList :: String -> Int -> Q [Name] +newNameList prefix n = ireplicateA n $ newName . (prefix ++) . show + +eliminatorName :: Name -> String +eliminatorName n + | first:_ <- nStr + , isUpper first + = "elim" ++ nStr + + | otherwise + = "~>" ++ nStr + where + nStr = nameBase n + +typeToTyVarBndr :: Type -> Maybe TyVarBndr +typeToTyVarBndr (SigT (VarT n) k) = Just $ KindedTV n k +typeToTyVarBndr _ = Nothing + +-- Reconstruct and arrow type from the list of types +ravel :: [Type] -> Type -> Type +ravel [] res = res +ravel (h:t) res = AppT (AppT ArrowT h) (ravel t res) + +-- apply an expression to a list of expressions +foldExp :: Exp -> [Exp] -> Exp +foldExp = foldl' AppE + +-- apply an expression to a list of types +foldAppType :: Exp -> [Type] -> Exp +foldAppType = foldl' AppTypeE + +-- | Decompose an applied type into its individual components. For example, this: +-- +-- @ +-- Either Int Char +-- @ +-- +-- would be unfolded to this: +-- +-- @ +-- Either :| [Int, Char] +-- @ +unfoldType :: Type -> NonEmpty Type +unfoldType = go [] + where + go :: [Type] -> Type -> NonEmpty Type + go acc (AppT t1 t2) = go (t2:acc) t1 + go acc (SigT t _) = go acc t + go acc (ForallT _ _ t) = go acc t + go acc t = t :| acc + +tyVarBndrName :: TyVarBndr -> Name +tyVarBndrName (PlainTV n) = n +tyVarBndrName (KindedTV n _) = n + +itraverse :: Applicative f => (Int -> a -> f b) -> [a] -> f [b] +itraverse f xs0 = go xs0 0 where + go [] _ = pure [] + go (x:xs) n = (:) <$> f n x <*> (go xs $! (n + 1)) + +ireplicateA :: Applicative f => Int -> (Int -> f a) -> f [a] +ireplicateA cnt0 f = + loop cnt0 0 + where + loop cnt n + | cnt <= 0 = pure [] + | otherwise = liftA2 (:) (f n) (loop (cnt - 1) $! (n + 1)) + +----- +-- Taken directly from singletons +----- + +singDataConName :: Name -> Name +singDataConName nm + | nm == '[] = 'SNil + | nm == '(:) = 'SCons + | Just degree <- tupleNameDegree_maybe nm = mkTupleDataName degree + | Just degree <- unboxedTupleNameDegree_maybe nm = mkTupleDataName degree + | otherwise = prefixUCName "S" ":%" nm + +mkTupleDataName :: Int -> Name +mkTupleDataName n = mkName $ "STuple" ++ (show n) + +-- put an uppercase prefix on a name. Takes two prefixes: one for identifiers +-- and one for symbols +prefixUCName :: String -> String -> Name -> Name +prefixUCName pre tyPre n = case (nameBase n) of + (':' : rest) -> mkName (tyPre ++ rest) + alpha -> mkName (pre ++ alpha) diff --git a/tests/PeanoSpec.hs b/tests/PeanoSpec.hs index 84f674f..a0389ea 100644 --- a/tests/PeanoSpec.hs +++ b/tests/PeanoSpec.hs @@ -57,7 +57,7 @@ spec = parallel $ do replicateVec :: forall (e :: Type) (howMany :: Peano). Sing howMany -> e -> Vec e howMany -replicateVec s e = elimPeano @howMany @(TyCon1 (Vec e)) s VNil step +replicateVec s e = elimPeano @(TyCon1 (Vec e)) @howMany s VNil step where step :: forall (k :: Peano). Sing k -> Vec e k -> Vec e (S k) step _ = (e :#) @@ -65,7 +65,7 @@ replicateVec s e = elimPeano @howMany @(TyCon1 (Vec e)) s VNil step mapVec :: forall (a :: Type) (b :: Type) (n :: Peano). SingI n => (a -> b) -> Vec a n -> Vec b n -mapVec f = elimPeano @n @(WhyMapVecSym2 a b) (sing @_ @n) base step +mapVec f = elimPeano @(WhyMapVecSym2 a b) @n (sing @_ @n) base step where base :: WhyMapVec a b Z base _ = VNil @@ -76,7 +76,7 @@ mapVec f = elimPeano @n @(WhyMapVecSym2 a b) (sing @_ @n) base step zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Peano). SingI n => (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n -zipWithVec f = elimPeano @n @(WhyZipWithVecSym3 a b c) (sing @_ @n) base step +zipWithVec f = elimPeano @(WhyZipWithVecSym3 a b c) @n (sing @_ @n) base step where base :: WhyZipWithVec a b c Z base _ _ = VNil @@ -91,7 +91,7 @@ zipWithVec f = elimPeano @n @(WhyZipWithVecSym3 a b c) (sing @_ @n) base step appendVec :: forall (e :: Type) (n :: Peano) (m :: Peano). SingI n => Vec e n -> Vec e m -> Vec e (n `Plus` m) -appendVec = elimPeano @n @(WhyAppendVecSym2 e m) (sing @_ @n) base step +appendVec = elimPeano @(WhyAppendVecSym2 e m) @n (sing @_ @n) base step where base :: WhyAppendVec e m Z base _ = id @@ -105,7 +105,7 @@ appendVec = elimPeano @n @(WhyAppendVecSym2 e m) (sing @_ @n) base step transposeVec :: forall (e :: Type) (n :: Peano) (m :: Peano). (SingI n, SingI m) => Vec (Vec e m) n -> Vec (Vec e n) m -transposeVec = elimPeano @n @(WhyTransposeVecSym2 e m) (sing @_ @n) base step +transposeVec = elimPeano @(WhyTransposeVecSym2 e m) @n (sing @_ @n) base step where base :: WhyTransposeVec e m Z base _ = replicateVec (sing @_ @m) VNil diff --git a/tests/PeanoTypes.hs b/tests/PeanoTypes.hs index 56e0b9b..6fe2737 100644 --- a/tests/PeanoTypes.hs +++ b/tests/PeanoTypes.hs @@ -1,16 +1,17 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module PeanoTypes where +import Data.Eliminator.TH import Data.Kind import Data.Singletons.TH @@ -27,14 +28,7 @@ $(singletons [d| times Z _ = Z times (S k) m = plus m (times k m) |]) - -elimPeano :: forall (n :: Peano) (p :: Peano ~> Type). - Sing n - -> p @@ Z - -> (forall (k :: Peano). Sing k -> p @@ k -> p @@ (S k)) - -> p @@ n -elimPeano SZ pZ _ = pZ -elimPeano (SS (sk :: Sing k)) pZ pS = pS sk (elimPeano @k @p sk pZ pS) +$(deriveElim ''Peano) data Vec a (n :: Peano) where VNil :: Vec a Z