decidable 0.1.3.1 → 0.1.4.0

raw patch · 5 files changed

+127/−12 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +14/−0
• decidable.cabal +2/−2
• src/Data/Type/Predicate.hs +7/−4
• src/Data/Type/Predicate/Logic.hs +26/−5
• src/Data/Type/Predicate/Param.hs +78/−1

@@ -1,6 +1,20 @@ Changelog ========= +Version 0.1.4.0+---------------++*October 29, 2018*++<https://github.com/mstksg/decidable/releases/tag/v0.1.4.0>++*   Added `tripleNegative` and `negateTwice` to *Data.Type.Predicate.Logic*,+    for more constructivist principles.+*   Renamed `excludedMiddle` to `complementation`.+*   Add `TyPP`, `SearchableTC`, `searchTC`, `SelectableTC`, `selectTC` to+    *Data.Type.Predicate.Param*, to mirror `TyPred` and the+    `DecidableTC`/`ProvableTC` interface from *Data.Type.Predicate*+ Version 0.1.3.1 --------------- 

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 8f4356d2d59f7c72a3fb5358dda90a0b36b47bb7fd03398fb1ed2c4c631a5a77+-- hash: 6e9513846ace27e5bfa2f348d6298c6ad1245b42db00135bb2aa42c5203f095e  name:           decidable-version:        0.1.3.1+version:        0.1.4.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

@@ -277,9 +277,10 @@ -- -- Is essentially 'Decidable', except with /type constructors/ @k -> -- 'Type'@ instead of matchable type-level functions (that are @k ~>--- 'Type'@).+-- 'Type'@).  Useful because 'decideTC' doesn't require anything fancy like+-- TypeApplications to use. ----- Mostly is in this library for compatiblity with "traditional" predicates+-- Also is in this library for compatiblity with "traditional" predicates -- that are GADT type constructors. -- -- @since 0.1.1.0@@ -305,8 +306,10 @@ -- -- Is essentially 'Provable', except with /type constructors/ @k -> 'Type'@ -- instead of matchable type-level functions (that are @k ~> 'Type'@).+-- Useful because 'proveTC' doesn't require anything fancy like+-- TypeApplications to use. ----- Mostly is in this library for compatiblity with "traditional" predicates+-- Also is in this library for compatiblity with "traditional" predicates -- that are GADT type constructors. -- -- @since 0.1.1.0@@ -373,7 +376,7 @@ -- | Flip the contents of a decision.  Turn a proof of @a@ into a disproof -- of not-@a@. ----- Note that this is not reversible in general in Haskell.  See+-- Note that this is not reversible in general in constructivist logic  See -- 'Data.Type.Predicate.Logic.doubleNegation' for a situation where it is. -- -- @since 0.1.1.0

@@ -33,7 +33,8 @@   , type (==>), proveImplies, Implies   , type (<==>), Equiv   -- * Logical deductions-  , compImpl, explosion, atom, excludedMiddle, doubleNegation+  , compImpl, explosion, atom+  , complementation, doubleNegation, tripleNegation, negateTwice   , contrapositive, contrapositive'   -- ** Lattice   , projAndFst, projAndSnd, injOrLeft, injOrRight@@ -206,18 +207,22 @@ atom = const  -- | We cannot have both @p@ and @'Not' p@.-excludedMiddle :: (p &&& Not p) --> Impossible-excludedMiddle _ (p, notP) _ = notP p+--+-- (Renamed in v0.1.4.0; used to be 'excludedMiddle')+--+-- @since 0.1.4.0+complementation :: forall p. (p &&& Not p) --> Impossible+complementation _ (p, notP) _ = notP p  -- | @since 0.1.3.0 instance {-# OVERLAPPING #-} Provable (p &&& Not p ==> Impossible) where-    prove = excludedMiddle @p+    prove = complementation @p  -- | If p implies q, then not q implies not p. contrapositive     :: (p --> q)     -> (Not q --> Not p)-contrapositive f x v p = v (f x p)+contrapositive f x vQ p = vQ (f x p)  -- | Reverse direction of 'contrapositive'.  Only possible if @q@ is -- 'Decidable' on its own, without the help of @p@, which makes this much@@ -230,9 +235,25 @@     f x vQ p  -- | Logical double negation.  Only possible if @p@ is 'Decidable'.+--+-- This is because in constructivist logic, not (not p) does not imply p.+-- However, p implies not (not p) (see 'negateTwice'), and not (not (not+-- p)) implies not p (see 'tripleNegation') doubleNegation :: forall p. Decidable p => Not (Not p) --> p doubleNegation x vvP = elimDisproof (decide @p x) $ \vP ->     vvP vP++-- | In constructivist logic, not (not (not p)) implies not p.+--+-- @since 0.1.4.0+tripleNegation :: forall p. Not (Not (Not p)) --> Not p+tripleNegation _ vvvP p = vvvP $ \vP -> vP p++-- | In constructivist logic, p implies not (not p).+--+-- @since 0.1.4.0+negateTwice :: p --> Not (Not p)+negateTwice _ p vP = vP p  -- | If @p '&&&' q@ is true, then so is @p@. projAndFst :: (p &&& q) --> p

