diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,19 @@ +## 0.9 [2021.10.31] +* Require `singletons-base-3.1` and GHC 9.2. +* Add `{e,E}limProxy` to `Data.Eliminator`. +* `Data.Eliminator` no longer exports `{e,E}limFirst` and `{e,E}limLast` + eliminators. If you wish to use eliminators that work over `First`/`Last` + from `Data.Monoid`, you must import them `Data.Eliminator.Monoid`. If you + wish to use eliminators that over `First`/`Last` from `Data.Semigroup`, you + must import them from the new `Data.Eliminator.Semigroup` module. +* `Data.Eliminator` no longer exports `{e,E}limProduct` and `{e,E}limSum` + eliminators. If you wish to use eliminators that work over `Product`/`Sum` + from `Data.Monoid` or `Data.Semigroup`, you must import them + `Data.Eliminator.Monoid` or `Data.Eliminator.Semigroup`. If you wish to use + eliminators that over `Product`/`Sum` from + `Data.Functor.Product`/`Data.Functor.Sum`, you must import them from the new + `Data.Eliminator.Functor` module. + ## 0.8 [2021.03.12] * Require `singletons-base-3.0` and GHC 9.0. * Remove eliminators for `Data.Semigroup.Option`, which is deprecated as of diff --git a/eliminators.cabal b/eliminators.cabal --- a/eliminators.cabal +++ b/eliminators.cabal @@ -1,5 +1,5 @@ name: eliminators -version: 0.8 +version: 0.9 synopsis: Dependently typed elimination functions using singletons description: This library provides eliminators for inductive data types, leveraging the power of the @singletons@ library to allow @@ -16,7 +16,7 @@ build-type: Simple extra-source-files: CHANGELOG.md, README.md cabal-version: >=1.10 -tested-with: GHC == 9.0.1 +tested-with: GHC == 9.2.1 source-repository head type: git @@ -24,15 +24,18 @@ library exposed-modules: Data.Eliminator + Data.Eliminator.Functor + Data.Eliminator.Monoid + Data.Eliminator.Semigroup Data.Eliminator.TH Data.Eliminator.TypeNats - build-depends: base >= 4.15 && < 4.16 + build-depends: base >= 4.16 && < 4.17 , extra >= 1.4.2 && < 1.8 - , singletons-base >= 3.0 && < 3.1 + , singletons-base >= 3.1 && < 3.2 , singleton-nats >= 0.4.2 && < 0.5 - , template-haskell >= 2.17 && < 2.18 + , template-haskell >= 2.18 && < 2.19 , th-abstraction >= 0.4 && < 0.5 - , th-desugar >= 1.12 && < 1.13 + , th-desugar >= 1.13 && < 1.14 hs-source-dirs: src default-language: Haskell2010 ghc-options: -Wall -Wcompat -Wno-unticked-promoted-constructors @@ -50,12 +53,13 @@ MatchabilizeTypes ListSpec ListTypes + PolyRecTypes VecTypes VecSpec - build-depends: base >= 4.15 && < 4.16 + build-depends: base >= 4.16 && < 4.17 , eliminators , hspec >= 2 && < 3 - , singletons-base >= 3.0 && < 3.1 + , singletons-base >= 3.1 && < 3.2 , singleton-nats >= 0.4.2 && < 0.5 build-tool-depends: hspec-discover:hspec-discover hs-source-dirs: tests diff --git a/src/Data/Eliminator.hs b/src/Data/Eliminator.hs --- a/src/Data/Eliminator.hs +++ b/src/Data/Eliminator.hs @@ -23,6 +23,29 @@ Portability: GHC Dependently typed elimination functions using @singletons@. + +This module exports a combination of eliminators whose names are known not to +clash with each other. Potential name conflicts have been resolved by putting +the conflicting names in separate modules: + +* "Data.Eliminator" defines 'elimNat', which works over the 'Nat' data type + from "Data.Nat". For an eliminator that works over 'Nat' from "GHC.TypeNats", + see "Data.Eliminator.TypeNats". + +* "Data.Eliminator" avoids exporting eliminators for @First@ and @Last@ data + types, as there are multiple data types with these names. If you want + eliminators for the 'First' and 'Last' data types from "Data.Monoid", import + them from "Data.Eliminator.Monoid". If you want eliminators for the 'First' + and 'Last' data types from "Data.Semigroup", import them from + "Data.Eliminator.Semigroup". + +* "Data.Eliminator" avoids exporting eliminators for @Product@ and @Sum@ data + types, as there are multiple data types with these names. If you want + eliminators for the 'Product' and 'Sum' data types from "Data.Monoid" or + "Data.Semigroup", import them from "Data.Eliminator.Monoid" or + "Data.Eliminator.Semigroup". If you want eliminators for the 'Product' and + 'Sum' data types from "Data.Functor.Product" and "Data.Functor.Sum", + respectively, import them from "Data.Eliminator.Functor". -} module Data.Eliminator ( -- * Eliminator functions @@ -43,12 +66,8 @@ , ElimDual , elimEither , ElimEither - , elimFirst - , ElimFirst , elimIdentity , ElimIdentity - , elimLast - , ElimLast , elimList , ElimList , elimMax @@ -63,10 +82,8 @@ , ElimNonEmpty , elimOrdering , ElimOrdering - , elimProduct - , ElimProduct - , elimSum - , ElimSum + , elimProxy + , ElimProxy , elimTuple0 , ElimTuple0 , elimTuple2 @@ -89,27 +106,22 @@ import Control.Monad.Extra +import Data.Eliminator.Functor +import Data.Eliminator.Monoid +import Data.Eliminator.Semigroup import Data.Eliminator.TH -import Data.Functor.Const (Const(..)) -import Data.Functor.Const.Singletons (SConst(..)) -import Data.Functor.Identity (Identity(..)) -import Data.Functor.Identity.Singletons (SIdentity(..)) import Data.List.NonEmpty (NonEmpty(..)) import Data.List.NonEmpty.Singletons (SNonEmpty(..)) -import Data.Monoid hiding (First, Last) -import Data.Monoid.Singletons hiding (SFirst, SLast) import Data.Nat import Data.Ord (Down(..)) import Data.Ord.Singletons (SDown(..)) -import Data.Semigroup -import Data.Semigroup.Singletons +import Data.Proxy.Singletons (SProxy(..)) import Data.Void (Void) import Language.Haskell.TH (nameBase) import Language.Haskell.TH.Desugar (tupleNameDegree_maybe) -import Prelude.Singletons hiding - (All, Any, Const, Last, Min, Max, Product, Sum) +import Prelude.Singletons {- $eliminators @@ -128,27 +140,15 @@ -} $(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n) - [ ''All - , ''Any - , ''Arg - , ''Bool - , ''Const + [ ''Bool , ''Down - , ''Dual , ''Either - , ''First - , ''Identity - , ''Last - , ''Max , ''Maybe - , ''Min , ''Nat , ''NonEmpty , ''Ordering - , ''Product - , ''Sum + , ''Proxy , ''Void - , ''WrappedMonoid ]) $(deriveElimNamed "elimList" ''[]) $(deriveTypeElimNamed "ElimList" ''[]) diff --git a/src/Data/Eliminator/Functor.hs b/src/Data/Eliminator/Functor.hs new file mode 100644 --- /dev/null +++ b/src/Data/Eliminator/Functor.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-| +Module: Data.Eliminator.Functor +Copyright: (C) 2021 Ryan Scott +License: BSD-style (see the file LICENSE) +Maintainer: Ryan Scott +Stability: Experimental +Portability: GHC + +Eliminator functions for data types in the @Data.Functor.*@ module namespace. +All of these are re-exported from "Data.Eliminator" with the exceptions of +'Sum' and 'Product', as these clash with eliminators of the same names in +"Data.Eliminator.Semigroup" and "Data.Eliminator.Monoid". +-} +module Data.Eliminator.Functor ( + elimConst + , ElimConst + , elimIdentity + , ElimIdentity + , elimProduct + , ElimProduct + , elimSum + , ElimSum + ) where + +import Control.Monad.Extra + +import Data.Eliminator.TH +import Data.Functor.Const (Const(..)) +import Data.Functor.Const.Singletons (SConst(..)) +import Data.Functor.Identity (Identity(..)) +import Data.Functor.Identity.Singletons (SIdentity(..)) +import Data.Functor.Product (Product(..)) +import Data.Functor.Product.Singletons (SProduct(..)) +import Data.Functor.Sum (Sum(..)) +import Data.Functor.Sum.Singletons (SSum(..)) + +$(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n) + [ ''Const + , ''Identity + , ''Product + , ''Sum + ]) diff --git a/src/Data/Eliminator/Monoid.hs b/src/Data/Eliminator/Monoid.hs new file mode 100644 --- /dev/null +++ b/src/Data/Eliminator/Monoid.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-| +Module: Data.Eliminator.Monoid +Copyright: (C) 2021 Ryan Scott +License: BSD-style (see the file LICENSE) +Maintainer: Ryan Scott +Stability: Experimental +Portability: GHC + +Eliminator functions for data types in "Data.Monoid". All of these are +re-exported from "Data.Eliminator" with the following exceptions: + +* 'First' and 'Last' are not re-exported from "Data.Eliminator", as they clash + with eliminators of the same names in "Data.Eliminator.Functor" and + "Data.Eliminator.Semigroup". + +* 'Sum' and 'Product' are not re-exported from "Data.Eliminator", as they clash + with eliminators of the same names in "Data.Eliminator.Functor". +-} +module Data.Eliminator.Monoid ( + elimAll + , ElimAll + , elimAny + , ElimAny + , elimDual + , ElimDual + , elimFirst + , ElimFirst + , elimLast + , ElimLast + , elimProduct + , ElimProduct + , elimSum + , ElimSum + ) where + +import Control.Monad.Extra + +import Data.Eliminator.TH +import Data.Monoid +import Data.Monoid.Singletons + +$(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n) + [ ''All + , ''Any + , ''Dual + , ''First + , ''Last + , ''Product + , ''Sum + ]) diff --git a/src/Data/Eliminator/Semigroup.hs b/src/Data/Eliminator/Semigroup.hs new file mode 100644 --- /dev/null +++ b/src/Data/Eliminator/Semigroup.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-| +Module: Data.Eliminator.Semigroup +Copyright: (C) 2021 Ryan Scott +License: BSD-style (see the file LICENSE) +Maintainer: Ryan Scott +Stability: Experimental +Portability: GHC + +Eliminator functions for data types in "Data.Semigroup". All of these are +re-exported from "Data.Eliminator" with the following exceptions: + +* 'First' and 'Last' are not re-exported from "Data.Eliminator", as they clash + with eliminators of the same names in "Data.Eliminator.Functor" and + "Data.Eliminator.Monoid". + +* 'Sum' and 'Product' are not re-exported from "Data.Eliminator", as they clash + with eliminators of the same names in "Data.Eliminator.Functor". +-} +module Data.Eliminator.Semigroup ( + elimAll + , ElimAll + , elimAny + , ElimAny + , elimArg + , ElimArg + , elimDual + , ElimDual + , elimFirst + , ElimFirst + , elimLast + , ElimLast + , elimMax + , ElimMax + , elimMin + , ElimMin + , elimProduct + , ElimProduct + , elimSum + , ElimSum + , elimWrappedMonoid + , ElimWrappedMonoid + ) where + +import Control.Monad.Extra + +import Data.Eliminator.Monoid hiding (elimFirst, ElimFirst, elimLast, ElimLast) +import Data.Eliminator.TH +import Data.Semigroup +import Data.Semigroup.Singletons + +$(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n) + [ ''Arg + , ''First + , ''Last + , ''Max + , ''Min + , ''WrappedMonoid + ]) diff --git a/src/Data/Eliminator/TH.hs b/src/Data/Eliminator/TH.hs --- a/src/Data/Eliminator/TH.hs +++ b/src/Data/Eliminator/TH.hs @@ -275,9 +275,10 @@ -> Name -- The name of the data type -> Q [Dec] -- The eliminator's type signature and body deriveElimNamed' prox funName dataName = do - info@(DatatypeInfo { datatypeVars = dataVarBndrs - , datatypeVariant = variant - , datatypeCons = cons + info@(DatatypeInfo { datatypeVars = dataVarBndrs + , datatypeInstTypes = instTys + , datatypeVariant = variant + , datatypeCons = cons }) <- reifyDatatype dataName let noDataFamilies = fail "Eliminators for data family instances are currently not supported" @@ -293,6 +294,8 @@ predVarBndr = kindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type)) singVarBndr = kindedTV singVar promDataKind caseTypes <- traverse (caseType prox dataName predVar) cons + unless (length (findParams info) == length instTys) $ + fail "Eliminators for polymorphically recursive data types are currently not supported" let returnType = predType predVar (VarT singVar) elimType = elimTypeSig prox dataVarBndrs predVarBndr singVarBndr caseTypes returnType @@ -328,44 +331,33 @@ returnType (zip vars fieldTypes) --- Generate a single clause for a term-level eliminator. -caseClause :: - Name -- The name of the eliminator function +-- Generate a single clause for a term-level eliminator's @go@ function. +goCaseClause :: + Name -- The name of the @go@ function -> Name -- The name of the data type - -> [TyVarBndrUnit] -- The type variables bound by the data type - -> TyVarBndrUnit -- The predicate type variable - -> Int -- The index of this constructor (0-indexed) - -> Int -- The total number of data constructors + -> Name -- The name of the "case alternative" to apply on the right-hand side -> ConstructorInfo -- The data constructor -> Q Clause -- The generated function clause -caseClause elimName dataName dataVarBndrs predVarBndr conIndex numCons +goCaseClause goName dataName usedCaseVar (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 = singledDataConName defaultOptions conName mkSingVarPat var varSig = SigP (VarP var) (singType varSig) singVarPats = zipWith mkSingVarPat singVars singVarSigs mbInductiveArg singVar singVarSig varType = - let prefix = foldAppTypeE (VarE elimName) - $ map (VarT . tvName) dataVarBndrs - ++ [VarT (tvName predVarBndr), VarT singVarSig] - inductiveArg = foldAppE prefix - $ VarE singVar:map VarE caseVars - in mbInductiveCase dataName varType inductiveArg + let inductiveArg = VarE goName `AppTypeE` VarT singVarSig + `AppE` VarE singVar + in mbInductiveCase dataName varType $ const inductiveArg mkArg f (singVar, singVarSig, varType) = foldAppE 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) + pure $ Clause [ConP singConName [] singVarPats] (NormalB rhs) [] @@ -403,7 +395,7 @@ let inductiveArg = foldAppT prefix $ VarT predVarName : VarT singVar : map VarT caseVarNames - in mbInductiveCase dataName varType inductiveArg + in mbInductiveCase dataName varType $ const inductiveArg mkArg f (singVar, varType) = foldAppDefunT (f `AppT` VarT singVar) $ maybeToList (mbInductiveArg singVar varType) @@ -476,16 +468,40 @@ ForallT [kindedTVSpecified var varType] [] $ ravel (singType var:maybeToList (mbInductiveType dataName predVar var varType)) t - qElimEqns _ elimName dataName dataVarBndrs predVarBndr _singVarBndr _caseTypes cons - | null cons - = do singVal <- newName "singVal" - pure $ FunD elimName [Clause [VarP singVal] - (NormalB (CaseE (VarE singVal) [])) []] - | otherwise - = do caseClauses - <- itraverse (\i -> caseClause elimName dataName - dataVarBndrs predVarBndr i (length cons)) cons - pure $ FunD elimName caseClauses + -- A unique characteristic of term-level eliminators is that we manually + -- apply the static argument transformation, e.g., + -- + -- elimT :: forall a (p :: T a ~> Type) (t :: T a). + -- Sing t + -- -> (forall (x :: a) (xs :: T a). + -- Sing x -> Sing xs -> Apply p xs -> Apply p (MkT x xs)) + -- -> Apply p t + -- elimT st k = go @s k + -- where + -- go :: forall (t' :: T a). + -- Sing t' -> Apply p t' + -- go (SMkT (sx :: Sing x) (sxs :: Sing xs)) = + -- k sx sxs (go @xs sxs) + -- + -- This reduces the likelihood of recursive calls falling afoul of GHC's + -- ambiguity check. + qElimEqns _ elimName dataName _dataVarBndrs predVarBndr singVarBndr _caseTypes cons = do + singTermVar <- newName "s" + caseVars <- newNameList "p" $ length cons + goName <- newName "go" + let singTypeVar = tvName singVarBndr + goSingTypeVar <- newName $ nameBase singTypeVar + let elimRHS = VarE goName `AppTypeE` VarT singTypeVar `AppE` VarE singTermVar + goSingVarBndr = mapTVName (const goSingTypeVar) singVarBndr + goReturnType = predType (tvName predVarBndr) (VarT goSingTypeVar) + goType = ForallT (changeTVFlags SpecifiedSpec [goSingVarBndr]) [] $ + ArrowT `AppT` singType goSingTypeVar `AppT` goReturnType + goClauses + <- if null cons + then pure [Clause [VarP singTermVar] (NormalB (CaseE (VarE singTermVar) [])) []] + else zipWithM (goCaseClause goName dataName) caseVars cons + pure $ FunD elimName [ Clause (map VarP (singTermVar:caseVars)) (NormalB elimRHS) + [SigD goName goType, FunD goName goClauses] ] instance Eliminator IsType where elimSigD _ = KiSigD @@ -512,21 +528,20 @@ mbInductiveType :: Name -> Name -> Name -> Kind -> Maybe Type mbInductiveType dataName predVar var varType = - mbInductiveCase dataName varType $ predType predVar $ VarT var + mbInductiveCase dataName varType $ const $ predType predVar $ VarT var --- TODO: Rule out polymorphic recursion -mbInductiveCase :: Name -> Type -> a -> Maybe a +mbInductiveCase :: Name -> Type -> ([TypeArg] -> a) -> Maybe a mbInductiveCase dataName varType inductiveArg = case unfoldType varType of - (headTy, _) + (headTy, argTys) -- Annoying special case for lists | ListT <- headTy , dataName == ''[] - -> Just inductiveArg + -> Just $ inductiveArg argTys | ConT n <- headTy , dataName == n - -> Just inductiveArg + -> Just $ inductiveArg argTys | otherwise -> Nothing @@ -573,10 +588,6 @@ foldAppE :: Exp -> [Exp] -> Exp foldAppE = foldl' AppE --- Apply an expression to a list of types using visible type applications. -foldAppTypeE :: Exp -> [Type] -> Exp -foldAppTypeE = foldl' AppTypeE - -- Apply a type to a list of types using ordinary function applications. foldAppT :: Type -> [Type] -> Type foldAppT = foldl' AppT @@ -602,6 +613,108 @@ loop cnt n | cnt <= 0 = pure [] | otherwise = liftA2 (:) (f n) (loop (cnt - 1) $! (n + 1)) + +-- | Find the data type constructor arguments that are parameters. +-- +-- Parameters are names which are unchanged across the structure. +-- They appear at least once in every constructor type, always appear +-- in the same argument position(s), and nothing else ever appears in those +-- argument positions. +-- +-- This was adapted from a similar algorithm used in Idris +-- (https://github.com/idris-lang/Idris-dev/blob/a13caeb4e50d0c096d34506f2ebf6b9d140a07aa/src/Idris/Elab/Utils.hs#L401-L468), +-- licensed under the BSD-3-Clause license. +findParams :: DatatypeInfo -> [Int] +findParams (DatatypeInfo { datatypeName = dataName + , datatypeInstTypes = instTys + , datatypeCons = cons + }) = + let allapps = map getDataApp cons + -- do each constructor separately, then merge the results (names + -- may change between constructors) + conParams = map paramPos allapps + in inAll conParams + where + inAll :: Eq pos => [[pos]] -> [pos] + inAll [] = [] + inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x + + paramPos :: Eq name => [[Maybe name]] -> [Int] + paramPos [] = [] + paramPos (args : rest) + = dropNothing $ keepSame (zip [0..] args) rest + + dropNothing :: [(pos, Maybe name)] -> [pos] + dropNothing [] = [] + dropNothing ((_, Nothing) : ts) = dropNothing ts + dropNothing ((x, _) : ts) = x : dropNothing ts + + keepSame :: Eq name => + [(pos, Maybe name)] -> [[Maybe name]] -> + [(pos, Maybe name)] + keepSame as [] = as + keepSame as (args : rest) = keepSame (update as args) rest + + update :: Eq name => [(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)] + update [] _ = [] + update _ [] = [] + update ((n, Just x) : as) (Just x' : args) + | x == x' = (n, Just x) : update as args + update ((n, _) : as) (_ : args) = (n, Nothing) : update as args + + getDataApp :: ConstructorInfo -> [[Maybe Name]] + getDataApp (ConstructorInfo { constructorFields = fields }) = + concatMap getThem $ + fields ++ [ applyType (ConT dataName) $ map TANormal + $ map unSigType instTys + ] + where + getThem :: Type -> [[Maybe Name]] + getThem ty = maybeToList $ mbInductiveCase dataName ty inductiveArg + + inductiveArg :: [TypeArg] -> [Maybe Name] + inductiveArg argTys = + let visArgTys = filterTANormals argTys + in mParam visArgTys visArgTys + + -- keep the arguments which are single names, which appear + -- in the return type, counting only the first time they appear in + -- the return type as the parameter position + mParam :: [Type] -> [Type] -> [Maybe Name] + mParam _ [] = [] + mParam args (VarT n:rest) + | paramIn False n args + = Just n : mParam (filter (noN n) args) rest + mParam args (_:rest) = Nothing : mParam args rest + + paramIn :: Bool -> Name -> [Type] -> Bool + paramIn ok _ [] = ok + paramIn ok n (VarT t:ts) = paramIn (ok || n == t) n ts + paramIn ok n (t:ts) + | n `elem` freeVariables t = False -- not a single name + | otherwise = paramIn ok n ts + + -- If the name appears again later, don't count that appearance + -- as a parameter position + noN :: Name -> Type -> Bool + noN n (VarT t) = n /= t + noN _ _ = False + +----- +-- Taken directly from th-desugar +----- + +-- | Remove all of the explicit kind signatures from a 'Type'. +unSigType :: Type -> Type +unSigType (SigT t _) = t +unSigType (AppT f x) = AppT (unSigType f) (unSigType x) +unSigType (ForallT tvbs ctxt t) = ForallT tvbs (map unSigType ctxt) (unSigType t) +unSigType (InfixT t1 n t2) = InfixT (unSigType t1) n (unSigType t2) +unSigType (UInfixT t1 n t2) = UInfixT (unSigType t1) n (unSigType t2) +unSigType (ParensT t) = ParensT (unSigType t) +unSigType (AppKindT t k) = AppKindT (unSigType t) (unSigType k) +unSigType (ImplicitParamT n t) = ImplicitParamT n (unSigType t) +unSigType t = t ----- -- Taken directly from singletons diff --git a/src/Data/Eliminator/TypeNats.hs b/src/Data/Eliminator/TypeNats.hs --- a/src/Data/Eliminator/TypeNats.hs +++ b/src/Data/Eliminator/TypeNats.hs @@ -21,7 +21,7 @@ import Data.Kind (Type) import Data.Singletons -import GHC.TypeLits.Singletons +import GHC.TypeLits.Singletons () import GHC.TypeNats import Unsafe.Coerce (unsafeCoerce) diff --git a/tests/DecideTypes.hs b/tests/DecideTypes.hs --- a/tests/DecideTypes.hs +++ b/tests/DecideTypes.hs @@ -11,6 +11,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-unused-foralls #-} module DecideTypes where import Data.Eliminator @@ -18,7 +19,7 @@ import Data.Nat import Data.Singletons.TH hiding (Decision(..)) -import Prelude.Singletons +import Prelude.Singletons (ConstSym1) -- Due to https://github.com/goldfirere/singletons/issues/82, promoting the -- Decision data type from Data.Singletons.Decide is a tad awkward. To work @@ -33,8 +34,11 @@ -> (forall (yes :: a). Sing yes -> p @@ Proved yes) -> (forall (no :: a ~> Void). Sing no -> p @@ Disproved no) -> p @@ d -elimDecision (SProved yes) pProved _ = pProved yes -elimDecision (SDisproved no) _ pDisproved = pDisproved no +elimDecision sd pProved pDisproved = go @d sd + where + go :: forall (d' :: PDecision a). Sing d' -> p @@ d' + go (SProved yes) = pProved yes + go (SDisproved no) = pDisproved no type ElimDecision :: forall a. forall (p :: PDecision a ~> Type) @@ -89,44 +93,71 @@ newtype WhyDecEqList (l1 :: [e]) = WhyDecEqList { runWhyDecEqList :: forall (l2 :: [e]). Sing l2 -> Decision (l1 :~: l2) } -$(singletons [d| - type ConstVoidNat :: forall (m :: Nat) -> Const Type m -> Const Type (S m) - type ConstVoidNat m r = Void +type ConstVoidNat :: Nat -> Type -> Type +type ConstVoidNat m r = Void - type EqSameNat :: Nat -> forall (m :: Nat) -> Const Type m -> Const Type (S m) - type EqSameNat n m r = n :~: m +-- ElimNat requires an argument of kind (forall (m :: Nat) -> ...), which is +-- not the same thing as (Nat -> ...). Unfortunately, it's not easy to convince +-- singletons-th to generate defunctionalization symbols for ConstVoidNat that +-- have a dependent kind like this. As a result, we have to define +-- defunctionalization symbols by hand with the appropriate kind. +type ConstVoidNatSym :: forall (m :: Nat) -> (Type ~> Type) +data ConstVoidNatSym m z +type instance Apply (ConstVoidNatSym m) r = ConstVoidNat m r - type ConstVoidList :: forall e. forall (y :: e) (ys :: [e]) - -> Const Type ys -> Const Type (y:ys) - type ConstVoidList y ys r = Void +type EqSameNat :: Nat -> Nat -> Type -> Type +type EqSameNat n m r = n :~: m - type EqSameList :: forall e. e -> [e] -> forall (y :: e) (ys :: [e]) - -> Const Type ys -> Const Type (y:ys) - type EqSameList x xs y ys r = (x :~: y, xs :~: ys) - |]) +type EqSameNatSym :: Nat -> forall (m :: Nat) -> (Type ~> Type) +data EqSameNatSym n m z +type instance Apply (EqSameNatSym n m) r = EqSameNat n m r +type ConstVoidList :: e -> [e] -> Type -> Type +type ConstVoidList y ys r = Void + +type ConstVoidListSym :: forall e. forall (y :: e) (ys :: [e]) + -> (Type ~> Type) +data ConstVoidListSym y ys z +type instance Apply (ConstVoidListSym y ys) r = ConstVoidList y ys r + +type EqSameList :: e -> [e] -> e -> [e] -> Type -> Type +type EqSameList x xs y ys r = (x :~: y, xs :~: ys) + +type EqSameListSym :: forall e. e -> [e] -> forall (y :: e) (ys :: [e]) + -> (Type ~> Type) +data EqSameListSym x xs y ys z +type instance Apply (EqSameListSym x xs y ys) r = EqSameList x xs y ys r + $(singletons [d| type NatEqConsequencesBase :: Nat -> Type - type NatEqConsequencesBase m = ElimNat (ConstSym1 Type) m () ConstVoidNatSym1 + type NatEqConsequencesBase m = ElimNat (ConstSym1 Type) m () ConstVoidNatSym - type NatEqConsequencesStep :: forall (m :: Nat) -> Const (Nat ~> Type) m - -> Nat -> Const Type (S m) - type NatEqConsequencesStep m r n = ElimNat (ConstSym1 Type) n Void (EqSameNatSym2 m) + type NatEqConsequencesStep :: Nat -> (Nat ~> Type) -> Nat -> Type + type NatEqConsequencesStep m r n = ElimNat (ConstSym1 Type) n Void (EqSameNatSym m) type ListEqConsequencesBase :: [e] -> Type - type ListEqConsequencesBase ys = ElimList (ConstSym1 Type) ys () ConstVoidListSym2 + type ListEqConsequencesBase ys = ElimList (ConstSym1 Type) ys () ConstVoidListSym - type ListEqConsequencesStep :: forall e. forall (x :: e) (xs :: [e]) - -> Const ([e] ~> Type) xs -> [e] -> Const Type (x:xs) - type ListEqConsequencesStep x xs r ys = ElimList (ConstSym1 Type) ys Void (EqSameListSym4 x xs) + type ListEqConsequencesStep :: e -> [e] -> ([e] ~> Type) -> [e] -> Type + type ListEqConsequencesStep x xs r ys = ElimList (ConstSym1 Type) ys Void (EqSameListSym x xs) |]) +type NatEqConsequencesStepSym :: forall (m :: Nat) + -> (Nat ~> Type) ~> (Nat ~> Type) +data NatEqConsequencesStepSym m z +type instance Apply (NatEqConsequencesStepSym m) r = NatEqConsequencesStepSym2 m r + +type ListEqConsequencesStepSym :: forall e. forall (x :: e) (xs :: [e]) + -> ([e] ~> Type) ~> ([e] ~> Type) +data ListEqConsequencesStepSym x xs z +type instance Apply (ListEqConsequencesStepSym x xs) r = ListEqConsequencesStepSym3 x xs r + $(singletons [d| type NatEqConsequences :: Nat -> Nat -> Type type NatEqConsequences n m = ElimNat (ConstSym1 (Nat ~> Type)) n NatEqConsequencesBaseSym0 - NatEqConsequencesStepSym1 @@ m + NatEqConsequencesStepSym @@ m type WhyNatEqConsequencesSame :: Nat -> Type type WhyNatEqConsequencesSame a = NatEqConsequences a a @@ -141,7 +172,7 @@ type ListEqConsequences (xs :: [e]) (ys :: [e]) = ElimList (ConstSym1 ([e] ~> Type)) xs ListEqConsequencesBaseSym0 - ListEqConsequencesStepSym2 @@ ys + ListEqConsequencesStepSym @@ ys type WhyListEqConsequencesSame :: [e] -> Type type WhyListEqConsequencesSame es = ListEqConsequences es es diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs --- a/tests/GADTSpec.hs +++ b/tests/GADTSpec.hs @@ -82,12 +82,16 @@ -> (forall a' b' (x :: a'). Sing x -> p @@ (MkFlarble1 x :: Flarble a' b')) -> (forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b'))) -> p @@ f -elimFlarble s@(SMkFlarble1 sx) pMkFlarble1 _ = - case s of - (_ :: Sing (MkFlarble1 x :: Flarble a' b')) -> pMkFlarble1 @a' @b' @x sx -elimFlarble s@SMkFlarble2 _ pMkFlarble2 = - case s of - (_ :: Sing (MkFlarble2 :: Flarble Bool (Maybe b'))) -> pMkFlarble2 @b' +elimFlarble sf pMkFlarble1 pMkFlarble2 = go @a @b @f sf + where + go :: forall a' b' (f' :: Flarble a' b'). + Sing f' -> p @@ f' + go s@(SMkFlarble1 sx) = + case s of + (_ :: Sing (MkFlarble1 x :: Flarble a'' b'')) -> pMkFlarble1 @a'' @b'' @x sx + go s@SMkFlarble2 = + case s of + (_ :: Sing (MkFlarble2 :: Flarble Bool (Maybe b''))) -> pMkFlarble2 @b'' type ElimFlarble :: forall (p :: forall x y. Flarble x y ~> Type) @@ -113,12 +117,15 @@ -> (forall a' b'. a' -> p @@ a' @@ b') -> (forall b'. p @@ Bool @@ Maybe b') -> p @@ a @@ b -elimPropFlarble f@(MkFlarble1 x) pMkFlarble1 _ = - case f of - (_ :: Flarble a' b') -> pMkFlarble1 @a' @b' x -elimPropFlarble f@MkFlarble2 _ pMkFlarble2 = - case f of - (_ :: Flarble Bool (Maybe b')) -> pMkFlarble2 @b' +elimPropFlarble fl pMkFlarble1 pMkFlarble2 = go @a @b fl + where + go :: forall a' b'. Flarble a' b' -> p @@ a' @@ b' + go f@(MkFlarble1 x) = + case f of + (_ :: Flarble a'' b'') -> pMkFlarble1 @a'' @b'' x + go f@MkFlarble2 = + case f of + (_ :: Flarble Bool (Maybe b'')) -> pMkFlarble2 @b'' type ElimPropFlarble :: forall (p :: Type ~> Type ~> Prop) diff --git a/tests/PolyRecTypes.hs b/tests/PolyRecTypes.hs new file mode 100644 --- /dev/null +++ b/tests/PolyRecTypes.hs @@ -0,0 +1,93 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module PolyRecTypes where + +import Data.Kind +import Data.Singletons.Base.TH + +import Internal + +$(singletons [d| + type WeirdList :: Type -> Type + data WeirdList a = WeirdNil | WeirdCons a (WeirdList (WeirdList a)) + |]) + +elimWeirdList :: forall (p :: forall t. WeirdList t ~> Type) + a (wl :: WeirdList a). + Sing wl + -> (forall t. p @t @@ WeirdNil) + -> (forall t (x :: t) (xs :: WeirdList (WeirdList t)). + Sing x -> Sing xs -> p @(WeirdList t) @@ xs -> p @t @@ (WeirdCons x xs)) + -> p @a @@ wl +elimWeirdList swl pWeirdNil pWeirdCons = go @a @wl swl + where + go :: forall t (wlt :: WeirdList t). Sing wlt -> p @t @@ wlt + go SWeirdNil = pWeirdNil @t + go (SWeirdCons (sx :: Sing x) (sxs :: Sing xs)) = + pWeirdCons @t @x @xs sx sxs (go @(WeirdList t) @xs sxs) + +type ElimWeirdList :: forall (p :: forall t. WeirdList t ~> Type) + -> forall a. + forall (wl :: WeirdList a) + -> (forall t. p @t @@ WeirdNil) + -> (forall t. + forall (x :: t) (xs :: WeirdList (WeirdList t)) -> + p @(WeirdList t) @@ xs ~> p @t @@ (WeirdCons x xs)) + -> p @a @@ wl +type family ElimWeirdList p wl pWeirdNil pWeirdCons where + forall (p :: forall t. WeirdList t ~> Type) + (pWeirdNil :: forall t. p @t @@ WeirdNil) + (pWeirdCons :: forall t. forall (x :: t) (xs :: WeirdList (WeirdList t)) -> + p @(WeirdList t) @@ xs ~> p @t @@ (WeirdCons x xs)) + a. + ElimWeirdList p (WeirdNil @a) pWeirdNil pWeirdCons = pWeirdNil @a + forall (p :: forall t. WeirdList t ~> Type) + (pWeirdNil :: forall t. p @t @@ WeirdNil) + (pWeirdCons :: forall t. forall (x :: t) (xs :: WeirdList (WeirdList t)) -> + p @(WeirdList t) @@ xs ~> p @t @@ (WeirdCons x xs)) + a (x :: a) (xs :: WeirdList (WeirdList a)). + ElimWeirdList p (WeirdCons @a x xs) pWeirdNil pWeirdCons = + pWeirdCons @a x xs @@ ElimWeirdList p @(WeirdList a) xs pWeirdNil pWeirdCons + +elimPropWeirdList :: forall (p :: Prop ~> Prop) + (a :: Prop). + WeirdList a + -> (forall (t :: Prop). p @@ t) + -> (forall (t :: Prop). + t -> WeirdList (WeirdList t) -> p @@ WeirdList t -> p @@ t) + -> p @@ a +elimPropWeirdList wl pWeirdNil pWeirdCons = go @a wl + where + go :: forall (t :: Prop). WeirdList t -> p @@ t + go WeirdNil = pWeirdNil @t + go (WeirdCons x xs) = pWeirdCons @t x xs (go @(WeirdList t) xs) + +type ElimPropWeirdList :: forall (p :: Prop ~> Prop) + -> forall (a :: Prop). + WeirdList a + -> (forall (t :: Prop). p @@ t) + -> (forall (t :: Prop). + t ~> WeirdList (WeirdList t) ~> p @@ WeirdList t ~> p @@ t) + -> p @@ a +type family ElimPropWeirdList p wl pWeirdNil pWeirdCons where + forall (p :: Prop ~> Prop) + (pWeirdNil :: forall (t :: Prop). p @@ t) + (pWeirdCons :: forall (t :: Prop). t ~> WeirdList (WeirdList t) ~> p @@ WeirdList t ~> p @@ t) + a. + ElimPropWeirdList p (WeirdNil @a) pWeirdNil pWeirdCons = pWeirdNil @a + forall (p :: Prop ~> Prop) + (pWeirdNil :: forall (t :: Prop). p @@ t) + (pWeirdCons :: forall (t :: Prop). t ~> WeirdList (WeirdList t) ~> p @@ WeirdList t ~> p @@ t) + a (x :: a) (xs :: WeirdList (WeirdList a)). + ElimPropWeirdList p (WeirdCons x xs) pWeirdNil pWeirdCons = + pWeirdCons @a @@ x @@ xs @@ ElimPropWeirdList p @(WeirdList a) xs pWeirdNil pWeirdCons diff --git a/tests/VecTypes.hs b/tests/VecTypes.hs --- a/tests/VecTypes.hs +++ b/tests/VecTypes.hs @@ -53,9 +53,13 @@ -> (forall (k :: Nat) (x :: a) (xs :: Vec a k). Sing x -> Sing xs -> p @@ xs -> p @@ (x :# xs)) -> p @@ v -elimVec SVNil pVNil _ = pVNil -elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons = - pVCons sx sxs (elimVec @a @p @k @xs sxs pVNil pVCons) +elimVec sv pVNil pVCons = go @n @v sv + where + go :: forall (n' :: Nat) (v' :: Vec a n'). + Sing v' -> p @@ v' + go SVNil = pVNil + go (sx :%# (sxs :: Sing (xs :: Vec a k))) = + pVCons sx sxs (go @k @xs sxs) type ElimVec :: forall a. forall (p :: forall (k :: Nat). Vec a k ~> Type) @@ -86,9 +90,11 @@ -> p @@ Z -> (forall (k :: Nat). a -> Vec a k -> p @@ k -> p @@ S k) -> p @@ n -elimPropVec VNil pZ _ = pZ -elimPropVec (x :# (xs :: Vec a k)) pZ pS = - pS x xs (elimPropVec @a @p @k xs pZ pS) +elimPropVec v pZ pS = go @n v + where + go :: forall (n' :: Nat). Vec a n' -> p @@ n' + go VNil = pZ + go (x :# (xs :: Vec a k)) = pS x xs (go @k xs) type ElimPropVec :: forall a. forall (p :: Nat ~> Prop)