diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,17 @@ Changelog ========= +Version 0.1.5.0 +--------------- + +*March 6, 2018* + + + +* Add `allToAny` to *Data.Type.Predicate.Quantification*. +* Add `PPMapV`, `EqBy`, and `IsTC` to *Data.Type.Predicate.Param*. +* Kind-indexed singletons for indices in *Data.Type.Universe*. + Version 0.1.4.0 --------------- @@ -8,7 +19,7 @@ -* Added `tripleNegative` and `negateTwice` to *Data.Type.Predicate.Logic*, +* Added `tripleNegation` and `negateTwice` to *Data.Type.Predicate.Logic*, for more constructivist principles. * Renamed `excludedMiddle` to `complementation`. * Add `TyPP`, `SearchableTC`, `searchTC`, `SelectableTC`, `selectTC` to diff --git a/decidable.cabal b/decidable.cabal --- a/decidable.cabal +++ b/decidable.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: 6e9513846ace27e5bfa2f348d6298c6ad1245b42db00135bb2aa42c5203f095e +-- hash: 39c525768bc5e732a9d0d8a6b1931c269a0e4339a68d83434f6b3a4cf3f80c9f name: decidable -version: 0.1.4.0 +version: 0.1.5.0 synopsis: Combinators for manipulating dependently-typed predicates. description: This library provides combinators and typeclasses for working and manipulating type-level predicates in Haskell, which are represented as matchable type-level diff --git a/src/Data/Type/Predicate.hs b/src/Data/Type/Predicate.hs --- a/src/Data/Type/Predicate.hs +++ b/src/Data/Type/Predicate.hs @@ -61,7 +61,8 @@ -- 'Predicate' k@ is true/satisfied by input @x :: k@ if there exists -- a value of type @P \@\@ x@, and that it false/disproved if such a value -- cannot exist. (Where '@@' is 'Apply', the singleton library's type-level --- function application for mathcable functions) +-- function application for mathcable functions). In some contexts, this +-- is also known as a dependently typed "view". -- -- See 'Provable' and 'Decidable' for more information on how to use, prove -- and decide these predicates. @@ -177,8 +178,8 @@ -- | Like '-?>', but only in a specific context @h@. type (p -?># q) h = forall a. Sing a -> p @@ a -> h (Decision (q @@ a)) --- | A proving function for predicate @p@. See 'Provable' for more --- information. +-- | A proving function for predicate @p@; in some contexts, also called +-- a "view function". See 'Provable' for more information. type Prove p = forall a. Sing a -> p @@ a -- | We say that @p@ implies @q@ (@p '-->' q@) if, given @p @@ a@, we can @@ -220,30 +221,38 @@ -- @ -- 'decide' \@MyPredicate -- @ + -- + -- See 'decideTC' and 'DecidableTC' for a version that isn't ambiguously + -- typed, but only works when @p@ is a type constructor. decide :: Decide p default decide :: Provable p => Decide p decide = Proved . prove @p --- | A typeclass for provable predicates (constructivist tautologies). +-- | A typeclass for provable predicates (constructivist tautologies). In +-- some context, these are also known as "views". -- -- A predicate is provable if, given any input @a@, you can generate -- a proof of @p \@\@ a@. Essentially, it means that a predicate is "always -- true". -- +-- We can call a type a view if, for any input @a@, there is /some/ +-- constructor of @p \@\@ a@ that can we can use to "categorize" @a@. +-- -- This typeclass associates a canonical proof function for every provable --- predicate. +-- predicate, or a canonical view function for any view. -- -- It confers two main advatnages: -- --- 1. The proof function for every predicate is available via the same --- name +-- 1. The proof function/view for every predicate/view is available via +-- the same name -- -- 2. We can write 'Provable' instances for polymorphic predicate -- transformers (predicates parameterized on other predicates) easily, -- by refering to 'Provable' instances of the transformed predicates. class Provable p where - -- | The canonical proving function for predicate @p@. + -- | The canonical proving function for predicate @p@ (or a canonical + -- view function for view @p@). -- -- Note that 'prove' is ambiguously typed, so you /always/ need to call -- by specifying the predicate you want to prove using TypeApplications @@ -252,6 +261,9 @@ -- @ -- 'prove' \@MyPredicate -- @ + -- + -- See 'proveTC' and 'ProvableTC' for a version that isn't ambiguously + -- typed, but only works when @p@ is a type constructor. prove :: Prove p -- | @'Disprovable' p@ is a constraint that @p@ can be disproven. diff --git a/src/Data/Type/Predicate/Param.hs b/src/Data/Type/Predicate/Param.hs --- a/src/Data/Type/Predicate/Param.hs +++ b/src/Data/Type/Predicate/Param.hs @@ -25,7 +25,8 @@ module Data.Type.Predicate.Param ( -- * Parameterized Predicates ParamPred - , FlipPP, ConstPP, PPMap, InP, AnyMatch, TyPP + , IsTC, EqBy + , FlipPP, ConstPP, PPMap, PPMapV, InP, AnyMatch, TyPP -- * Deciding and Proving , Found, NotFound , Selectable, select @@ -40,6 +41,7 @@ import Data.Kind import Data.Singletons +import Data.Singletons.Decide import Data.Singletons.Prelude.Tuple import Data.Singletons.Sigma import Data.Type.Predicate @@ -101,6 +103,51 @@ data ConstPP :: Predicate v -> ParamPred k v type instance Apply (ConstPP p k) v = p @@ v +-- | @Found ('EqBy' f) \@\@ x@ is true if there exists some value when, +-- with @f@ applied to it, is equal to @x@. +-- +-- See 'IsTC' for a useful specific application. +-- +-- @ +-- 'EqBy' :: (v ~> k) -> 'ParamPred' k v +-- 'Found' ('EqBy' f) :: 'Predicate' k +-- @ +-- +-- @since 0.1.5.0 +data EqBy :: (v ~> k) -> ParamPred k v +type instance Apply (EqBy f x) y = x :~: (f @@ y) + +-- | @Found ('IsTC' t) \@\@ x@ is true if @x@ was made using the unary type +-- constructor @t@. +-- +-- For example: +-- +-- @ +-- type IsJust = (Found (IsTC 'Just) :: Predicate (Maybe v)) +-- @ +-- +-- makes a predicate where @IsJust \@\@ x@ is true if @x@ is 'Just', and +-- false if @x@ is 'Nothing'. +-- +-- For a more general version, see 'EqBy' +-- +-- The kind of 'IsTC' is: +-- +-- @ +-- 'IsTC' :: (v -> k) -> 'ParamPred' k v +-- 'Found' ('IsTC' t) :: 'Predicate' k +-- @ +-- +-- Applied to specific things: +-- +-- @ +-- 'IsTC' ''Just' :: 'ParamPred' (Maybe v) v +-- 'Found' ('IsTC' ''Just'') :: 'Predicate' (Maybe v) +-- @ +-- +-- @since 0.1.5.0 +type IsTC t = EqBy (TyCon1 t) + -- | Convert a normal '->' type constructor taking two arguments into -- a 'ParamPred'. -- @@ -118,6 +165,12 @@ data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v type instance Apply (PPMap f p x) y = p (f @@ x) @@ y +-- | Pre-compose a function to a 'ParamPred', but on the "value" side. +-- +-- @since 0.1.5.0 +data PPMapV :: (u ~> v) -> ParamPred k u -> ParamPred k v +type instance Apply (PPMapV f p x) y = p x @@ (f @@ y) + instance (Decidable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Decidable (Found (PPMap f p)) where decide = mapDecision (\case i :&: p -> i :&: p) (\case i :&: p -> i :&: p) @@ -141,11 +194,15 @@ -- | The deciding/searching function for @'Searchable' p@. -- --- Must be called by applying the 'ParamPred': +-- Because this is ambiguously typed, it must be called by applying the +-- 'ParamPred': -- -- @ -- 'search' \@p -- @ +-- +-- See 'searchTC' and 'SearchableTC' for a version that isn't ambiguously +-- typed, but only works when @p@ is a type constructor. search :: forall p. Searchable p => Decide (Found p) @@ -153,11 +210,15 @@ -- | The proving/selecting function for @'Selectable' p@. -- --- Must be called by applying the 'ParamPred': +-- Because this is ambiguously typed, it must be called by applying the +-- 'ParamPred': -- -- @ -- 'select' \@p -- @ +-- +-- See 'selectTC' and 'SelectableTC' for a version that isn't ambiguously +-- typed, but only works when @p@ is a type constructor. select :: forall p. Selectable p => Prove (Found p) diff --git a/src/Data/Type/Predicate/Quantification.hs b/src/Data/Type/Predicate/Quantification.hs --- a/src/Data/Type/Predicate/Quantification.hs +++ b/src/Data/Type/Predicate/Quantification.hs @@ -20,33 +20,33 @@ -- module Data.Type.Predicate.Quantification ( -- * Any - Any, WitAny(..), anyImpossible + Any, WitAny(..), None, anyImpossible -- ** Decision , decideAny, idecideAny, decideNone, idecideNone - -- ** Negation - , None, allNotNone, noneAllNot -- ** Entailment , entailAny, ientailAny, entailAnyF, ientailAnyF -- ** Composition , allComp, compAll -- * All - , All, WitAll(..) + , All, WitAll(..), NotAll -- ** Decision , decideAll, idecideAll - -- ** Negation - , NotAll - , anyNotNotAll, notAllAnyNot -- ** Entailment , entailAll, ientailAll, entailAllF, ientailAllF , decideEntailAll, idecideEntailAll -- ** Composition , anyComp, compAny + -- * Logical interplay + , allToAny + , allNotNone, noneAllNot + , anyNotNotAll, notAllAnyNot ) where import Data.Kind import Data.Singletons import Data.Singletons.Decide import Data.Type.Predicate +import Data.Type.Predicate.Logic import Data.Type.Universe -- | 'decideNone', but providing an 'Elem'. @@ -201,3 +201,10 @@ => None f p --> All f (Not p) noneAllNot xs vAny = elimDisproof (decide @(All f (Not p)) xs) $ \vAll -> vAll $ WitAll $ \i p -> vAny $ WitAny i p + +-- | If something is true for all xs, then it must be true for at least one +-- x in xs, provided that xs is not empty. +-- +-- @since 0.1.5.0 +allToAny :: (All f p &&& NotNull f) --> Any f p +allToAny _ (a, WitAny i _) = WitAny i $ runWitAll a i diff --git a/src/Data/Type/Universe.hs b/src/Data/Type/Universe.hs --- a/src/Data/Type/Universe.hs +++ b/src/Data/Type/Universe.hs @@ -45,7 +45,6 @@ , decideAny, decideAll, genAllA, genAll, igenAll , foldMapUni, ifoldMapUni, index, pickElem -- * Universe Combination - , Sing (SComp, SInL, SInR) -- ** Universe Composition , (:.:)(..), sGetComp, GetComp , allComp, compAll, anyComp, compAny @@ -55,6 +54,9 @@ , allSumL, allSumR, sumLAll, sumRAll -- * Defunctionalization symbols , ElemSym0, ElemSym1, ElemSym2, GetCompSym0, GetCompSym1 + -- * Singletons + , SIndex(..), SIJust(..), SIRight(..), SNEIndex(..), SISnd(..), SIProxy, SIIdentity(..) + , Sing (SComp, SInL, SIndex', SIJust', SIRight', SNEIndex', SISnd', SIProxy', SIIdentity') ) where import Control.Applicative @@ -290,6 +292,57 @@ type instance Elem [] = Index +-- | Kind-indexed singleton for 'Index'. Provided as a separate data +-- declaration to allow you to use these at the type level. However, the +-- main interface is still provided through the newtype wrapper 'SIndex'', +-- which has an actual proper 'Sing' instance. +-- +-- @since 0.1.5.0 +data SIndex as a :: Index as a -> Type where + SIZ :: SIndex (a ': as) a 'IZ + SIS :: SIndex bs a i -> SIndex (b ': bs) a ('IS i) + +deriving instance Show (SIndex as a i) + +newtype instance Sing (i :: Index as a) where + SIndex' :: SIndex as a i -> Sing i + +instance SingI 'IZ where + sing = SIndex' SIZ + +instance SingI i => SingI ('IS i) where + sing = case sing of + SIndex' i -> SIndex' (SIS i) + +instance SingKind (Index as a) where + type Demote (Index as a) = Index as a + fromSing (SIndex' i) = go i + where + go :: SIndex bs b i -> Index bs b + go = \case + SIZ -> IZ + SIS j -> IS (go j) + toSing i = go i (SomeSing . SIndex') + where + go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r + go = \case + IZ -> ($ SIZ) + IS j -> \f -> go j (f . SIS) + +instance SDecide (Index as a) where + SIndex' i %~ SIndex' j = go i j + where + go :: SIndex bs b i -> SIndex bs b j -> Decision (i :~: j) + go = \case + SIZ -> \case + SIZ -> Proved Refl + SIS _ -> Disproved $ \case {} + SIS i' -> \case + SIZ -> Disproved $ \case {} + SIS j' -> case go i' j' of + Proved Refl -> Proved Refl + Disproved v -> Disproved $ \case Refl -> v Refl + instance Universe [] where idecideAny :: forall k (p :: k ~> Type) (as :: [k]). () @@ -345,6 +398,31 @@ instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IJust as)) where decide x = withSingI x $ pickElem +-- | Kind-indexed singleton for 'IJust'. Provided as a separate data +-- declaration to allow you to use these at the type level. However, the +-- main interface is still provided through the newtype wrapper 'SIJust'', +-- which has an actual proper 'Sing' instance. +-- +-- @since 0.1.5.0 +data SIJust as a :: IJust as a -> Type where + SIJust :: SIJust ('Just a) a 'IJust + +deriving instance Show (SIJust as a i) + +newtype instance Sing (i :: IJust as a) where + SIJust' :: SIJust as a i -> Sing i + +instance SingI 'IJust where + sing = SIJust' SIJust + +instance SingKind (IJust as a) where + type Demote (IJust as a) = IJust as a + fromSing (SIJust' SIJust) = IJust + toSing IJust = SomeSing (SIJust' SIJust) + +instance SDecide (IJust as a) where + SIJust' SIJust %~ SIJust' SIJust = Proved Refl + type instance Elem Maybe = IJust -- | Test that a 'Maybe' is 'Just'. @@ -384,6 +462,31 @@ instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IRight as)) where decide x = withSingI x $ pickElem +-- | Kind-indexed singleton for 'IRight'. Provided as a separate data +-- declaration to allow you to use these at the type level. However, the +-- main interface is still provided through the newtype wrapper 'SIRight'', +-- which has an actual proper 'Sing' instance. +-- +-- @since 0.1.5.0 +data SIRight as a :: IRight as a -> Type where + SIRight :: SIRight ('Right a) a 'IRight + +deriving instance Show (SIRight as a i) + +newtype instance Sing (i :: IRight as a) where + SIRight' :: SIRight as a i -> Sing i + +instance SingI 'IRight where + sing = SIRight' SIRight + +instance SingKind (IRight as a) where + type Demote (IRight as a) = IRight as a + fromSing (SIRight' SIRight) = IRight + toSing IRight = SomeSing (SIRight' SIRight) + +instance SDecide (IRight as a) where + SIRight' SIRight %~ SIRight' SIRight = Proved Refl + type instance Elem (Either j) = IRight -- | Test that an 'Either' is 'Right' @@ -424,6 +527,49 @@ instance (SingI (as :: NonEmpty k), SDecide k) => Decidable (TyPred (NEIndex as)) where decide x = withSingI x $ pickElem +-- | Kind-indexed singleton for 'NEIndex'. Provided as a separate data +-- declaration to allow you to use these at the type level. However, the +-- main interface is still provided through the newtype wrapper +-- 'SNEIndex'', which has an actual proper 'Sing' instance. +-- +-- @since 0.1.5.0 +data SNEIndex as a :: NEIndex as a -> Type where + SNEHead :: SNEIndex (a ':| as) a 'NEHead + SNETail :: SIndex as a i -> SNEIndex (b ':| as) a ('NETail i) + +deriving instance Show (SNEIndex as a i) + +newtype instance Sing (i :: NEIndex as a) where + SNEIndex' :: SNEIndex as a i -> Sing i + +instance SingI 'NEHead where + sing = SNEIndex' SNEHead + +instance SingI i => SingI ('NETail i) where + sing = case sing of + SIndex' i -> SNEIndex' (SNETail i) + +instance SingKind (NEIndex as a) where + type Demote (NEIndex as a) = NEIndex as a + fromSing = \case + SNEIndex' SNEHead -> NEHead + SNEIndex' (SNETail i) -> NETail $ fromSing (SIndex' i) + toSing = \case + NEHead -> SomeSing (SNEIndex' SNEHead) + NETail i -> withSomeSing i $ \case + SIndex' j -> SomeSing (SNEIndex' (SNETail j)) + +instance SDecide (NEIndex as a) where + (%~) = \case + SNEIndex' SNEHead -> \case + SNEIndex' SNEHead -> Proved Refl + SNEIndex' (SNETail _) -> Disproved $ \case {} + SNEIndex' (SNETail i) -> \case + SNEIndex' SNEHead -> Disproved $ \case {} + SNEIndex' (SNETail j) -> case SIndex' i %~ SIndex' j of + Proved Refl -> Proved Refl + Disproved v -> Disproved $ \case Refl -> v Refl + type instance Elem NonEmpty = NEIndex instance Universe NonEmpty where @@ -475,6 +621,31 @@ instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (ISnd as)) where decide x = withSingI x $ pickElem +-- | Kind-indexed singleton for 'ISnd'. Provided as a separate data +-- declaration to allow you to use these at the type level. However, the +-- main interface is still provided through the newtype wrapper 'SISnd'', +-- which has an actual proper 'Sing' instance. +-- +-- @since 0.1.5.0 +data SISnd as a :: ISnd as a -> Type where + SISnd :: SISnd '(a, b) b 'ISnd + +deriving instance Show (SISnd as a i) + +newtype instance Sing (i :: ISnd as a) where + SISnd' :: SISnd as a i -> Sing i + +instance SingI 'ISnd where + sing = SISnd' SISnd + +instance SingKind (ISnd as a) where + type Demote (ISnd as a) = ISnd as a + fromSing (SISnd' SISnd) = ISnd + toSing ISnd = SomeSing (SISnd' SISnd) + +instance SDecide (ISnd as a) where + SISnd' SISnd %~ SISnd' SISnd = Proved Refl + type instance Elem ((,) j) = ISnd instance Universe ((,) j) where @@ -498,6 +669,27 @@ instance Provable (Not (TyPred (IProxy 'Proxy))) where prove _ = \case {} +-- | Kind-indexed singleton for 'IProxy'. Provided as a separate data +-- declaration to allow you to use these at the type level. However, the +-- main interface is still provided through the newtype wrapper 'SIProxy'', +-- which has an actual proper 'Sing' instance. +-- +-- @since 0.1.5.0 +data SIProxy as a :: IProxy as a -> Type + +deriving instance Show (SIProxy as a i) + +newtype instance Sing (i :: IProxy as a) where + SIProxy' :: SIProxy as a i -> Sing i + +instance SingKind (IProxy as a) where + type Demote (IProxy as a) = IProxy as a + fromSing (SIProxy' i) = case i of {} + toSing = \case {} + +instance SDecide (IProxy as a) where + SIProxy' i %~ SIProxy' _ = Proved $ case i of {} + type instance Elem Proxy = IProxy -- | The null universe @@ -517,6 +709,31 @@ instance (SingI (as :: Identity k), SDecide k) => Decidable (TyPred (IIdentity as)) where decide x = withSingI x $ pickElem + +-- | Kind-indexed singleton for 'IIdentity'. Provided as a separate data +-- declaration to allow you to use these at the type level. However, the +-- main interface is still provided through the newtype wrapper 'SIIdentity'', +-- which has an actual proper 'Sing' instance. +-- +-- @since 0.1.5.0 +data SIIdentity as a :: IIdentity as a -> Type where + SIId :: SIIdentity ('Identity a) a 'IId + +deriving instance Show (SIIdentity as a i) + +newtype instance Sing (i :: IIdentity as a) where + SIIdentity' :: SIIdentity as a i -> Sing i + +instance SingI 'IId where + sing = SIIdentity' SIId + +instance SingKind (IIdentity as a) where + type Demote (IIdentity as a) = IIdentity as a + fromSing (SIIdentity' SIId) = IId + toSing IId = SomeSing (SIIdentity' SIId) + +instance SDecide (IIdentity as a) where + SIIdentity' SIId %~ SIIdentity' SIId = Proved Refl type instance Elem Identity = IIdentity