decidable 0.1.1.0 → 0.1.2.0

raw patch · 10 files changed

+583/−149 lines, 10 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +27/−0
• README.md +2/−1
• decidable.cabal +7/−3
• src/Data/Type/Predicate.hs +43/−24
• src/Data/Type/Predicate/Auto.hs +180/−9
• src/Data/Type/Predicate/Logic.hs +7/−15
• src/Data/Type/Predicate/Param.hs +40/−9
• src/Data/Type/Predicate/Quantification.hs +60/−16
• src/Data/Type/Universe.hs +210/−57
• src/Data/Type/Universe/Subset.hs +7/−15

@@ -1,6 +1,33 @@ Changelog ========= +Version 0.1.2.0+---------------++*October 14, 2018*++<https://github.com/mstksg/decidable/releases/tag/v0.1.2.0>++*   New `:.:` for universe composition, with `Elem` and `Universe` instances,+    and associated functions for working with them alongside `Any`, `All`.+*   Many of the `Elem` instances and indices in *Data.Type.Universe* have had+    their name changed to be more consistent with their role as indices.+    `IsJust` is now `IJust`, `IsRight` is `IRight`, `Snd` is `ISnd`.+*   Convenience predicates for alternate universes, such as `IsJust`, `IsLeft`,+    `IsNothing`, etc.+*   `NotAll` quantifier added alongside `None`.+*   Many new implications added to *Data.Type.Predicate.Quantification*,+    converting not-any and all-not, etc.+*   `NotFound p` added as a convenience predicate synonym for `Not (Found p)`.+*   Some implications showing the equivalence between `Found (InP f)` and+    `NotNull f` added to *Data.Type.Predicate.Param*.+*   Many new deduction rules added to *Data.Type.Predicate.Auto*.  Please see+    module documentation for a detailed list of new rules and classes in this+    version.+*   Convenient combinators for dealing with `Refuted` and `Decision` added to+    *Data.Type.Predicate*: `elimDisproof` and `mapRefuted.++ Version 0.1.1.0 --------------- 

@@ -7,6 +7,7 @@ This library provides combinators and typeclasses for working and manipulating type-level predicates in Haskell, which are represented as matchable type-level functions `k ~> Type` from the *singletons* library.  See *Data.Type.Predicate*-for a good starting point.+for a good starting point, and the documentation for `Predicate` on how to+define predicates.  [decidable]: http://hackage.haskell.org/package/decidable

@@ -2,12 +2,16 @@ -- -- see: https://github.com/sol/hpack ----- hash: 24f4181ba9122110e3a7d932fd7820c169b392a5cdbc76825cd8f60f5410f0e3+-- hash: 81cda78c02736265f023817475cdcf593f3a1cd1d8601f09bf92e4719d064fc1  name:           decidable-version:        0.1.1.0+version:        0.1.2.0 synopsis:       Combinators for manipulating dependently-typed predicates.-description:    Please see the README on GitHub at <https://github.com/mstksg/decidable#readme>+description:    This library provides combinators and typeclasses for working and manipulating+                type-level predicates in Haskell, which are represented as matchable type-level+                functions @k ~> Type@ from the @singletons@ library.  See "Data.Type.Predicate"+                for a good starting point, and the documentation for 'Predicate' on how to+                define predicates. category:       Dependent Types homepage:       https://github.com/mstksg/decidable#readme bug-reports:    https://github.com/mstksg/decidable/issues

