decidable 0.1.4.0 → 0.1.5.0

raw patch · 6 files changed

+330/−22 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +12/−1
• decidable.cabal +2/−2
• src/Data/Type/Predicate.hs +20/−8
• src/Data/Type/Predicate/Param.hs +64/−3
• src/Data/Type/Predicate/Quantification.hs +14/−7
• src/Data/Type/Universe.hs +218/−1

@@ -1,6 +1,17 @@ Changelog ========= +Version 0.1.5.0+---------------++*March 6, 2018*++<https://github.com/mstksg/decidable/releases/tag/v0.1.5.0>++*   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 @@  <https://github.com/mstksg/decidable/releases/tag/v0.1.4.0> -*   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

@@ -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

@@ -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.

@@ -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)

@@ -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

@@ -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