@@ -25,16 +25,20 @@ module Data.Type.Predicate.Param (   -- * Parameterized Predicates     ParamPred-  , FlipPP, ConstPP, PPMap, InP, AnyMatch+  , FlipPP, ConstPP, PPMap, InP, AnyMatch, TyPP   -- * Deciding and Proving   , Found, NotFound   , Selectable, select   , Searchable, search   , inPNotNull, notNullInP+  -- ** Type Constructors+  , SelectableTC, selectTC+  , SearchableTC, searchTC   -- * Combining   , OrP, AndP   ) where +import           Data.Kind import           Data.Singletons import           Data.Singletons.Prelude.Tuple import           Data.Singletons.Sigma@@ -97,6 +101,17 @@ data ConstPP :: Predicate v -> ParamPred k v type instance Apply (ConstPP p k) v = p @@ v +-- | Convert a normal '->' type constructor taking two arguments into+-- a 'ParamPred'.+--+-- @+-- 'TyPP' :: (k -> v -> 'Type') -> 'ParamPred' k v+-- @+--+-- @since 0.1.4.0+data TyPP :: (k -> v -> Type) -> ParamPred k v+type instance Apply (TyPP t k) v = t k v+ -- | Pre-compose a function to a 'ParamPred'.  Is essentially @'flip' -- ('.')@, but unfortunately defunctionalization doesn't work too well with -- that definition.@@ -147,6 +162,68 @@     :: forall p. Selectable p     => Prove (Found p) select = prove @(Found p)++-- | If @T :: k -> v -> 'Type'@ is a type constructor, then @'SearchableTC'+-- T@ is a constraint that @T@ is "searchable", in that you have+-- a canonical function:+--+-- @+-- 'searchTC' :: 'Sing' x -> 'Decision' (Σ v ('TyPP' T x))+-- @+--+-- That, given an @x :: k@, we can decide whether or not a @y :: v@ exists+-- that satisfies @T x y@.+--+-- Is essentially 'Searchable', except with /type constructors/ @k ->+-- 'Type'@ instead of matchable type-level functions (that are @k ~>+-- 'Type'@).  Useful because 'searchTC' doesn't require anything fancy like+-- TypeApplications to use.+--+-- @since 0.1.4.0+type SearchableTC t = Decidable (Found (TyPP t))++-- | If @T :: k -> v -> 'Type'@ is a type constructor, then @'Selectable'+-- T@ is a constraint that @T@ is "selectable", in that you have+-- a canonical function:+--+-- @+-- 'selectTC' :: 'Sing' a -> Σ v ('TyPP' T x)+-- @+--+-- That is, given an @x :: k@, we can /always/ find a @y :: k@ that+-- satisfies @T x y@.+--+-- Is essentially 'Selectable', except with /type constructors/ @k ->+-- 'Type'@ instead of matchable type-level functions (that are @k ~>+-- 'Type'@). Useful because 'selectTC' doesn't require anything fancy like+-- TypeApplications to use.+--+-- @since 0.1.4.0+type SelectableTC t = Provable  (Found (TyPP t))++-- | The canonical selecting function for @'Searchable' t@.+--+-- Note that because @t@ must be an injective type constructor, you can use+-- this without explicit type applications; the instance of 'SearchableTC'+-- can be inferred from the result type.+--+-- @since 0.1.4.0+searchTC+    :: forall t. SearchableTC t+    => Decide (Found (TyPP t))+searchTC = search @(TyPP t)++-- | The canonical selecting function for @'SelectableTC' t@.+--+-- Note that because @t@ must be an injective type constructor, you can use+-- this without explicit type applications; the instance of 'SelectableTC'+-- can be inferred from the result type.+--+-- @since 0.1.4.0+selectTC+    :: forall t. SelectableTC t+    => Prove (Found (TyPP t))+selectTC = select @(TyPP t)  -- | A @'ParamPred' (f k) k@.  Parameterized on an @as :: f k@, returns -- a predicate that is true if there exists any @a :: k@ in @as@.