@@ -1,20 +1,15 @@-{-# LANGUAGE AllowAmbiguousTypes    #-}-{-# LANGUAGE ConstraintKinds        #-}-{-# LANGUAGE DefaultSignatures      #-}-{-# LANGUAGE EmptyCase              #-}-{-# LANGUAGE FlexibleContexts       #-}-{-# LANGUAGE FlexibleInstances      #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE GADTs                  #-}-{-# LANGUAGE LambdaCase             #-}-{-# LANGUAGE MultiParamTypeClasses  #-}-{-# LANGUAGE RankNTypes             #-}-{-# LANGUAGE ScopedTypeVariables    #-}-{-# LANGUAGE TemplateHaskell        #-}-{-# LANGUAGE TypeApplications       #-}-{-# LANGUAGE TypeFamilies           #-}-{-# LANGUAGE TypeInType             #-}-{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds     #-}+{-# LANGUAGE DefaultSignatures   #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE FlexibleInstances   #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE TypeInType          #-}+{-# LANGUAGE TypeOperators       #-}  -- | -- Module      : Data.Type.Predicate@@ -50,7 +45,9 @@   -- * Manipulate Decisions   , Decision(..)   , flipDecision, mapDecision+  , elimDisproof   , forgetDisproof, forgetProof, isProved, isDisproved+  , mapRefuted   ) where  import           Data.Kind@@ -320,11 +317,11 @@ instance Provable Evident where     prove = id -instance (Decidable f, SingI g) => Decidable (f .@#@$$$ g) where-    decide = decide @f . ((sing :: Sing g) @@)+instance (Decidable p, SingI f) => Decidable (PMap f p) where+    decide = decide @p . ((sing :: Sing f) @@) -instance (Provable f, SingI g) => Provable (f .@#@$$$ g) where-    prove = prove @f . ((sing :: Sing g) @@)+instance (Provable p, SingI f) => Provable (PMap f p) where+    prove = prove @p . ((sing :: Sing f) @@)  -- | Compose two implications. compImpl@@ -355,7 +352,7 @@ -- of not-@a@. -- -- Note that this is not reversible in general in Haskell.  See--- 'doubleNegation' for a situation where it is.+-- 'Data.Type.Predicate.Logic.doubleNegation' for a situation where it is. -- -- @since 0.1.1.0 flipDecision@@ -372,8 +369,8 @@     -> Decision a     -> Decision b mapDecision f g = \case-    Proved    p -> Proved $ f p-    Disproved v -> Disproved $ v . g+    Proved    p -> Proved    $ f p+    Disproved v -> Disproved $ mapRefuted g v  -- | Converts a 'Decision' to a 'Maybe'.  Drop the witness of disproof of -- @a@, returning 'Just' if 'Proved' (with the proof) and 'Nothing' if@@ -407,3 +404,25 @@ -- @since 0.1.1.0 isDisproved :: Decision a -> Bool isDisproved = isNothing . forgetDisproof++-- | Helper function for a common pattern of eliminating the disproved+-- branch of 'Decision' to certaintify the proof.+--+-- @since 0.1.2.0+elimDisproof+    :: Decision a+    -> Refuted (Refuted a)+    -> a+elimDisproof = \case+    Proved    p -> const p+    Disproved v -> absurd . ($ v)++-- | Change the target of a 'Refuted' with a contravariant mapping+-- function.+--+-- @since 0.1.2.0+mapRefuted+    :: (a -> b)+    -> Refuted b+    -> Refuted a+mapRefuted = flip (.)

@@ -1,17 +1,17 @@ {-# LANGUAGE AllowAmbiguousTypes   #-}-{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE EmptyCase             #-} {-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-} {-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE LambdaCase            #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds             #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE TypeApplications      #-} {-# LANGUAGE TypeFamilies          #-} {-# LANGUAGE TypeInType            #-} {-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE TypeSynonymInstances  #-}+{-# LANGUAGE UndecidableInstances  #-}  -- | -- Module      : Data.Type.Predicate.Auto@@ -27,16 +27,25 @@ -- -- @since 0.1.1.0 module Data.Type.Predicate.Auto (+  -- * Automatically generate witnesses at compile-time     Auto(..)-  , AutoElem(..)+  , AutoNot, autoNot   , AutoProvable+  -- ** Helper classes+  , AutoElem(..)+  , AutoAll(..)+  -- * Auto with help+  , autoAny, autoNotAll   ) where -import           Data.List.NonEmpty        (NonEmpty(..))+import           Data.List.NonEmpty                 (NonEmpty(..)) import           Data.Singletons+import           Data.Singletons.Sigma import           Data.Type.Equality import           Data.Type.Predicate import           Data.Type.Predicate.Logic+import           Data.Type.Predicate.Param+import           Data.Type.Predicate.Quantification import           Data.Type.Universe  -- | Automatically generate a witness for predicate @p@ applied to input@@ -48,6 +57,21 @@ -- -- Very close in nature to the @Known@ typeclass in the /type-combinators/ -- library.+--+-- Admittedly this interface is a bit clunky and ad-hoc; at this point you+-- can just try writing 'auto' in your code and praying that it works.  You+-- always have the option, of course, to just manually write proofs.  If+-- you have any inference rules to suggest, feel free to submit a PR!+--+-- An important limitation of 'Auto' is the Haskell type system prevents+-- "either-or" constraints; this could potentially be implemented using+-- compiler plugins.+--+-- One consequence of this is that it is impossible to automatically derive+-- @'Any' f p@ and @'Not' ('All' f p)@.+--+-- For these, the compiler needs help; you can use 'autoAny' and+-- 'autoNotAll' for these situations. class Auto (p :: Predicate k) (a :: k) where     -- | Have the compiler generate a witness for @p \@\@ a@.     --@@ -61,6 +85,10 @@ instance SingI a => Auto Evident a where     auto = sing +-- | @since 0.1.2.0+instance SingI a => Auto (Not Impossible) a where+    auto = ($ sing)+ instance Auto (EqualTo a) a where     auto = Refl @@ -91,7 +119,7 @@     auto = prove @p @a sing  -- | Typeclass representing 'Elem's pointing to an @a :: k@ that can be--- generated automatically from type-level collection @as :: f k@.  +-- generated automatically from type-level collection @as :: f k@. -- -- If GHC knows both the type-level collection and the element you want to -- find at compile-time, this instance should allow it to find it.@@ -123,10 +151,10 @@     autoElem = IS autoElem  instance AutoElem Maybe ('Just a) a where-    autoElem = IsJust+    autoElem = IJust  instance AutoElem (Either j) ('Right a) a where-    autoElem = IsRight+    autoElem = IRight  instance AutoElem NonEmpty (a ':| as) a where     autoElem = NEHead@@ -134,6 +162,149 @@ instance AutoElem [] as a => AutoElem NonEmpty (b ':| as) a where     autoElem = NETail autoElem +-- | @since 0.1.2.0+instance AutoElem ((,) j) '(w, a) a where+    autoElem = ISnd++-- TODO: ???+-- instance AutoElem (f :.: g) p ('Comp ass) where+ instance AutoElem f as a => Auto (In f as) a where     auto = autoElem @f @as @a +-- | Helper class for deriving 'Auto' instances for 'All' predicates; each+-- 'Universe' instance is expected to implement these if possible, to get+-- free 'Auto' instaces for their 'All' predicates.+--+-- Also helps for 'Not' 'Any' predicates and 'Not' 'Found' 'AnyMatch'+-- predicates.+--+-- @since 0.1.2.0+class AutoAll f (p :: Predicate k) (as :: f k) where+    -- | Generate an 'All' for a given predicate over all items in @as@.+    autoAll :: All f p @@ as++instance AutoAll [] p '[] where+    autoAll = WitAll $ \case {}++instance (Auto p a, AutoAll [] p as) => AutoAll [] p (a ': as) where+    autoAll = WitAll $ \case+        IZ   -> auto @_ @p @a+        IS i -> runWitAll (autoAll @[] @p @as) i++instance AutoAll Maybe p 'Nothing where+    autoAll = WitAll $ \case {}++instance Auto p a => AutoAll Maybe p ('Just a) where+    autoAll = WitAll $ \case IJust -> auto @_ @p @a++instance AutoAll (Either j) p ('Left e) where+    autoAll = WitAll $ \case {}++instance Auto p a => AutoAll (Either j) p ('Right a) where+    autoAll = WitAll $ \case IRight -> auto @_ @p @a++instance (Auto p a, AutoAll [] p as) => AutoAll NonEmpty p (a ':| as) where+    autoAll = WitAll $ \case+        NEHead   -> auto @_ @p @a+        NETail i -> runWitAll (autoAll @[] @p @as) i++instance AutoAll f (All g p) ass => AutoAll (f :.: g) p ('Comp ass) where+    autoAll = WitAll $ \(i :? j) ->+      runWitAll (runWitAll (autoAll @f @(All g p) @ass) i) j++instance Auto p a => AutoAll ((,) j) p '(w, a) where+    autoAll = WitAll $ \case ISnd -> auto @_ @p @a++-- | @since 0.1.2.0+instance AutoAll f p as => Auto (All f p) as where+    auto = autoAll @f @p @as++-- | @since 0.1.2.0+instance SingI a => Auto (NotNull []) (a ': as) where+    auto = WitAny IZ sing++-- | @since 0.1.2.0+instance SingI a => Auto IsJust ('Just a) where+    auto = WitAny IJust sing++-- | @since 0.1.2.0+instance SingI a => Auto IsRight ('Right a) where+    auto = WitAny IRight sing++-- | @since 0.1.2.0+instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where+    auto = WitAny NEHead sing++-- | @since 0.1.2.0+instance SingI a => Auto (NotNull ((,) j)) '(w, a) where+    auto = WitAny ISnd sing++-- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to not be+-- true at compiletime.+--+-- @since 0.1.2.0+type AutoNot (p :: Predicate k) = Auto (Not p)++-- | Disprove @p \@\@ a@ at compiletime.+--+-- @+-- autoNot @_ @p @a :: Not p @@ a+-- @+--+-- @since 0.1.2.0+autoNot :: forall k (p :: Predicate k) (a :: k). AutoNot p a => Not p @@ a+autoNot = auto @k @(Not p) @a++-- | @since 0.1.2.0+instance Auto (Found p) (f @@ a) => Auto (Found (PPMap f p)) a where+    auto = case auto @_ @(Found p) @(f @@ a) of+        i :&: p -> i :&: p++-- | @since 0.1.2.0+instance Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p)) a where+    auto = mapRefuted (\(i :&: p) -> i :&: p)+         $ autoNot @_ @(Found p) @(f @@ a)++-- | @since 0.1.2.0+instance Auto p (f @@ a) => Auto (PMap f p) a where+    auto = auto @_ @p @(f @@ a)++-- | @since 0.1.2.0+instance AutoNot p (f @@ a) => Auto (Not (PMap f p)) a where+    auto = autoNot @_ @p @(f @@ a)++-- | Helper function to generate an @'Any' f p@ if you can pick out+-- a specific @a@ in @as@ where the predicate is provable at compile-time.+--+-- This is used to get around a fundamental limitation of 'Auto' as+-- a Haskell typeclass.+--+-- @since 0.1.2.0+autoAny+    :: forall f p as a. Auto p a+    => Elem f as a+    -> Any f p @@ as+autoAny i = WitAny i (auto @_ @p @a)++-- | @since 0.1.2.0+instance (SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p)) as where+    auto = allNotNone sing $ autoAll @f @(Not p) @as++-- | Helper function to generate a @'Not' ('All' f p)@ if you can pick out+-- a specific @a@ in @as@ where the predicate is disprovable at compile-time.+--+-- This is used to get around a fundamental limitation of 'Auto' as+-- a Haskell typeclass.+--+-- @since 0.1.2.0+autoNotAll+    :: forall p f as a. (AutoNot p a, SingI as)+    => Elem f as a+    -> Not (All f p) @@ as+autoNotAll = anyNotNotAll sing . autoAny++-- | @since 0.1.2.0+instance (SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p))) as where+    auto = mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p))+         $ auto @_ @(Not (Any f (Found p))) @as

@@ -1,11 +1,11 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds     #-}-{-# LANGUAGE EmptyCase           #-} {-# LANGUAGE FlexibleContexts    #-} {-# LANGUAGE FlexibleInstances   #-} {-# LANGUAGE LambdaCase          #-} {-# LANGUAGE RankNTypes          #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections       #-} {-# LANGUAGE TypeApplications    #-} {-# LANGUAGE TypeFamilies        #-} {-# LANGUAGE TypeInType          #-}@@ -63,9 +63,7 @@     -> Decision (q @@ a)     -> Decision ((p &&& q) @@ a) decideAnd = \case-    Proved p    -> \case-      Proved q    -> Proved (p, q)-      Disproved v -> Disproved $ \(_, q) -> v q+    Proved p    -> mapDecision (p,) snd     Disproved v -> \_ -> Disproved $ \(p, _) -> v p  -- | @p '|||' q@ is a predicate that either @p@ and @q@ are true.@@ -84,11 +82,7 @@     -> Decision ((p ||| q) @@ a) decideOr = \case     Proved p    -> \_ -> Proved $ Left p-    Disproved v -> \case-      Proved q    -> Proved $ Right q-      Disproved w -> Disproved $ \case-        Left p  -> v p-        Right q -> w q+    Disproved v -> mapDecision Right (either (absurd . v) id)  -- | Left-biased "or".  In proofs, prioritize a proof of the left side over -- a proof of the right side.@@ -227,15 +221,13 @@     :: forall p q. Decidable q     => (Not q --> Not p)     -> (p --> q)-contrapositive' f x p = case decide @q x of-    Proved     q -> q-    Disproved vq -> absurd $ f x vq p+contrapositive' f x p = elimDisproof (decide @q x) $ \vQ ->+    f x vQ p  -- | Logical double negation.  Only possible if @p@ is 'Decidable'. doubleNegation :: forall p. Decidable p => Not (Not p) --> p-doubleNegation x vvp = case decide @p x of-    Proved    p  -> p-    Disproved vp -> absurd $ vvp vp+doubleNegation x vvP = elimDisproof (decide @p x) $ \vP ->+    vvP vP  -- | If @p '&&&' q@ is true, then so is @p@. projAndFst :: (p &&& q) --> p

@@ -1,6 +1,4 @@ {-# LANGUAGE ConstraintKinds      #-}-{-# LANGUAGE DefaultSignatures    #-}-{-# LANGUAGE EmptyCase            #-} {-# LANGUAGE FlexibleContexts     #-} {-# LANGUAGE FlexibleInstances    #-} {-# LANGUAGE LambdaCase           #-}@@ -9,7 +7,6 @@ {-# LANGUAGE TypeFamilies         #-} {-# LANGUAGE TypeInType           #-} {-# LANGUAGE TypeOperators        #-}-{-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE UndecidableInstances #-}  -- |@@ -29,9 +26,10 @@     ParamPred   , FlipPP, ConstPP, PPMap, InP, AnyMatch   -- * Deciding and Proving-  , Found+  , Found, NotFound   , Selectable, select   , Searchable, search+  , inPNotNull, notNullInP   ) where  import           Data.Singletons@@ -54,17 +52,38 @@ -- -- For some context, an instance of @'Provable' ('Found' P)@, where @P :: -- 'ParamPred' k v@, means that for any input @x :: k@, we can always find--- a @y :: v@ such that we have @P x @@ y@.+-- a @y :: v@ such that we have @P x \@\@ y@. -- -- In the language of quantifiers, it means that forall @x :: k@, there--- exists a @y :: v@ such that @P x @@ y@.+-- exists a @y :: v@ such that @P x \@\@ y@. -- -- For an instance of @'Decidable' ('Found' P)@, it means that for all @x -- :: k@, we can prove or disprove the fact that there exists a @y :: v@--- such that @P x @@ y@.+-- such that @P x \@\@ y@. data Found :: ParamPred k v -> Predicate k type instance Apply (Found (p :: ParamPred k v)) a = Σ v (p a) +-- | Convert a parameterized predicate into a predicate on the parameter.+--+-- A @'Found' p@ is a predicate on @p :: 'ParamPred' k v@ that tests a @k@+-- for the fact that there /cannot exist/ a @v@ where @'ParamPred' k v@ is+-- satisfied.  That is, @'NotFound' P \@\@ x@ is satisfied if no @y :: v@+-- can exist where @P x \@\@ y@ is satisfied.+--+-- For some context, an instance of @'Provable' ('NotFound' P)@, where @P+-- :: 'ParamPred' k v@, means that for any input @x :: k@, we can always+-- reject any @y :: v@ that claims to satisfy @P x \@\@ y@.+--+-- In the language of quantifiers, it means that forall @x :: k@, there+-- does not exist a @y :: v@ such that @P x \@\@ y@.+--+-- For an instance of @'Decidable' ('Found' P)@, it means that for all @x+-- :: k@, we can prove or disprove the fact that there does not exist a @y+-- :: v@ such that @P x \@\@ y@.+--+-- @since 0.1.2.0+type NotFound (p :: ParamPred k v) = (Not (Found p) :: Predicate k)+ -- | Flip the arguments of a 'ParamPred'. data FlipPP :: ParamPred v k -> ParamPred k v type instance Apply (FlipPP p x) y = p y @@ x@@ -131,6 +150,18 @@ -- Essentially 'NotNull'. type InP f = (ElemSym1 f :: ParamPred (f k) k) +-- | @'NotNull' f@ is basically @'Found' ('InP' f)@.+--+-- @since 0.1.2.0+notNullInP :: NotNull f --> Found (InP f)+notNullInP _ (WitAny i s) = s :&: i++-- | @'NotNull' f@ is basically @'Found' ('InP' f)@.+--+-- @since 0.1.2.0+inPNotNull :: Found (InP f) --> NotNull f+inPNotNull _ (s :&: i) = WitAny i s+ instance Universe f => Decidable (Found (InP f)) where     decide = mapDecision (\case WitAny i s -> s :&: i    )                          (\case s :&: i     -> WitAny i s)@@ -138,11 +169,11 @@  instance Decidable (NotNull f ==> Found (InP f)) instance Provable (NotNull f ==> Found (InP f)) where-    prove _ (WitAny i s) = s :&: i+    prove = notNullInP  instance Decidable (Found (InP f) ==> NotNull f) instance Provable (Found (InP f) ==> NotNull f) where-    prove _ (s :&: i) = WitAny i s+    prove = inPNotNull  -- | @'AnyMatch' f@ takes a parmaeterized predicate on @k@ (testing for -- a @v@) and turns it into a parameterized predicate on @f k@ (testing for

@@ -1,18 +1,10 @@-{-# LANGUAGE AllowAmbiguousTypes   #-}-{-# LANGUAGE EmptyCase             #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE LambdaCase            #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RankNTypes            #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeApplications      #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeInType            #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE TypeSynonymInstances  #-}-{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE TypeInType          #-}+{-# LANGUAGE TypeOperators       #-}  -- | -- Module      : Data.Type.Predicate.Quantification@@ -28,18 +20,27 @@ -- module Data.Type.Predicate.Quantification (   -- * Any-    Any, WitAny(..), None+    Any, WitAny(..), anyImpossible   -- ** Decision   , decideAny, idecideAny, decideNone, idecideNone+  -- ** Negation+  , None, allNotNone, noneAllNot   -- ** Entailment   , entailAny, ientailAny, entailAnyF, ientailAnyF+  -- ** Composition+  , allComp, compAll   -- * All   , All, WitAll(..)   -- ** Decision   , decideAll, idecideAll+  -- ** Negation+  , NotAll+  , anyNotNotAll, notAllAnyNot   -- ** Entailment   , entailAll, ientailAll, entailAllF, ientailAllF   , decideEntailAll, idecideEntailAll+  -- ** Composition+  , anyComp, compAny   ) where  import           Data.Kind@@ -157,3 +158,46 @@     => p -?> q     -> All f p -?> All f q decideEntailAll = dmap @(All f)++-- | It is impossible for any value in a collection to be 'Impossible'.+--+-- @since 0.1.2.0+anyImpossible :: Universe f => Any f Impossible --> Impossible+anyImpossible _ (WitAny i p) = p . index i++-- | If any @a@ in @as@ does not satisfy @p@, then not all @a@ in @as@+-- satisfy @p@.+--+-- @since 0.1.2.0+anyNotNotAll :: Any f (Not p) --> NotAll f p+anyNotNotAll _ (WitAny i v) a = v $ runWitAll a i++-- | If not all @a@ in @as@ satisfy @p@, then there must be at least one+-- @a@ in @as@ that does not satisfy @p@.  Requires @'Decidable' p@ in+-- order to locate that specific @a@.+--+-- @since 0.1.2.0+notAllAnyNot+    :: forall f p. (Universe f, Decidable p)+    => NotAll f p --> Any f (Not p)+notAllAnyNot xs vAll = elimDisproof (decide @(Any f (Not p)) xs) $ \vAny ->+    vAll $ WitAll $ \i ->+      elimDisproof (decide @p (index i xs)) $ \vP ->+        vAny $ WitAny i vP++-- | If @p@ is false for all @a@ in @as@, then no @a@ in @as@ satisfies+-- @p@.+--+-- @since 0.1.2.0+allNotNone :: All f (Not p) --> None f p+allNotNone _ a (WitAny i v) = runWitAll a i v++-- | If no @a@ in @as@ satisfies @p@, then @p@ is false for all @a@ in+-- @as@.  Requires @'Decidable' p@ to interrogate the input disproof.+--+-- @since 0.1.2.0+noneAllNot+    :: forall f p. (Universe f, Decidable p)+    => 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

@@ -1,19 +1,20 @@-{-# LANGUAGE EmptyCase             #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE InstanceSigs          #-}-{-# LANGUAGE LambdaCase            #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RankNTypes            #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE StandaloneDeriving    #-}-{-# LANGUAGE TypeApplications      #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeInType            #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE TypeSynonymInstances  #-}-{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE DeriveDataTypeable   #-}+{-# LANGUAGE DeriveFunctor        #-}+{-# LANGUAGE DeriveGeneric        #-}+{-# LANGUAGE DeriveTraversable    #-}+{-# LANGUAGE EmptyCase            #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE InstanceSigs         #-}+{-# LANGUAGE LambdaCase           #-}+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE TemplateHaskell      #-}+{-# LANGUAGE TypeApplications     #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeInType           #-}+{-# LANGUAGE TypeOperators        #-}  -- | -- Module      : Data.Type.Universe@@ -31,27 +32,35 @@   -- * Universe     Elem, In, Universe(..)   -- ** Instances-  , Index(..), IsJust(..), IsRight(..), NEIndex(..), Snd(..)+  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..)+  , CompElem(..)   -- ** Predicates-  , All, WitAll(..)+  , All, WitAll(..), NotAll   , Any, WitAny(..), None   , Null, NotNull+  -- *** Specialized+  , IsJust, IsNothing, IsRight, IsLeft   -- * Decisions and manipulations   , decideAny, decideAll, genAllA, genAll, igenAll   , foldMapUni, ifoldMapUni, index, pickElem+  -- * Universe Composition+  , (:.:)(..), Sing(SComp), sGetComp, GetComp+  , allComp, compAll, anyComp, compAny   -- * Defunctionalization symbols-  , ElemSym0, ElemSym1, ElemSym2+  , ElemSym0, ElemSym1, ElemSym2, GetCompSym0, GetCompSym1   ) where -import           Data.Type.Predicate.Logic import           Control.Applicative import           Data.Functor.Identity import           Data.Kind import           Data.List.NonEmpty                    (NonEmpty(..)) import           Data.Singletons import           Data.Singletons.Decide-import           Data.Singletons.Prelude hiding        (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Snd, Null, Not)+import           Data.Singletons.Prelude hiding        (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Null, Not) import           Data.Type.Predicate+import           Data.Type.Predicate.Logic+import           Data.Typeable                         (Typeable)+import           GHC.Generics                          (Generic) import           Prelude hiding                        (any, all) import qualified Data.Singletons.Prelude.List.NonEmpty as NE @@ -152,6 +161,10 @@ -- satisfies predicate @p@. type None f p = (Not (Any f p) :: Predicate (f k)) +-- | A @'NotAll' f p@ is a predicate on a collection @as@ that at least one+-- @a@ in @as@ does not satisfy predicate @p@.+type NotAll f p = (Not (All f p) :: Predicate (f k))+ -- | Lifts a predicate @p@ on an individual @a@ into a predicate that on -- a collection @as@ that is true if and only if /any/ item in @as@ -- satisfies the original predicate.@@ -310,61 +323,81 @@  -- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is -- 'Just'.-data IsJust :: Maybe k -> k -> Type where-    IsJust :: IsJust ('Just a) a+data IJust :: Maybe k -> k -> Type where+    IJust :: IJust ('Just a) a -deriving instance Show (IsJust as a)-instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IsJust as)) where+deriving instance Show (IJust as a)+instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IJust as)) where     decide x = withSingI x $ pickElem -type instance Elem Maybe = IsJust+type instance Elem Maybe = IJust +-- | Test that a 'Maybe' is 'Just'.+--+-- @since 0.1.2.0+type IsJust    = (NotNull Maybe :: Predicate (Maybe k))++-- | Test that a 'Maybe' is 'Nothing'.+--+-- @since 0.1.2.0+type IsNothing = (Null    Maybe :: Predicate (Maybe k))+ instance Universe Maybe where     idecideAny f = \case       SNothing -> Disproved $ \case WitAny i _ -> case i of {}-      SJust x  -> case f IsJust x of-        Proved p    -> Proved $ WitAny IsJust p+      SJust x  -> case f IJust x of+        Proved p    -> Proved $ WitAny IJust p         Disproved v -> Disproved $ \case-          WitAny IsJust p -> v p+          WitAny IJust p -> v p      idecideAll f = \case       SNothing -> Proved $ WitAll $ \case {}-      SJust x  -> case f IsJust x of-        Proved p    -> Proved $ WitAll $ \case IsJust -> p-        Disproved v -> Disproved $ \a -> v $ runWitAll a IsJust+      SJust x  -> case f IJust x of+        Proved p    -> Proved $ WitAll $ \case IJust -> p+        Disproved v -> Disproved $ \a -> v $ runWitAll a IJust      igenAllA f = \case       SNothing -> pure $ WitAll $ \case {}-      SJust x  -> (\p -> WitAll $ \case IsJust -> p) <$> f IsJust x+      SJust x  -> (\p -> WitAll $ \case IJust -> p) <$> f IJust x  -- | Witness an item in a type-level @'Either' j@ by proving the 'Either' -- is 'Right'.-data IsRight :: Either j k -> k -> Type where-    IsRight :: IsRight ('Right a) a+data IRight :: Either j k -> k -> Type where+    IRight :: IRight ('Right a) a -deriving instance Show (IsRight as a)-instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IsRight as)) where+deriving instance Show (IRight as a)+instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IRight as)) where     decide x = withSingI x $ pickElem -type instance Elem (Either j) = IsRight+type instance Elem (Either j) = IRight +-- | Test that an 'Either' is 'Right'+--+-- @since 0.1.2.0+type IsRight = (NotNull (Either j) :: Predicate (Either j k))++-- | Test that an 'Either' is 'Left'+--+-- @since 0.1.2.0+type IsLeft  = (Null    (Either j) :: Predicate (Either j k))+ instance Universe (Either j) where     idecideAny f = \case       SLeft  _ -> Disproved $ \case WitAny i _ -> case i of {}-      SRight x -> case f IsRight x of-        Proved p    -> Proved $ WitAny IsRight p+      SRight x -> case f IRight x of+        Proved p    -> Proved $ WitAny IRight p         Disproved v -> Disproved $ \case-          WitAny IsRight p -> v p+          WitAny IRight p -> v p      idecideAll f = \case       SLeft  _ -> Proved $ WitAll $ \case {}-      SRight x -> case f IsRight x of-        Proved p    -> Proved $ WitAll $ \case IsRight -> p-        Disproved v -> Disproved $ \a -> v $ runWitAll a IsRight+      SRight x -> case f IRight x of+        Proved p    -> Proved $ WitAll $ \case IRight -> p+        Disproved v -> Disproved $ \a -> v $ runWitAll a IRight      igenAllA f = \case       SLeft  _ -> pure $ WitAll $ \case {}-      SRight x -> (\p -> WitAll $ \case IsRight -> p) <$> f IsRight x+      SRight x -> (\p -> WitAll $ \case IRight -> p) <$> f IRight x  -- | Witness an item in a type-level 'NonEmpty' by either indicating that -- it is the "head", or by providing an index in the "tail".@@ -419,22 +452,142 @@           NETail i -> runWitAll ps i  -- | Trivially witness an item in the second field of a type-level tuple.-data Snd :: (j, k) -> k -> Type where-    Snd :: Snd '(a, b) b+data ISnd :: (j, k) -> k -> Type where+    ISnd :: ISnd '(a, b) b -deriving instance Show (Snd as a)-instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (Snd as)) where+deriving instance Show (ISnd as a)+-- TODO: does this interfere with NonNull stuff?+instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (ISnd as)) where     decide x = withSingI x $ pickElem -type instance Elem ((,) j) = Snd+type instance Elem ((,) j) = ISnd  instance Universe ((,) j) where-    idecideAny f (STuple2 _ x) = case f Snd x of-      Proved p    -> Proved $ WitAny Snd p-      Disproved v -> Disproved $ \case WitAny Snd p -> v p+    idecideAny f (STuple2 _ x) = case f ISnd x of+      Proved p    -> Proved $ WitAny ISnd p+      Disproved v -> Disproved $ \case WitAny ISnd p -> v p -    idecideAll f (STuple2 _ x) = case f Snd x of-      Proved p    -> Proved $ WitAll $ \case Snd -> p-      Disproved v -> Disproved $ \a -> v $ runWitAll a Snd+    idecideAll f (STuple2 _ x) = case f ISnd x of+      Proved p    -> Proved $ WitAll $ \case ISnd -> p+      Disproved v -> Disproved $ \a -> v $ runWitAll a ISnd -    igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case Snd -> p) <$> f Snd x+    igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case ISnd -> p) <$> f ISnd x++-- | Compose two Functors.  Is the same as 'Data.Functor.Compose.Compose'+-- and 'GHC.Generics.:.:', except with a singleton and meant to be used at+-- the type level.  Will be redundant if either of the above gets brought+-- into the singletons library.+--+-- Note that because this is a higher-kinded data constructor, there is no+-- 'SingKind'  instance; if you need 'fromSing' and 'toSing', try going+-- through 'Comp' and 'getComp' and 'SComp' and 'sGetComp'.+--+-- @since 0.1.2.0+data (f :.: g) a = Comp { getComp :: f (g a) }+    deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)+deriving instance (Traversable f, Traversable g) => Traversable (f :.: g)++data instance Sing (k :: (f :.: g) a) where+    SComp :: Sing x -> Sing ('Comp x)++-- | 'getComp' lifted to the type level+--+-- @since 0.1.2.0+type family GetComp c where+    GetComp ('Comp a) = a++-- | Singletonized witness for 'GetComp'+--+-- @since 0.1.2.0+sGetComp :: Sing a -> Sing (GetComp a)+sGetComp (SComp x) = x+ +instance SingI ass => SingI ('Comp ass) where+    sing = SComp sing++data GetCompSym0 :: (f :.: g) k ~> f (g k)+type instance Apply GetCompSym0 ('Comp ass) = ass+type GetCompSym1 a = GetComp a++-- instance forall f g a f' g' a'. (SingKind (f (g a)), Demote (f (g a)) ~ f' (g' a')) => SingKind ((f :.: g) a) where+--     type Demote ((f :.: g) a) = (:.:) f' g' a'++-- | A pair of indices allows you to index into a nested structure.+--+-- @since 0.1.2.0+data CompElem :: (f :.: g) k -> k -> Type where+    (:?) :: Elem f ass as+         -> Elem g as  a+         -> CompElem ('Comp ass) a++-- deriving instance ((forall as. Show (Elem f ass as)), (forall as. Show (Elem g as a)))+--     => Show (CompElem ('Comp ass :: (f :.: g) k) a)++type instance Elem (f :.: g) = CompElem++instance (Universe f, Universe g) => Universe (f :.: g) where+    idecideAny+        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()+        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))+        -> Sing ass+        -> Decision (Any (f :.: g) p @@ ass)+    idecideAny f (SComp xss)+        = mapDecision anyComp compAny+        . idecideAny @f @_ @(Any g p) go+        $ xss+      where+        go  :: Elem f (GetComp ass) as+            -> Sing as+            -> Decision (Any g p @@ as)+        go i = idecideAny $ \j -> f (i :? j)++    idecideAll+        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()+        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))+        -> Sing ass+        -> Decision (All (f :.: g) p @@ ass)+    idecideAll f (SComp xss)+        = mapDecision allComp compAll+        . idecideAll @f @_ @(All g p) go+        $ xss+      where+        go  :: Elem f (GetComp ass) as+            -> Sing as+            -> Decision (All g p @@ as)+        go i = idecideAll $ \j -> f (i :? j)++    igenAllA+        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k) h. Applicative h+        => (forall a. Elem (f :.: g) ass a -> Sing a -> h (p @@ a))+        -> Sing ass+        -> h (All (f :.: g) p @@ ass)+    igenAllA f (SComp ass) = allComp <$> igenAllA @f @_ @(All g p) go ass+      where+        go  :: Elem f (GetComp ass) (as :: g k)+            -> Sing as+            -> h (All g p @@ as)+        go i = igenAllA $ \j -> f (i :? j)++-- | Turn a composition of 'Any' into an 'Any' of a composition.+--+-- @since 0.1.2.0+anyComp :: Any f (Any g p) @@ as -> Any (f :.: g) p @@ 'Comp as+anyComp (WitAny i (WitAny j p)) = WitAny (i :? j) p++-- | Turn an 'Any' of a composition into a composition of 'Any'.+--+-- @since 0.1.2.0+compAny :: Any (f :.: g) p @@ 'Comp as -> Any f (Any g p) @@ as+compAny (WitAny (i :? j) p) = WitAny i (WitAny j p)++-- | Turn a composition of 'All' into an 'All' of a composition.+--+-- @since 0.1.2.0+allComp :: All f (All g p) @@ as -> All (f :.: g) p @@ 'Comp as+allComp a = WitAll $ \(i :? j) -> runWitAll (runWitAll a i) j++-- | Turn an 'All' of a composition into a composition of 'All'.+--+-- @since 0.1.2.0+compAll :: All (f :.: g) p @@ 'Comp as -> All f (All g p) @@ as+compAll a = WitAll $ \i -> WitAll $ \j -> runWitAll a (i :? j)

@@ -1,18 +1,10 @@-{-# LANGUAGE AllowAmbiguousTypes   #-}-{-# LANGUAGE EmptyCase             #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE LambdaCase            #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RankNTypes            #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeApplications      #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeInType            #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE TypeSynonymInstances  #-}-{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE TypeInType          #-}+{-# LANGUAGE TypeOperators       #-}  -- | -- Module      : Data.Type.Universe.Subset