diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,11 @@ +## 0.7 [2020.03.25] +* Require `singletons-2.7` and GHC 8.10. +* Add experimental support for generating type-level eliminators through the + `deriveTypeElim` and `deriveTypeElimNamed` functions. +* Add eliminators for `All`, `Any`, `Arg`, `Const`, `Down`, `Dual`, `First`, + `Identity`, `Last`, `Max`, `Min`, `Option`, `Product`, `Sum`, + and `WrappedMonoid`. + ## 0.6 [2019.08.27] * Require `singletons-2.6` and GHC 8.8. diff --git a/eliminators.cabal b/eliminators.cabal --- a/eliminators.cabal +++ b/eliminators.cabal @@ -1,5 +1,5 @@ name: eliminators -version: 0.6 +version: 0.7 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 == 8.8.1 +tested-with: GHC == 8.10.1 source-repository head type: git @@ -26,13 +26,13 @@ exposed-modules: Data.Eliminator Data.Eliminator.TH Data.Eliminator.TypeNats - build-depends: base >= 4.13 && < 4.14 - , extra >= 1.4.2 && < 1.7 - , singletons >= 2.6 && < 2.7 + build-depends: base >= 4.14 && < 4.15 + , extra >= 1.4.2 && < 1.8 + , singletons >= 2.7 && < 2.8 , singleton-nats >= 0.4.2 && < 0.5 - , template-haskell >= 2.15 && < 2.16 + , template-haskell >= 2.16 && < 2.17 , th-abstraction >= 0.3 && < 0.4 - , th-desugar >= 1.10 && < 1.11 + , th-desugar >= 1.11 && < 1.12 hs-source-dirs: src default-language: Haskell2010 ghc-options: -Wall -Wcompat -Wno-unticked-promoted-constructors @@ -46,14 +46,16 @@ EqualityTypes GADTSpec Internal + MatchabilizeSpec + MatchabilizeTypes ListSpec ListTypes VecTypes VecSpec - build-depends: base >= 4.13 && < 4.14 + build-depends: base >= 4.14 && < 4.15 , eliminators , hspec >= 2 && < 3 - , singletons >= 2.6 && < 2.7 + , singletons >= 2.7 && < 2.8 , 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 @@ -7,11 +7,13 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} {-| Module: Data.Eliminator Copyright: (C) 2017 Ryan Scott @@ -25,32 +27,89 @@ module Data.Eliminator ( -- * Eliminator functions -- $eliminators - elimBool + elimAll + , ElimAll + , elimAny + , ElimAny + , elimArg + , ElimArg + , elimBool + , ElimBool + , elimConst + , ElimConst + , elimDown + , ElimDown + , elimDual + , ElimDual , elimEither + , ElimEither + , elimFirst + , ElimFirst + , elimIdentity + , ElimIdentity + , elimLast + , ElimLast , elimList + , ElimList + , elimMax + , ElimMax , elimMaybe + , ElimMaybe + , elimMin + , ElimMin , elimNat + , ElimNat , elimNonEmpty + , ElimNonEmpty + , elimOption + , ElimOption , elimOrdering + , ElimOrdering + , elimProduct + , ElimProduct + , elimSum + , ElimSum , elimTuple0 + , ElimTuple0 , elimTuple2 + , ElimTuple2 , elimTuple3 + , ElimTuple3 , elimTuple4 + , ElimTuple4 , elimTuple5 + , ElimTuple5 , elimTuple6 + , ElimTuple6 , elimTuple7 + , ElimTuple7 , elimVoid + , ElimVoid + , elimWrappedMonoid + , ElimWrappedMonoid ) where import Control.Monad.Extra import Data.Eliminator.TH +import Data.Functor.Const (Const(..)) +import Data.Functor.Identity (Identity(..)) import Data.List.NonEmpty (NonEmpty(..)) +import Data.Monoid hiding (First, Last) import Data.Nat -import Data.Singletons.Prelude +import Data.Ord (Down(..)) +import Data.Semigroup +import Data.Singletons.Prelude hiding + (All, Any, Const, Last, Min, Max, Product, Sum) +import Data.Singletons.Prelude.Const (SConst(..)) +import Data.Singletons.Prelude.Identity (SIdentity(..)) import Data.Singletons.Prelude.List.NonEmpty (SNonEmpty(..)) +import Data.Singletons.Prelude.Monoid hiding (SFirst, SLast) +import Data.Singletons.Prelude.Ord (SDown(..)) +import Data.Singletons.Prelude.Semigroup import Data.Void (Void) +import Language.Haskell.TH (nameBase) import Language.Haskell.TH.Desugar (tupleNameDegree_maybe) {- $eliminators @@ -69,8 +128,37 @@ with @~>@ prepended. -} -$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''Nat, ''NonEmpty, ''Ordering, ''Void]) -$(deriveElimNamed "elimList" ''[]) -$(concatMapM (\n -> let Just deg = tupleNameDegree_maybe n - in deriveElimNamed ("elimTuple" ++ show deg) n) +$(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n) + [ ''All + , ''Any + , ''Arg + , ''Bool + , ''Const + , ''Down + , ''Dual + , ''Either + , ''First + , ''Identity + , ''Last + , ''Max + , ''Maybe + , ''Min + , ''Nat + , ''NonEmpty + , ''Option + , ''Ordering + , ''Product + , ''Sum + , ''Void + , ''WrappedMonoid + ]) +$(deriveElimNamed "elimList" ''[]) +$(deriveTypeElimNamed "ElimList" ''[]) +$(concatMapM (\n -> do deg <- fromMaybeM (fail $ "Internal error: " + ++ nameBase n + ++ " is not the name of a tuple") + (pure $ tupleNameDegree_maybe n) + terms <- deriveElimNamed ("elimTuple" ++ show deg) n + types <- deriveTypeElimNamed ("ElimTuple" ++ show deg) n + pure $ terms ++ types) [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)]) 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 @@ -1,4 +1,7 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE Unsafe #-} {-| Module: Data.Eliminator.TH @@ -12,25 +15,32 @@ -} module Data.Eliminator.TH ( -- * Eliminator generation - -- $conventions + -- ** Term-level eliminators + -- $term-conventions deriveElim , deriveElimNamed + -- ** Type-level eliminators + -- $type-conventions + , deriveTypeElim + , deriveTypeElimNamed ) where import Control.Applicative import Control.Monad -import Data.Char (isUpper) +import Data.Char (isLetter, isUpper, toUpper) import Data.Foldable import qualified Data.Kind as Kind (Type) import Data.Maybe +import Data.Proxy import Data.Singletons.Prelude +import Data.Singletons.TH.Options import Language.Haskell.TH import Language.Haskell.TH.Datatype import Language.Haskell.TH.Desugar hiding (NewOrData(..)) -{- $conventions +{- $term-conventions 'deriveElim' and 'deriveElimNamed' provide a way to automate the creation of eliminator functions, which are mostly boilerplate. Here is a complete example showing how one might use 'deriveElim': @@ -134,7 +144,6 @@ -- | @'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. @@ -147,7 +156,123 @@ -- | @'deriveElimNamed' funName dataName@ generates a top-level elimination -- function named @funName@ for the datatype @dataName@. deriveElimNamed :: String -> Name -> Q [Dec] -deriveElimNamed funName dataName = do +deriveElimNamed = deriveElimNamed' (Proxy @IsTerm) + +{- $type-conventions +'deriveTypeElim' and 'deriveTypeElimNamed' are like 'deriveElim' and +'deriveElimNamed' except that they create /type/-level eliminators instead of +term-level ones. Here is an example showing how one might use +'deriveTypeElim': + +@ +data MyList a = MyNil | MyCons a (MyList a) +$('deriveTypeElim' ''MyList) +@ + +This will produce an eliminator function that looks roughly like the following: + +@ +type ElimMyList :: forall (a :: 'Type'). + forall (p :: MyList a '~>' 'Type') (l :: MyList a) + -> 'Apply' p MyNil + -> (forall (x :: a) (xs :: MyList a) + -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs)) + -> 'Apply' p l +type family ElimMyList p l pMyNil pMyCons where + forall (a :: 'Type') + (p :: MyList a ~> 'Type') + (pMyNil :: 'Apply' p MyNil) + (pMyCons :: forall (x :: a) (xs :: MyList a) + -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs)). + ElimMyList @a p MyNil pMyNil pMyCons = + pMyNil + forall (a :: 'Type') + (p :: MyList a ~> 'Type') + (_pMyNil :: 'Apply' p MyNil) + (pMyCons :: forall (x :: a) (xs :: MyList a) + -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs)) + x' xs'. + ElimMyList @a p (MyCons x' xs') pMyNil pMyCons = + 'Apply' (pMyCons x' xs') (ElimMyList @a p xs' pMyNil pMyCons) +@ + +Note the following differences from a term-level eliminator that 'deriveElim' +would generate: + +* Type-level eliminators do not use 'Sing'. Instead, they use visible dependent + quantification. That is, instead of generating + @forall (x :: a). Sing x -> ...@ (as a term-level eliminator would do), a + type-level eliminator would use @forall (x :: a) -> ...@. + +* Term-level eliminators quantify @p@ with an invisible @forall@, whereas + type-level eliminators quantify @p@ with a visible @forall@. (Really, @p@ + ought to be quantified visibly in both forms of eliminator, but GHC does not + yet support visible dependent quantification at the term level.) + +* Type-level eliminators use ('~>') in certain places where (@->@) would appear + in term-level eliminators. For instance, note the use of + @'Apply' p xs '~>' 'Apply' p (MyCons x xs)@ in @ElimMyList@ above. This is + done to make it easier to use type-level eliminators with defunctionalization + symbols (which aren't necessary for term-level eliminators). + + This comes with a notable drawback: type-level eliminators cannot support + data constructors where recursive occurrences of the data type appear in a + position other than the last field of a constructor. In other words, + 'deriveTypeElim' works on the @MyList@ example above, but not this variant: + + @ + data SnocList a = SnocNil | SnocCons (SnocList a) a + @ + + This is because @$('deriveTypeElim' ''SnocList)@ would generate an eliminator + with the following kind: + + @ + type ElimSnocList :: forall (a :: 'Type'). + forall (p :: SnocList a '~>' 'Type') (l :: SnocList a) + -> 'Apply' p SnocNil + -> (forall (xs :: SnocList a) -> 'Apply' p xs + '~>' (forall (x :: a) -> 'Apply' p (SnocCons x xs))) + -> 'Apply' p l + @ + + Unfortunately, the kind + @'Apply' p xs '~>' (forall (x :: a) -> 'Apply' p (SnocCons x xs))@ is + impredicative. + +* In addition to the language extensions that 'deriveElim' requires, you'll need + to enable these extensions in order to use 'deriveTypeElim': + + * @StandaloneKindSignatures@ + + * @UndecidableInstances@ +-} + +-- | @'deriveTypeElim' dataName@ generates a type-level eliminator for the +-- datatype @dataName@. The eliminator will follow these naming conventions: +-- +-- * 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. +deriveTypeElim :: Name -> Q [Dec] +deriveTypeElim dataName = deriveTypeElimNamed (upcase (eliminatorName dataName)) dataName + +-- | @'deriveTypeElimNamed' funName dataName@ generates a type-level eliminator +-- named @funName@ for the datatype @dataName@. +deriveTypeElimNamed :: String -> Name -> Q [Dec] +deriveTypeElimNamed = deriveElimNamed' (Proxy @IsType) + +-- The workhorse for deriveElim(Named). This generates either a term- or +-- type-level eliminator, depending on which Eliminator instance is used. +deriveElimNamed' :: + Eliminator t + => proxy t + -> String -- The name of the eliminator function + -> 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 @@ -161,32 +286,29 @@ Newtype -> pure () predVar <- newName "p" singVar <- newName "s" - let elimN = mkName funName + let elimName = mkName funName promDataKind = datatypeType info predVarBndr = KindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type)) singVarBndr = KindedTV singVar promDataKind - caseTypes <- traverse (caseType dataName predVar) cons + caseTypes <- traverse (caseType prox 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] + elimType = elimTypeSig prox dataVarBndrs predVarBndr singVarBndr + caseTypes returnType + elimEqns <- qElimEqns prox (mkName funName) dataName + dataVarBndrs predVarBndr singVarBndr + caseTypes cons + pure [elimSigD prox elimName elimType, elimEqns] -caseType :: Name -> Name -> ConstructorInfo -> Q Type -caseType dataName predVar +-- Generate the type for a "case alternative" in an eliminator function's type +-- signature, which is done on a constructor-by-constructor basis. +caseType :: + Eliminator t + => proxy t + -> Name -- The name of the data type + -> Name -- The predicate type variable + -> ConstructorInfo -- The data constructor + -> Q Type -- The full case type +caseType prox dataName predVar (ConstructorInfo { constructorName = conName , constructorVars = conVars , constructorContext = conContext @@ -199,19 +321,22 @@ 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)) + prependElimCaseTypeVar prox dataName predVar var varType t) returnType (zip vars fieldTypes) -caseClause :: Name -> Name -> [Name] -> Int -> Int - -> ConstructorInfo -> Q Clause -caseClause dataName elimN bndrNamesPrefix conIndex numCons +-- Generate a single clause for a term-level eliminator. +caseClause :: + Name -- The name of the eliminator function + -> Name -- The name of the data type + -> [TyVarBndr] -- The type variables bound by the data type + -> TyVarBndr -- The predicate type variable + -> Int -- The index of this constructor (0-indexed) + -> Int -- The total number of data constructors + -> ConstructorInfo -- The data constructor + -> Q Clause -- The generated function clause +caseClause elimName dataName dataVarBndrs predVarBndr conIndex numCons (ConstructorInfo { constructorName = conName , constructorFields = fieldTypes }) = do let numFields = length fieldTypes @@ -222,26 +347,170 @@ if i == conIndex then pure usedCaseVar else newName ("_p" ++ show i) - let singConName = singDataConName conName + let singConName = singledDataConName defaultOptions 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 + 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 mkArg f (singVar, singVarSig, varType) = - foldExp f $ VarE singVar - : maybeToList (mbInductiveArg 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) (NormalB rhs) [] +-- Generate a single equation for a type-level eliminator. +-- +-- This code is fairly similar in structure to caseClause, but different +-- enough in subtle ways that I did not attempt to de-duplicate this code as +-- a method of the Eliminator class. +caseTySynEqn :: + Name -- The name of the eliminator function + -> Name -- The name of the data type + -> [TyVarBndr] -- The type variables bound by the data type + -> TyVarBndr -- The predicate type variable + -> Int -- The index of this constructor (0-indexed) + -> [Type] -- The types of each "case alternative" in the eliminator + -- function's type signature + -> ConstructorInfo -- The data constructor + -> Q TySynEqn -- The generated type family equation +caseTySynEqn elimName dataName dataVarBndrs predVarBndr conIndex caseTypes + (ConstructorInfo { constructorName = conName + , constructorFields = fieldTypes }) + = do let dataVarNames = map tvName dataVarBndrs + predVarName = tvName predVarBndr + numFields = length fieldTypes + singVars <- newNameList "s" numFields + usedCaseVar <- newName "useThis" + caseVarBndrs <- flip itraverse caseTypes $ \i caseTy -> + let mkVarName + | i == conIndex = pure usedCaseVar + | otherwise = newName ("_p" ++ show i) + in liftA2 KindedTV mkVarName (pure caseTy) + let caseVarNames = map tvName caseVarBndrs + prefix = foldAppKindT (ConT elimName) $ map VarT dataVarNames + mbInductiveArg singVar varType = + let inductiveArg = foldAppT prefix $ VarT predVarName + : VarT singVar + : map VarT caseVarNames + in mbInductiveCase dataName varType inductiveArg + mkArg f (singVar, varType) = + foldAppDefunT (f `AppT` VarT singVar) + $ maybeToList (mbInductiveArg singVar varType) + bndrs = dataVarBndrs ++ predVarBndr : caseVarBndrs ++ map PlainTV singVars + lhs = foldAppT prefix $ VarT predVarName + : foldAppT (ConT conName) (map VarT singVars) + : map VarT caseVarNames + rhs = foldl' mkArg (VarT usedCaseVar) $ zip singVars fieldTypes + pure $ TySynEqn (Just bndrs) lhs rhs + +-- Are we dealing with a term or a type? +data TermOrType + = IsTerm + | IsType + +-- A class that abstracts out certain common operations that one must perform +-- for both term- and type-level eliminators. +class Eliminator (t :: TermOrType) where + -- Create the Dec for an eliminator function's type signature. + elimSigD :: + proxy t + -> Name -- The name of the eliminator function + -> Type -- The type of the eliminator function + -> Dec -- The type signature Dec (SigD or KiSigD) + + -- Create an eliminator function's type. + elimTypeSig :: + proxy t + -> [TyVarBndr] -- The type variables bound by the data type + -> TyVarBndr -- The predicate type variable + -> TyVarBndr -- The type variable whose kind is that of the data type itself + -> [Type] -- The types of each "case alternative" in the eliminator + -- function's type signature + -> Type -- The eliminator function's return type + -> Type -- The full type + + -- Take a data constructor's field type and prepend it to a "case + -- alternative" in an eliminator function's type signature. + prependElimCaseTypeVar :: + proxy t + -> Name -- The name of the data type + -> Name -- The predicate type variable + -> Name -- A fresh type variable name + -> Kind -- The field type + -> Type -- The rest of the "case alternative" type + -> Type -- The "case alternative" type after prepending + + -- Generate the clauses/equations for the body of the eliminator function. + qElimEqns :: + proxy t + -> Name -- The name of the eliminator function + -> Name -- The name of the data type + -> [TyVarBndr] -- The type variables bound by the data type + -> TyVarBndr -- The predicate type variable + -> TyVarBndr -- The type variable whose kind is that of the data type itself + -> [Type] -- The types of each "case alternative" in the eliminator + -- function's type signature + -> [ConstructorInfo] -- The data constructors + -> Q Dec -- The Dec containing the clauses/equations + +instance Eliminator IsTerm where + elimSigD _ = SigD + + elimTypeSig _ dataVarBndrs predVarBndr singVarBndr caseTypes returnType = + ForallT (dataVarBndrs ++ [predVarBndr, singVarBndr]) [] $ + ravel (singType (tvName singVarBndr):caseTypes) returnType + + prependElimCaseTypeVar _ dataName predVar var varType t = + ForallT [KindedTV 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 + +instance Eliminator IsType where + elimSigD _ = KiSigD + + elimTypeSig _ dataVarBndrs predVarBndr singVarBndr caseTypes returnType = + ForallT dataVarBndrs [] $ + ForallVisT [predVarBndr, singVarBndr] $ + ravel caseTypes returnType + + prependElimCaseTypeVar _ dataName predVar var varType t = + ForallVisT [KindedTV var varType] $ + ravelDefun (maybeToList (mbInductiveType dataName predVar var varType)) t + + qElimEqns _ elimName dataName dataVarBndrs predVarBndr singVarBndr caseTypes cons = do + caseVarBndrs <- replicateM (length caseTypes) (PlainTV <$> newName "p") + let predVar = tvName predVarBndr + singVar = tvName singVarBndr + tyFamHead = TypeFamilyHead elimName + (PlainTV predVar:PlainTV singVar:caseVarBndrs) + NoSig Nothing + caseEqns <- itraverse (\i -> caseTySynEqn elimName dataName + dataVarBndrs predVarBndr i caseTypes) cons + pure $ ClosedTypeFamilyD tyFamHead caseEqns + +mbInductiveType :: Name -> Name -> Name -> Kind -> Maybe Type +mbInductiveType dataName predVar var varType = + mbInductiveCase dataName varType $ predType predVar $ VarT var + -- TODO: Rule out polymorphic recursion mbInductiveCase :: Name -> Type -> a -> Maybe a mbInductiveCase dataName varType inductiveArg @@ -271,6 +540,7 @@ newNameList :: String -> Int -> Q [Name] newNameList prefix n = ireplicateA n $ newName . (prefix ++) . show +-- Compute an eliminator function's name from the data type name. eliminatorName :: Name -> String eliminatorName n | first:_ <- nStr @@ -282,23 +552,41 @@ where nStr = nameBase n --- Reconstruct and arrow type from the list of types +-- Construct a function type, separating the arguments with -> ravel :: [Type] -> Type -> Type -ravel [] res = res -ravel (h:t) res = AppT (AppT ArrowT h) (ravel t res) +ravel args res = go args + where + go [] = res + go (h:t) = AppT (AppT ArrowT h) (go t) --- apply an expression to a list of expressions -foldExp :: Exp -> [Exp] -> Exp -foldExp = foldl' AppE +-- Construct a function type, separating the arguments with ~> +ravelDefun :: [Type] -> Type -> Type +ravelDefun args res = go args + where + go [] = res + go (h:t) = AppT (AppT (ConT ''(~>)) h) (go t) --- apply an expression to a list of types -foldAppType :: Exp -> [Type] -> Exp -foldAppType = foldl' AppTypeE +-- Apply an expression to a list of expressions using ordinary function applications. +foldAppE :: Exp -> [Exp] -> Exp +foldAppE = foldl' AppE -tyVarBndrName :: TyVarBndr -> Name -tyVarBndrName (PlainTV n) = n -tyVarBndrName (KindedTV n _) = n +-- 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 + +-- Apply a type to a list of types using defunctionalized applications +-- (i.e., using Apply from singletons). +foldAppDefunT :: Type -> [Type] -> Type +foldAppDefunT = foldl' (\x y -> ConT ''Apply `AppT` x `AppT` y) + +-- Apply a type to a list of types using visible kind applications. +foldAppKindT :: Type -> [Type] -> Type +foldAppKindT = foldl' AppKindT + itraverse :: Applicative f => (Int -> a -> f b) -> [a] -> f [b] itraverse f xs0 = go xs0 0 where go [] _ = pure [] @@ -316,24 +604,18 @@ -- 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 = prefixConName "S" "%" nm +-- Make an identifier uppercase. If the identifier is infix, this acts as the +-- identity function. +upcase :: String -> String +upcase str + | isHsLetter first + = toUpper first : tail str -mkTupleDataName :: Int -> Name -mkTupleDataName n = mkName $ "STuple" ++ (show n) + | otherwise + = str + where + first = head str --- Put an uppercase prefix on a constructor name. Takes two prefixes: --- one for identifiers and one for symbols. --- --- This is different from 'prefixName' in that infix constructor names always --- start with a colon, so we must insert the prefix after the colon in order --- for the new name to be syntactically valid. -prefixConName :: String -> String -> Name -> Name -prefixConName pre tyPre n = case (nameBase n) of - (':' : rest) -> mkName (':' : tyPre ++ rest) - alpha -> mkName (pre ++ alpha) +-- is it a letter or underscore? +isHsLetter :: Char -> Bool +isHsLetter c = isLetter c || c == '_' diff --git a/tests/DecideTypes.hs b/tests/DecideTypes.hs --- a/tests/DecideTypes.hs +++ b/tests/DecideTypes.hs @@ -5,6 +5,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} @@ -12,13 +13,16 @@ {-# LANGUAGE UndecidableInstances #-} module DecideTypes where +import Data.Eliminator import Data.Kind import Data.Nat +import Data.Singletons.Prelude import Data.Singletons.TH hiding (Decision(..)) -- Due to https://github.com/goldfirere/singletons/issues/82, promoting the -- Decision data type from Data.Singletons.Decide is a tad awkward. To work -- around these, we define a more general Decision' data type here. +type Decision' :: (Type ~> Type ~> Type) -> Type -> Type data Decision' p a = Proved a | Disproved (p @@ a @@ Void) @@ -31,16 +35,36 @@ elimDecision (SProved yes) pProved _ = pProved yes elimDecision (SDisproved no) _ pDisproved = pDisproved no +type ElimDecision :: forall a. + forall (p :: PDecision a ~> Type) + (d :: PDecision a) -> + (forall (yes :: a) -> p @@ Proved yes) + -> (forall (no :: a ~> Void) -> p @@ Disproved no) + -> p @@ d +type family ElimDecision p d pProved pDisproved where + forall a (p :: PDecision a ~> Type) + (pProved :: forall (yes :: a) -> p @@ Proved yes) + (pDisproved :: forall (no :: a ~> Void) -> p @@ Disproved no) yes. + ElimDecision p (Proved yes) pProved pDisproved = pProved yes + forall a (p :: PDecision a ~> Type) + (pProved :: forall (yes :: a) -> p @@ Proved yes) + (pDisproved :: forall (no :: a ~> Void) -> p @@ Disproved no) no. + ElimDecision p (Disproved no) pProved pDisproved = pDisproved no + instance Show a => Show (Decision' p a) where showsPrec p (Proved a) = showParen (p > 10) $ showString "Proved " . showsPrec 11 a showsPrec p (Disproved _) = showParen (p > 10) $ showString "Disproved " +type Decision :: Type -> Type type Decision = Decision' (TyCon (->)) + +type PDecision :: Type -> Type type PDecision = Decision' (~>@#@$) -data SDecision :: forall a. PDecision a -> Type where +type SDecision :: PDecision a -> Type +data SDecision d where SProved :: forall a (x :: a). Sing x -> SDecision (Proved x) SDisproved :: forall a (r :: a ~> Void). Sing r -> SDecision (Disproved r) type instance Sing = SDecision @@ -56,36 +80,80 @@ -- These newtype wrappers are needed to work around -- https://gitlab.haskell.org/ghc/ghc/issues/9269 -newtype WhyDecEqNat (k :: Nat) = WhyDecEqNat +type WhyDecEqNat :: Nat -> Type +newtype WhyDecEqNat k = WhyDecEqNat { runWhyDecEqNat :: forall (j :: Nat). Sing j -> Decision (k :~: j) } + +type WhyDecEqList :: [e] -> Type newtype WhyDecEqList (l1 :: [e]) = WhyDecEqList { runWhyDecEqList :: forall (l2 :: [e]). Sing l2 -> Decision (l1 :~: l2) } $(singletons [d| - type family NatEqConsequences (a :: Nat) (b :: Nat) :: Type where - NatEqConsequences Z Z = () - NatEqConsequences Z (S _) = Void - NatEqConsequences (S _) Z = Void - NatEqConsequences (S k1) (S k2) = k1 :~: k2 + type ConstVoidNat :: forall (m :: Nat) -> Const Type m -> Const Type (S m) + type ConstVoidNat m r = Void - type WhyNatEqConsequencesSame (a :: Nat) = NatEqConsequences a a + type EqSameNat :: Nat -> forall (m :: Nat) -> Const Type m -> Const Type (S m) + type EqSameNat n m r = n :~: m - type WhyDecEqZ (k :: Nat) = Decision (Z :~: k) + type ConstVoidList :: forall e. forall (y :: e) (ys :: [e]) + -> Const Type ys -> Const Type (y:ys) + type ConstVoidList y ys r = Void - type WhyDecEqS (n :: Nat) (k :: Nat) = Decision (S n :~: k) + 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 family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where - ListEqConsequences '[] '[] = () - ListEqConsequences '[] (_:_) = Void - ListEqConsequences (_:_) '[] = Void - ListEqConsequences (x:xs) (y:ys) = (x :~: y, xs :~: ys) +$(singletons [d| + type NatEqConsequencesBase :: Nat -> Type + type NatEqConsequencesBase m = ElimNat (ConstSym1 Type) m () ConstVoidNatSym1 - type WhyListEqConsequencesSame (es :: [e]) = ListEqConsequences es es + 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 WhyDecEqNil (es :: [e]) = Decision ('[] :~: es) + type ListEqConsequencesBase :: [e] -> Type + type ListEqConsequencesBase ys = ElimList (ConstSym1 Type) ys () ConstVoidListSym2 - type WhyDecEqCons (x :: e) (xs :: [e]) (es :: [e]) = Decision ((x:xs) :~: es) + 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 WhyIntermixListEqs1 (x :: e) (xs :: [e]) (ys :: [e]) (k :: e) = (x:xs) :~: (k:ys) - type WhyIntermixListEqs2 (x :: e) (xs :: [e]) (k :: [e]) = (x:xs) :~: (x:k) +$(singletons [d| + type NatEqConsequences :: Nat -> Nat -> Type + type NatEqConsequences n m = + ElimNat (ConstSym1 (Nat ~> Type)) n + NatEqConsequencesBaseSym0 + NatEqConsequencesStepSym1 @@ m + + type WhyNatEqConsequencesSame :: Nat -> Type + type WhyNatEqConsequencesSame a = NatEqConsequences a a + + type WhyDecEqZ :: Nat -> Type + type WhyDecEqZ k = Decision (Z :~: k) + + type WhyDecEqS :: Nat -> Nat -> Type + type WhyDecEqS n k = Decision (S n :~: k) + + type ListEqConsequences :: [e] -> [e] -> Type + type ListEqConsequences (xs :: [e]) (ys :: [e]) = + ElimList (ConstSym1 ([e] ~> Type)) xs + ListEqConsequencesBaseSym0 + ListEqConsequencesStepSym2 @@ ys + + type WhyListEqConsequencesSame :: [e] -> Type + type WhyListEqConsequencesSame es = ListEqConsequences es es + + type WhyDecEqNil :: [e] -> Type + type WhyDecEqNil es = Decision ('[] :~: es) + + type WhyDecEqCons :: e -> [e] -> [e] -> Type + type WhyDecEqCons x xs es = Decision ((x:xs) :~: es) + + type WhyIntermixListEqs1 :: e -> [e] -> [e] -> e -> Type + type WhyIntermixListEqs1 x xs ys k = (x:xs) :~: (k:ys) + + type WhyIntermixListEqs2 :: e -> [e] -> [e] -> Type + type WhyIntermixListEqs2 x xs k = (x:xs) :~: (x:k) |]) diff --git a/tests/EqualitySpec.hs b/tests/EqualitySpec.hs --- a/tests/EqualitySpec.hs +++ b/tests/EqualitySpec.hs @@ -86,41 +86,41 @@ sym :: forall t (a :: t) (b :: t). a :~: b -> b :~: a sym eq = withSomeSing eq $ \(singEq :: Sing r) -> - (~>:~:) @t @a @(WhySymSym1 a) @b @r singEq Refl + (~>:~:) @t @a @WhySymSym0 @b @r singEq Refl sSym :: forall t (a :: t) (b :: t) (e :: a :~: b). Sing e -> Sing (Symmetry e) -sSym se = (~>:~:) @t @a @(WhySSymSym1 a) @b @e se SRefl +sSym se = (~>:~:) @t @a @WhySSymSym0 @b @e se SRefl hsym :: forall j k (a :: j) (b :: k). a :~~: b -> b :~~: a hsym eq = withSomeSing eq $ \(singEq :: Sing r) -> - (~>:~~:) @j @a @(WhyHSymSym1 a) @k @b @r singEq HRefl + (~>:~~:) @j @a @WhyHSymSym0 @k @b @r singEq HRefl sHSym :: forall j k (a :: j) (b :: k) (e :: a :~~: b). Sing e -> Sing (HSymmetry e) -sHSym se = (~>:~~:) @j @a @(WhySHSymSym1 a) @k @b @e se SHRefl +sHSym se = (~>:~~:) @j @a @WhySHSymSym0 @k @b @e se SHRefl symIdempotent :: forall t (a :: t) (b :: t) (e :: a :~: b). Sing e -> Symmetry (Symmetry e) :~: e -symIdempotent se = (~>:~:) @t @a @(WhySymIdempotentSym1 a) @b @e se Refl +symIdempotent se = (~>:~:) @t @a @WhySymIdempotentSym0 @b @e se Refl hsymIdempotent :: forall j k (a :: j) (b :: k) (e :: a :~~: b). Sing e -> HSymmetry (HSymmetry e) :~: e -hsymIdempotent se = (~>:~~:) @j @a @(WhyHSymIdempotentSym1 a) @k @b @e se Refl +hsymIdempotent se = (~>:~~:) @j @a @WhyHSymIdempotentSym0 @k @b @e se Refl trans :: forall t (a :: t) (b :: t) (c :: t). a :~: b -> b :~: c -> a :~: c trans eq1 eq2 = withSomeSing eq1 $ \(singEq1 :: Sing r) -> - unwrapTrans ((~>:~:) @t @a @(WhyTransSym1 a) @b @r + unwrapTrans ((~>:~:) @t @a @WrappedTransSym0 @b @r singEq1 (WrapTrans id)) eq2 htrans :: forall j k l (a :: j) (b :: k) (c :: l). a :~~: b -> b :~~: c -> a :~~: c htrans eq1 eq2 = withSomeSing eq1 $ \(singEq1 :: Sing r) -> - unwrapHTrans ((~>:~~:) @j @a @(WhyHTransSym1 a) @k @b @r + unwrapHTrans ((~>:~~:) @j @a @WrappedHTransSym0 @k @b @r singEq1 (WrapHTrans id)) eq2 replace :: forall t (from :: t) (to :: t) (p :: t ~> Type). @@ -158,45 +158,45 @@ -> f @@ a :~: f @@ b cong eq = withSomeSing eq $ \(singEq :: Sing r) -> - (~>:~:) @x @a @(WhyCongSym2 f a) @b @r singEq Refl + (~>:~:) @x @a @(WhyCongSym1 f) @b @r singEq Refl eqIsRefl :: forall k (a :: k) (b :: k) (e :: a :~: b). Sing e -> e :~~: (Refl :: a :~: a) -eqIsRefl eq = (~>:~:) @k @a @(WhyEqIsReflSym1 a) @b @e eq HRefl +eqIsRefl eq = (~>:~:) @k @a @WhyEqIsReflSym0 @b @e eq HRefl heqIsHRefl :: forall j k (a :: j) (b :: k) (e :: a :~~: b). Sing e -> e :~~: (HRefl :: a :~~: a) -heqIsHRefl heq = (~>:~~:) @j @a @(WhyHEqIsHReflSym1 a) @k @b @e heq HRefl +heqIsHRefl heq = (~>:~~:) @j @a @WhyHEqIsHReflSym0 @k @b @e heq HRefl transLeft :: forall j (a :: j) (b :: j) (e :: a :~: b). Sing e -> Trans e Refl :~: e -transLeft se = leibniz @(a :~: b) @(WhyTransLeftSym1 a) +transLeft se = leibniz @(a :~: b) @WhyTransLeftSym0 @(Symmetry (Symmetry e)) @e (symIdempotent se) transLeftHelper where transLeftHelper :: Trans (Symmetry (Symmetry e)) Refl :~: Symmetry (Symmetry e) - transLeftHelper = (~>:~:) @j @b @(WhyTransLeftHelperSym1 b) @a @(Symmetry e) + transLeftHelper = (~>:~:) @j @b @WhyTransLeftHelperSym0 @a @(Symmetry e) (sSym se) Refl htransLeft :: forall j k (a :: j) (b :: k) (e :: a :~~: b). Sing e -> HTrans e HRefl :~: e -htransLeft se = leibniz @(a :~~: b) @(WhyHTransLeftSym1 a) +htransLeft se = leibniz @(a :~~: b) @WhyHTransLeftSym0 @(HSymmetry (HSymmetry e)) @e (hsymIdempotent se) htransLeftHelper where htransLeftHelper :: HTrans (HSymmetry (HSymmetry e)) HRefl :~: HSymmetry (HSymmetry e) - htransLeftHelper = (~>:~~:) @k @b @(WhyHTransLeftHelperSym1 b) @j @a @(HSymmetry e) + htransLeftHelper = (~>:~~:) @k @b @WhyHTransLeftHelperSym0 @j @a @(HSymmetry e) (sHSym se) Refl transRight :: forall j (a :: j) (b :: j) (e :: a :~: b). Sing e -> Trans Refl e :~: e -transRight se = (~>:~:) @j @a @(WhyTransRightSym1 a) @b @e se Refl +transRight se = (~>:~:) @j @a @WhyTransRightSym0 @b @e se Refl htransRight :: forall j k (a :: j) (b :: k) (e :: a :~~: b). Sing e -> HTrans HRefl e :~: e -htransRight se = (~>:~~:) @j @a @(WhyHTransRightSym1 a) @k @b @e se Refl +htransRight se = (~>:~~:) @j @a @WhyHTransRightSym0 @k @b @e se Refl -- Commented out for now, since these take ages to compile :( -- Perhaps https://gitlab.haskell.org/ghc/ghc/merge_requests/611 will make @@ -205,7 +205,7 @@ sTrans :: forall t (a :: t) (b :: t) (c :: t) (e1 :: a :~: b) (e2 :: b :~: c). Sing e1 -> Sing e2 -> Sing (Trans e1 e2) -sTrans se1 = unwrapSTrans $ (~>:~:) @t @a @(WhySTransSym1 a) @b @e1 +sTrans se1 = unwrapSTrans $ (~>:~:) @t @a @WhySTransSym0 @b @e1 se1 (WrapSTrans sTransHelper) where sTransHelper :: forall (z :: t) (e' :: a :~: z). @@ -216,7 +216,7 @@ sHTrans :: forall j k l (a :: j) (b :: k) (c :: l) (e1 :: a :~~: b) (e2 :: b :~~: c). Sing e1 -> Sing e2 -> Sing (HTrans e1 e2) -sHTrans se1 = unwrapSHTrans $ (~>:~~:) @j @a @(WhySHTransSym1 a) @k @b @e1 +sHTrans se1 = unwrapSHTrans $ (~>:~~:) @j @a @WhySHTransSym0 @k @b @e1 se1 (WrapSHTrans sHTransHelper) where sHTransHelper :: forall m (z :: m) (e' :: a :~~: z). diff --git a/tests/EqualityTypes.hs b/tests/EqualityTypes.hs --- a/tests/EqualityTypes.hs +++ b/tests/EqualityTypes.hs @@ -4,6 +4,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} @@ -18,7 +19,8 @@ import Internal -data (%:~:) :: forall k (a :: k) (b :: k). a :~: b -> Type where +type (%:~:) :: a :~: b -> Type +data (%:~:) e where SRefl :: (%:~:) Refl type instance Sing = (%:~:) @@ -39,6 +41,18 @@ -> p @@ r (~>:~:) SRefl pRefl = pRefl +type (~>:~:) :: forall k (a :: k). + forall (p :: forall (y :: k). a :~: y ~> Type) + -> forall (b :: k). + forall (r :: a :~: b) + -> p @@ Refl + -> p @@ r +type family (~>:~:) p r pRefl where + forall k (a :: k) + (p :: forall (y :: k). a :~: y ~> Type) + (pRefl :: p @@ Refl). + (~>:~:) p Refl pRefl = pRefl + (~>!:~:) :: forall k (a :: k) (p :: k ~> Prop) (b :: k). @@ -47,7 +61,17 @@ -> p @@ b (~>!:~:) Refl pRefl = pRefl -data (%:~~:) :: forall j k (a :: j) (b :: k). a :~~: b -> Type where +type (~>!:~:) :: forall k (a :: k). + forall (p :: k ~> Prop) + -> forall (b :: k). + a :~: b + -> p @@ a + -> p @@ b +type family (~>!:~:) p r pRefl where + (~>!:~:) _ Refl pRefl = pRefl + +type (%:~~:) :: forall j k (a :: j) (b :: k). a :~~: b -> Type +data (%:~~:) e where SHRefl :: (%:~~:) HRefl type instance Sing = (%:~~:) @@ -68,6 +92,18 @@ -> p @@ r (~>:~~:) SHRefl pHRefl = pHRefl +type (~>:~~:) :: forall j (a :: j). + forall (p :: forall z (y :: z). a :~~: y ~> Type) + -> forall k (b :: k). + forall (r :: a :~~: b) + -> p @@ HRefl + -> p @@ r +type family (~>:~~:) p r pHRefl where + forall j (a :: j) + (p :: forall z (y :: z). a :~~: y ~> Type) + (pHRefl :: p @@ HRefl). + (~>:~~:) p HRefl pHRefl = pHRefl + (~>!:~~:) :: forall j (a :: j) (p :: forall z. z ~> Prop) k (b :: k). @@ -76,123 +112,233 @@ -> p @@ b (~>!:~~:) HRefl pHRefl = pHRefl +type (~>!:~~:) :: forall j (a :: j). + forall (p :: forall z. z ~> Prop) + -> forall k (b :: k). + a :~~: b + -> p @@ a + -> p @@ b +type family (~>!:~~:) p r pHRefl where + forall j (a :: j) + (p :: forall z. z ~> Prop) + (pHRefl :: p @@ a). + (~>!:~~:) p (HRefl :: a :~~: a) pHRefl = pHRefl + ----- -- These newtype wrappers are needed to work around -- https://gitlab.haskell.org/ghc/ghc/issues/9269 -newtype WrappedTrans (x :: k) (e :: x :~: y) = - WrapTrans { unwrapTrans :: forall (z :: k). y :~: z -> x :~: z } -newtype WrappedHTrans (x :: j) (e :: x :~~: (y :: k)) = - WrapHTrans { unwrapHTrans :: forall l (z :: l). y :~~: z -> x :~~: z } +type WrappedTrans' :: + (Type ~> Type ~> Type) -> forall k (x :: k) (y :: k). x :~: y -> Type +newtype WrappedTrans' p (e :: (x :: k) :~: y) = + WrapTrans (forall (z :: k). p @@ (y :~: z) @@ (x :~: z)) --- This is all needed to avoid impredicativity in the defunctionalization --- symbols for WhyHReplace and WhyHLeibniz. -newtype WrappedPred = WrapPred { unwrapPred :: forall z. z ~> Type } -type family UnwrapPred (wp :: WrappedPred) :: forall z. z ~> Type where - forall (uwp :: forall z. z ~> Type). UnwrapPred (WrapPred uwp) = uwp +type WrappedHTrans' :: + (Type ~> Type ~> Type) -> forall j (x :: j) k (y :: k). x :~~: y -> Type +newtype WrappedHTrans' p (e :: x :~~: y) = + WrapHTrans (forall l (z :: l). p @@ (y :~~: z) @@ (x :~~: z)) $(singletons [d| - type WhySym (a :: t) (e :: a :~: (y :: t)) = - y :~: a :: Type + type WrappedTrans :: forall k (x :: k) (y :: k). x :~: y -> Type + type WrappedTrans = WrappedTrans' (TyCon2 (->)) - type WhySSym (a :: t) (e :: a :~: (y :: t)) = - Sing (Symmetry e) :: Type + type PWrappedTrans :: forall k (x :: k) (y :: k). x :~: y -> Type + type PWrappedTrans = WrappedTrans' (~>@#@$) - type WhyHSym (a :: j) (e :: a :~~: (y :: z)) = - y :~~: a :: Type + type WrappedHTrans :: forall j (x :: j) k (y :: k). x :~~: y -> Type + type WrappedHTrans = WrappedHTrans' (TyCon2 (->)) - type WhySHSym (a :: j) (e :: a :~~: (y :: z)) = - Sing (HSymmetry e) :: Type + type PWrappedHTrans :: forall j (x :: j) k (y :: k). x :~~: y -> Type + type PWrappedHTrans = WrappedHTrans' (~>@#@$) + |]) - type family Symmetry (x :: (a :: k) :~: (b :: k)) :: b :~: a where - Symmetry Refl = Refl +unwrapTrans :: WrappedTrans (e :: (x :: k) :~: y) + -> forall (z :: k). y :~: z -> x :~: z +unwrapTrans (WrapTrans f) = f - type WhySymIdempotent (a :: t) (r :: a :~: (z :: t)) = - Symmetry (Symmetry r) :~: r :: Type +type UnwrapTrans :: + forall k (x :: k) (y :: k) (e :: x :~: y). + PWrappedTrans e -> forall (z :: k). y :~: z ~> x :~: z +type family UnwrapTrans wt :: forall z. y :~: z ~> x :~: z where + forall k (x :: k) (y :: k) (uwt :: forall (z :: k). y :~: z ~> x :~: z). + UnwrapTrans (WrapTrans uwt) = uwt - type family HSymmetry (x :: a :~~: b) :: b :~~: a where - HSymmetry HRefl = HRefl +unwrapHTrans :: WrappedHTrans (e :: x :~~: y) + -> forall l (z :: l). y :~~: z -> x :~~: z +unwrapHTrans (WrapHTrans f) = f - type WhyHSymIdempotent (a :: j) (r :: a :~~: (y :: z)) = - HSymmetry (HSymmetry r) :~: r :: Type +type UnwrapHTrans :: + forall j (x :: j) k (y :: k) (e :: x :~~: y). + PWrappedHTrans e -> forall l (z :: l). y :~~: z ~> x :~~: z +type family UnwrapHTrans wht :: forall l (z :: l). y :~~: z ~> x :~~: z where + forall j (x :: j) k (y :: k) (uwht :: forall l (z :: l). y :~~: z ~> x :~~: z). + UnwrapHTrans (WrapHTrans uwht) = uwht - type WhyTrans (x :: k) (e :: x :~: (y :: k)) = - WrappedTrans x e :: Type +-- This is all needed to avoid impredicativity in the defunctionalization +-- symbols for WhyHReplace and WhyHLeibniz. +type WrappedPred :: Type +newtype WrappedPred = WrapPred { unwrapPred :: forall z. z ~> Type } - type WhyHTrans (x :: j) (e :: x :~~: (y :: k)) = - WrappedHTrans x e :: Type +type UnwrapPred :: WrappedPred -> forall z. z ~> Type +type family UnwrapPred wp :: forall z. z ~> Type where + forall (uwp :: forall z. z ~> Type). UnwrapPred (WrapPred uwp) = uwp - type family Trans (x :: a :~: b) (y :: b :~: c) :: a :~: c where +$(singletons [d| + type WhySym :: forall t (a :: t) (y :: t). a :~: y -> Type + type WhySym (e :: a :~: y) = y :~: a + + type WhyHSym :: forall j (a :: j) t (y :: t). a :~~: y -> Type + type WhyHSym (e :: a :~~: y) = y :~~: a + + type TransStep :: forall k (x :: k) (z :: k). x :~: z -> x :~: z + type TransStep e = e + + type HTransStep :: forall j (x :: j) k (z :: k). x :~~: z -> x :~~: z + type HTransStep e = e + |]) + +$(singletons [d| + -- These use eliminators, but th-desugar takes a while to expand them. + -- TODO RGS: Investigate why. + {- + type Trans :: a :~: b -> b :~: c -> a :~: c + type Trans x y = + UnwrapTrans ((~>:~:) PWrappedTransSym0 x (WrapTrans TransStepSym0)) @@ y + + type HTrans :: a :~~: b -> b :~~: c -> a :~~: c + type HTrans x y = + UnwrapHTrans ((~>:~~:) PWrappedHTransSym0 x (WrapHTrans HTransStepSym0)) @@ y + -} + + type Trans :: a :~: b -> b :~: c -> a :~: c + type family Trans x y where Trans Refl Refl = Refl - type family HTrans (x :: a :~~: b) (y :: b :~~: c) :: a :~~: c where + type HTrans :: a :~~: b -> b :~~: c -> a :~~: c + type family HTrans x y where HTrans HRefl HRefl = HRefl + |]) - type WhyReplace (from :: t) (p :: t ~> Type) (e :: from :~: (y :: t)) = - p @@ y :: Type +type WhyReplace :: forall t. forall (from :: t) + -> (t ~> Type) + -> forall (y :: t). from :~: y + -> Type +type WhyReplace from p (e :: from :~: y) = p @@ y +data WhyReplaceSym2 :: forall t. forall (from :: t) + -> (t ~> Type) + -> forall (y :: t). from :~: y + ~> Type +type instance Apply (WhyReplaceSym2 x y) z = WhyReplace x y z - type WhyHReplace (from :: j) (p :: WrappedPred) (e :: from :~~: (y :: k)) = - UnwrapPred p @@ y :: Type +type WhyHReplace :: forall j. forall (from :: j) + -> WrappedPred + -> forall k (y :: k). from :~~: y + -> Type +type WhyHReplace from p (e :: from :~~: y) = UnwrapPred p @@ y +data WhyHReplaceSym2 :: forall j. forall (from :: j) + -> WrappedPred + -> forall k (y :: k). from :~~: y ~> Type +type instance Apply (WhyHReplaceSym2 x y) z = WhyHReplace x y z +$(singletons [d| type WhyLeibniz (f :: t ~> Type) (a :: t) (z :: t) = f @@ a -> f @@ z :: Type - - type WhyHLeibniz (f :: WrappedPred) (a :: j) (b :: k) = - UnwrapPred f @@ a -> UnwrapPred f @@ b :: Type - - type WhyCong (f :: x ~> y) (a :: x) (e :: a :~: (z :: x)) = - f @@ a :~: f @@ z :: Type + |]) - type WhyEqIsRefl (a :: k) (e :: a :~: (z :: k)) = - e :~~: (Refl :: a :~: a) :: Type +type WhyHLeibniz :: WrappedPred + -> forall j. j + -> forall k. k + -> Type +type WhyHLeibniz f a b = UnwrapPred f @@ a -> UnwrapPred f @@ b +data WhyHLeibnizSym2 :: WrappedPred + -> forall j. j + -> forall k. k + ~> Type +type instance Apply (WhyHLeibnizSym2 x y) z = WhyHLeibniz x y z - type WhyHEqIsHRefl (a :: j) (e :: a :~~: (z :: k)) = - e :~~: (HRefl :: a :~~: a) :: Type +type WhyCong :: (x ~> y) -> forall (a :: x) (z :: x). a :~: z -> Type +type WhyCong f (e :: a :~: z) = f @@ a :~: f @@ z +data WhyCongSym1 :: (x ~> y) -> forall (a :: x) (z :: x). a :~: z ~> Type +type instance Apply (WhyCongSym1 x) y = WhyCong x y - type WhyTransLeft (a :: k) (e :: a :~: (z :: k)) = - Trans e Refl :~: e :: Type +$(singletons [d| + type WhyEqIsRefl :: forall k (a :: k) (z :: k). a :~: z -> Type + type WhyEqIsRefl (e :: a :~: z) = e :~~: (Refl :: a :~: a) - type WhyTransLeftHelper (b :: k) (e :: b :~: (z :: k)) = - Trans (Symmetry e) Refl :~: Symmetry e :: Type + type WhyHEqIsHRefl :: forall j (a :: j) k (z :: k). a :~~: z -> Type + type WhyHEqIsHRefl (e :: a :~~: z) = e :~~: (HRefl :: a :~~: a) - type WhyHTransLeft (a :: j) (e :: a :~~: (z :: k)) = - HTrans e HRefl :~: e :: Type + type WhyTransLeft :: forall k (a :: k) (z :: k). a :~: z -> Type + type WhyTransLeft e = Trans e Refl :~: e - type WhyHTransLeftHelper (b :: k) (e :: b :~~: (z :: j)) = - HTrans (HSymmetry e) HRefl :~: HSymmetry e :: Type + type WhyHTransLeft :: forall j (a :: j) k (z :: k). a :~~: z -> Type + type WhyHTransLeft e = HTrans e HRefl :~: e - type WhyTransRight (a :: k) (e :: a :~: (z :: k)) = - Trans Refl e :~: e :: Type + type WhyTransRight :: forall k (a :: k) (z :: k). a :~: z -> Type + type WhyTransRight e = Trans Refl e :~: e - type WhyHTransRight (a :: j) (e :: a :~~: (z :: k)) = - HTrans HRefl e :~: e :: Type + type WhyHTransRight :: forall j (a :: j) k (z :: k). a :~~: z -> Type + type WhyHTransRight e = HTrans HRefl e :~: e - type WhyRebalance (b :: x2 :~: x3) (c :: x3 :~: x4) (a :: x1 :~: x2) = - Trans a (Trans b c) :~: Trans (Trans a b) c :: Type + type WhyRebalance :: x2 :~: x3 -> x3 :~: x4 -> x1 :~: x2 -> Type + type WhyRebalance b c a = Trans a (Trans b c) :~: Trans (Trans a b) c - type WhyRebalanceHelper (b :: x2 :~: x3) (c :: x3 :~: x4) (a :: x2 :~: x1) = - Trans (Symmetry a) (Trans b c) :~: Trans (Trans (Symmetry a) b) c :: Type + type WhyHRebalance :: x2 :~~: x3 -> x3 :~~: x4 -> x1 :~~: x2 -> Type + type WhyHRebalance b c a = HTrans a (HTrans b c) :~: HTrans (HTrans a b) c + |]) - type WhyHRebalance (b :: x2 :~~: x3) (c :: x3 :~~: x4) (a :: x1 :~~: x2) = - HTrans a (HTrans b c) :~: HTrans (HTrans a b) c :: Type +type Symmetry :: a :~: b -> b :~: a +type Symmetry (r :: a :~: b) = (~>:~:) WhySymSym0 r Refl - type WhyHRebalanceHelper (b :: x2 :~~: x3) (c :: x3 :~~: x4) (a :: x2 :~~: (x1 :: k1)) = - HTrans (HSymmetry a) (HTrans b c) :~: HTrans (HTrans (HSymmetry a) b) c :: Type - |]) +type HSymmetry :: a :~~: b -> b :~~: a +type HSymmetry (r :: a :~~: b) = (~>:~~:) WhyHSymSym0 r HRefl -- These newtype wrappers are needed to work around -- https://gitlab.haskell.org/ghc/ghc/issues/9269 -newtype WrappedSTrans (x :: k) (e1 :: x :~: y) = +type WrappedSTrans :: forall k (x :: k) (y :: k). x :~: y -> Type +newtype WrappedSTrans (e1 :: (x :: k) :~: y) = WrapSTrans { unwrapSTrans :: forall (z :: k) (e2 :: y :~: z). Sing e2 -> Sing (Trans e1 e2) } -newtype WrappedSHTrans (x :: j) (e1 :: x :~~: (y :: k)) = + +type WrappedSHTrans :: forall j (x :: j) k (y :: k). x :~~: y -> Type +newtype WrappedSHTrans (e1 :: x :~~: y) = WrapSHTrans { unwrapSHTrans :: forall l (z :: l) (e2 :: y :~~: z). Sing e2 -> Sing (HTrans e1 e2) } $(singletons [d| - type WhySTrans (x :: k) (e :: x :~: (y :: k)) = - WrappedSTrans x e :: Type + type WhySSym :: forall t (a :: t) (y :: t). a :~: y -> Type + type WhySSym e = Sing (Symmetry e) - type WhySHTrans (x :: j) (e :: x :~~: (y :: k)) = - WrappedSHTrans x e :: Type + type WhySymIdempotent :: forall t (a :: t) (z :: t). a :~: z -> Type + type WhySymIdempotent r = Symmetry (Symmetry r) :~: r + + type WhySHSym :: forall j (a :: j) z (y :: z). a :~~: y -> Type + type WhySHSym e = Sing (HSymmetry e) + + type WhyHSymIdempotent :: forall j (a :: j) z (y :: z). a :~~: y -> Type + type WhyHSymIdempotent r = HSymmetry (HSymmetry r) :~: r + + type WhyTransLeftHelper :: forall k (b :: k) (z :: k). b :~: z -> Type + type WhyTransLeftHelper e = Trans (Symmetry e) Refl :~: Symmetry e + + type WhyHTransLeftHelper :: forall k. forall (b :: k) j (z :: j). b :~~: z -> Type + type WhyHTransLeftHelper e = HTrans (HSymmetry e) HRefl :~: HSymmetry e + + type WhySTrans :: forall k (x :: k) (y :: k). x :~: y -> Type + type WhySTrans e = WrappedSTrans e + + type WhySHTrans :: forall j (x :: j) k (y :: k). x :~~: y -> Type + type WhySHTrans e = WrappedSHTrans e |]) + +type WhyRebalanceHelper :: x2 :~: x3 -> x3 :~: x4 -> forall x1. x2 :~: x1 -> Type +type WhyRebalanceHelper b c a = + Trans (Symmetry a) (Trans b c) :~: Trans (Trans (Symmetry a) b) c +data WhyRebalanceHelperSym2 :: x2 :~: x3 -> x3 :~: x4 -> forall x1. x2 :~: x1 ~> Type +type instance Apply (WhyRebalanceHelperSym2 x y) z = WhyRebalanceHelper x y z + +type WhyHRebalanceHelper :: x2 :~~: x3 -> x3 :~~: x4 -> forall k1 (x1 :: k1). x2 :~~: x1 -> Type +type WhyHRebalanceHelper b c a = + HTrans (HSymmetry a) (HTrans b c) :~: HTrans (HTrans (HSymmetry a) b) c +data WhyHRebalanceHelperSym2 :: x2 :~~: x3 -> x3 :~~: x4 -> forall k1 (x1 :: k1). x2 :~~: x1 ~> Type +type instance Apply (WhyHRebalanceHelperSym2 x y) z = WhyHRebalanceHelper x y z diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs --- a/tests/GADTSpec.hs +++ b/tests/GADTSpec.hs @@ -4,9 +4,11 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module GADTSpec where import Data.Kind @@ -24,10 +26,12 @@ ----- -data So :: Bool -> Type where +type So :: Bool -> Type +data So b where Oh :: So True -data SSo :: forall (what :: Bool). So what -> Type where +type SSo :: So what -> Type +data SSo s where SOh :: SSo Oh type instance Sing = SSo @@ -38,17 +42,38 @@ -> p @@ s elimSo SOh pOh = pOh +type ElimSo :: forall (p :: forall (long_sucker :: Bool). So long_sucker ~> Type) + -> forall (what :: Bool). + forall (s :: So what) + -> p @@ Oh + -> p @@ s +type family ElimSo p s pOh where + forall (p :: forall (long_sucker :: Bool). So long_sucker ~> Type) + (pOh :: p @@ Oh). + ElimSo p Oh pOh = pOh + elimPropSo :: forall (p :: Bool ~> Prop) (what :: Bool). So what -> p @@ True -> p @@ what elimPropSo Oh pOh = pOh -data Flarble :: Type -> Type -> Type where +type ElimPropSo :: forall (p :: Bool ~> Prop) + -> forall (what :: Bool). + So what + -> p @@ True + -> p @@ what +type family ElimPropSo p s pOh where + forall (p :: Bool ~> Prop) (pOh :: p @@ True). + ElimPropSo p Oh pOh = pOh + +type Flarble :: Type -> Type -> Type +data Flarble a b where MkFlarble1 :: a -> Flarble a b MkFlarble2 :: a ~ Bool => Flarble a (Maybe b) -data SFlarble :: forall a b. Flarble a b -> Type where +type SFlarble :: Flarble a b -> Type +data SFlarble f where SMkFlarble1 :: Sing x -> SFlarble (MkFlarble1 x) SMkFlarble2 :: SFlarble MkFlarble2 type instance Sing = SFlarble @@ -66,9 +91,28 @@ case s of (_ :: Sing (MkFlarble2 :: Flarble Bool (Maybe b'))) -> pMkFlarble2 @b' +type ElimFlarble :: + forall (p :: forall x y. Flarble x y ~> Type) + -> forall a b. + forall (f :: Flarble a b) + -> (forall a' b'. forall (x :: a') -> p @@ (MkFlarble1 x :: Flarble a' b')) + -> (forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b'))) + -> p @@ f +type family ElimFlarble p f pMkFlarble1 pMkFlarble2 where + forall (p :: forall x y. Flarble x y ~> Type) a b + (pMkFlarble1 :: forall a' b'. forall (x :: a') -> p @@ (MkFlarble1 x :: Flarble a' b')) + (pMkFlarble2 :: forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b'))) x. + ElimFlarble p (MkFlarble1 x :: Flarble a b) pMkFlarble1 pMkFlarble2 = + pMkFlarble1 @a @b x + forall (p :: forall x y. Flarble x y ~> Type) + (pMkFlarble1 :: forall a' b'. forall (x :: a') -> p @@ (MkFlarble1 x :: Flarble a' b')) + (pMkFlarble2 :: forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b'))) b'. + ElimFlarble p (MkFlarble2 :: Flarble Bool (Maybe b')) pMkFlarble1 pMkFlarble2 = + pMkFlarble2 @b' + elimPropFlarble :: forall (p :: Type ~> Type ~> Prop) a b. Flarble a b - -> (forall a' b'. a -> p @@ a' @@ b') + -> (forall a' b'. a' -> p @@ a' @@ b') -> (forall b'. p @@ Bool @@ Maybe b') -> p @@ a @@ b elimPropFlarble f@(MkFlarble1 x) pMkFlarble1 _ = @@ -78,10 +122,31 @@ case f of (_ :: Flarble Bool (Maybe b')) -> pMkFlarble2 @b' -data Obj :: Type where +type ElimPropFlarble :: + forall (p :: Type ~> Type ~> Prop) + -> forall a b. + Flarble a b + -> (forall a' b'. a' ~> p @@ a' @@ b') + -> (forall b'. p @@ Bool @@ Maybe b') + -> p @@ a @@ b +type family ElimPropFlarble p f pMkFlarble1 pMkFlarble2 where + forall (p :: Type ~> Type ~> Prop) a b + (pMkFlarble1 :: forall a' b'. a' ~> p @@ a' @@ b') + (pMkFlarble2 :: forall b'. p @@ Bool @@ Maybe b') x. + ElimPropFlarble p (MkFlarble1 x :: Flarble a b) pMkFlarble1 pMkFlarble2 = + pMkFlarble1 @a @b @@ x + forall (p :: Type ~> Type ~> Prop) + (pMkFlarble1 :: forall a' b'. a' ~> p @@ a' @@ b') + (pMkFlarble2 :: forall b'. p @@ Bool @@ Maybe b') b'. + ElimPropFlarble p (MkFlarble2 :: Flarble Bool (Maybe b')) pMkFlarble1 pMkFlarble2 = + pMkFlarble2 @b' + +type Obj :: Type +data Obj where MkObj :: o -> Obj -data SObj :: Obj -> Type where +type SObj :: Obj -> Type +data SObj o where SMkObj :: forall obiwan (obj :: obiwan). Sing obj -> SObj (MkObj obj) type instance Sing = SObj @@ -91,8 +156,23 @@ -> p @@ o elimObj (SMkObj (sx :: Sing (x :: obj))) pMkObj = pMkObj @obj @x sx +type ElimObj :: forall (p :: Obj ~> Type) + (o :: Obj) + -> (forall obj. forall (x :: obj) -> p @@ MkObj x) + -> p @@ o +type family ElimObj p o pMkObj where + forall (p :: Obj ~> Type) + (pMkObj :: forall obj. forall (x :: obj) -> p @@ MkObj x) + obj (x :: obj). + ElimObj p (MkObj (x :: obj)) pMkObj = pMkObj @obj x + elimPropObj :: forall (p :: Prop). Obj -> (forall obj. obj -> p) -> p elimPropObj (MkObj o) pMkObj = pMkObj o + +type ElimPropObj :: forall (p :: Prop) -> Obj -> (forall obj. obj ~> p) -> p +type family ElimPropObj p o pMkObj where + forall (p :: Prop) (pMkObj :: forall obj. obj ~> p) o. + ElimPropObj p (MkObj o) pMkObj = pMkObj @@ o diff --git a/tests/Internal.hs b/tests/Internal.hs --- a/tests/Internal.hs +++ b/tests/Internal.hs @@ -1,5 +1,7 @@ +{-# LANGUAGE StandaloneKindSignatures #-} module Internal where import Data.Kind +type Prop :: Type type Prop = Type diff --git a/tests/ListTypes.hs b/tests/ListTypes.hs --- a/tests/ListTypes.hs +++ b/tests/ListTypes.hs @@ -1,20 +1,22 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ListTypes where +import Data.Kind import Data.Singletons.Prelude import Data.Singletons.Prelude.List import Data.Singletons.TH $(singletons [d| - type WhyMapPreservesLength (f :: x ~> y) (l :: [x]) - = Length l :~: Length (Map f l) + type WhyMapPreservesLength :: (x ~> y) -> [x] -> Type + type WhyMapPreservesLength f l = Length l :~: Length (Map f l) - type WhyMapFusion (f :: y ~> z) (g :: x ~> y) (l :: [x]) - = Map f (Map g l) :~: Map (f .@#@$$$ g) l + type WhyMapFusion :: (y ~> z) -> (x ~> y) -> [x] -> Type + type WhyMapFusion f g l = Map f (Map g l) :~: Map (f .@#@$$$ g) l |]) diff --git a/tests/MatchabilizeSpec.hs b/tests/MatchabilizeSpec.hs new file mode 100644 --- /dev/null +++ b/tests/MatchabilizeSpec.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module MatchabilizeSpec where + +import Data.Eliminator +import Data.Singletons +import Data.Singletons.Prelude +import Data.Type.Equality + +import MatchabilizeTypes + +import Test.Hspec + +main :: IO () +main = hspec spec + +spec :: Spec +spec = pure () + +----- + +type ElimMaybeSimple :: b -> (a ~> b) -> Maybe a -> b +type ElimMaybeSimple (n :: b) j m = + UnMatchabilize (ElimMaybe (ConstSym1 b) m n (Matchabilize j)) + +test1 :: ElimMaybeSimple "a" IdSym0 Nothing :~: "a" +test1 = Refl + +test2 :: ElimMaybeSimple "a" IdSym0 (Just "b") :~: "b" +test2 = Refl diff --git a/tests/MatchabilizeTypes.hs b/tests/MatchabilizeTypes.hs new file mode 100644 --- /dev/null +++ b/tests/MatchabilizeTypes.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -Wno-unused-foralls #-} +module MatchabilizeTypes where + +import Data.Singletons + +type Matchabilize :: (a ~> b) -> forall (x :: a) -> b +data family Matchabilize + +type UnMatchabilize :: k -> k +type family UnMatchabilize a where + UnMatchabilize (Matchabilize f a) = f @@ a + UnMatchabilize x = x diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs --- a/tests/VecSpec.hs +++ b/tests/VecSpec.hs @@ -133,13 +133,13 @@ (SingKind e, SingI j, e ~ Demote e) => Vec (Vec e j) n -> Vec e (n * j) concatVec l = withSomeSing l $ \(singL :: Sing l) -> - elimVec @(Vec e j) @(WhyConcatVecSym2 e j) @n @l singL base step + elimVec @(Vec e j) @WhyConcatVecSym0 @n @l singL base step where - base :: WhyConcatVec e j VNil + base :: WhyConcatVec VNil base = VNil step :: forall (k :: Nat) (x :: Vec e j) (xs :: Vec (Vec e j) k). Sing x -> Sing xs - -> WhyConcatVec e j xs - -> WhyConcatVec e j (x :# xs) + -> WhyConcatVec xs + -> WhyConcatVec (x :# xs) step h _ vKJ = appendVec (fromSing h) vKJ diff --git a/tests/VecTypes.hs b/tests/VecTypes.hs --- a/tests/VecTypes.hs +++ b/tests/VecTypes.hs @@ -6,6 +6,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} @@ -19,6 +20,7 @@ import Data.Singletons.TH import Internal +type Vec :: Type -> Nat -> Type data Vec :: Type -> Nat -> Type where VNil :: Vec a Z (:#) :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n) @@ -27,7 +29,8 @@ deriving instance Ord a => Ord (Vec a n) deriving instance Show a => Show (Vec a n) -data SVec :: forall a (n :: Nat). Vec a n -> Type where +type SVec :: Vec a n -> Type +data SVec v where SVNil :: SVec VNil (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> SVec (x :# xs) type instance Sing = SVec @@ -60,6 +63,30 @@ elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons = pVCons sx sxs (elimVec @a @p @k @xs sxs pVNil pVCons) +type ElimVec :: forall a. + forall (p :: forall (k :: Nat). Vec a k ~> Type) + -> forall (n :: Nat). + forall (v :: Vec a n) + -> p @@ VNil + -> (forall (k :: Nat). + forall (x :: a) (xs :: Vec a k) -> + p @@ xs ~> p @@ (x :# xs)) + -> p @@ v +type family ElimVec p v pVNil pVCons where + forall a (p :: forall (k :: Nat). Vec a k ~> Type) + (pVNil :: p @@ VNil) + (pVCons :: forall (k :: Nat). + forall (x :: a) (xs :: Vec a k) -> + p @@ xs ~> p @@ (x :# xs)). + ElimVec p VNil pVNil pVCons = pVNil + forall a (p :: forall (k :: Nat). Vec a k ~> Type) + (pVNil :: p @@ VNil) + (pVCons :: forall (k :: Nat). + forall (x :: a) (xs :: Vec a k) -> + p @@ xs ~> p @@ (x :# xs)) k x xs. + ElimVec p (x :# (xs :: Vec a k)) pVNil pVCons = + pVCons x xs @@ ElimVec @a p @k xs pVNil pVCons + elimPropVec :: forall a (p :: Nat ~> Prop) (n :: Nat). Vec a n -> p @@ Z @@ -69,19 +96,37 @@ elimPropVec (x :# (xs :: Vec a k)) pZ pS = pS x xs (elimPropVec @a @p @k xs pZ pS) +type ElimPropVec :: forall a. + forall (p :: Nat ~> Prop) + -> forall (n :: Nat). + Vec a n + -> p @@ Z + -> (forall (k :: Nat). a ~> Vec a k ~> p @@ k ~> p @@ S k) + -> p @@ n +type family ElimPropVec p v pZ pS where + forall a (p :: Nat ~> Prop) + (pZ :: p @@ Z) + (pS :: forall (k :: Nat). a ~> Vec a k ~> p @@ k ~> p @@ S k). + ElimPropVec p VNil pZ pS = pZ + forall a (p :: Nat ~> Prop) + (pZ :: p @@ Z) + (pS :: forall (k :: Nat). a ~> Vec a k ~> p @@ k ~> p @@ S k) k x xs. + ElimPropVec p (x :# (xs :: Vec a k)) pZ pS = + pS @@ x @@ xs @@ ElimPropVec @a p @k xs pZ pS + $(singletons [d| - type WhyMapVec a b (n :: Nat) = - Vec a n -> Vec b n + type WhyMapVec :: Type -> Type -> Nat -> Type + type WhyMapVec a b n = Vec a n -> Vec b n - type WhyZipWithVec a b c (n :: Nat) = - Vec a n -> Vec b n -> Vec c n + type WhyZipWithVec :: Type -> Type -> Type -> Nat -> Type + type WhyZipWithVec a b c n = Vec a n -> Vec b n -> Vec c n - type WhyAppendVec e (m :: Nat) (n :: Nat) = - Vec e n -> Vec e m -> Vec e (n + m) + type WhyAppendVec :: Type -> Nat -> Nat -> Type + type WhyAppendVec e m n = Vec e n -> Vec e m -> Vec e (n + m) - type WhyTransposeVec e (m :: Nat) (n :: Nat) = - Vec (Vec e m) n -> Vec (Vec e n) m + type WhyTransposeVec :: Type -> Nat -> Nat -> Type + type WhyTransposeVec e m n = Vec (Vec e m) n -> Vec (Vec e n) m - type WhyConcatVec e (j :: Nat) (l :: Vec (Vec e j) n) = - Vec e (n * j) :: Type + type WhyConcatVec :: Vec (Vec e j) n -> Type + type WhyConcatVec (l :: Vec (Vec e j) n) = Vec e (n * j) |])