diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,20 @@ Changelog ========= +Version 0.1.4.0 +--------------- + +*October 29, 2018* + + + +* 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 --------------- 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: 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 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 @@ -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 diff --git a/src/Data/Type/Predicate/Logic.hs b/src/Data/Type/Predicate/Logic.hs --- a/src/Data/Type/Predicate/Logic.hs +++ b/src/Data/Type/Predicate/Logic.hs @@ -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 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,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@.