decidable 0.3.1.0 → 0.3.1.1

raw patch · 9 files changed

+1197/−917 lines, 9 filesdep ~functor-productsdep ~microlensdep ~singletonsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: functor-products, microlens, singletons, singletons-base, vinyl

API changes (from Hackage documentation)

Files

• CHANGELOG.md +9/−0
• decidable.cabal +6/−6
• src/Data/Type/Predicate.hs +261/−218
• src/Data/Type/Predicate/Auto.hs +127/−110
• src/Data/Type/Predicate/Logic.hs +119/−81
• src/Data/Type/Predicate/Param.hs +113/−76
• src/Data/Type/Predicate/Quantification.hs +145/−93
• src/Data/Type/Universe.hs +313/−254
• src/Data/Type/Universe/Subset.hs +104/−79

@@ -1,6 +1,15 @@ Changelog ========= +Version 0.3.1.1+---------------++*February 27, 2024*++<https://github.com/mstksg/functor-products/releases/tag/v0.3.1.1>++*   Remove upper bounds and deprecated pragmas+ Version 0.3.1.0 --------------- 

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           decidable-version:        0.3.1.0+version:        0.3.1.1 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@@ -47,9 +47,9 @@   ghc-options: -Wall -Wredundant-constraints -Wcompat -Werror=incomplete-patterns   build-depends:       base >=4.16 && <5-    , functor-products >=0.1.2 && <0.2-    , microlens <0.5-    , singletons >=3.0 && <3.1-    , singletons-base <3.2-    , vinyl <0.15+    , functor-products >=0.1.2+    , microlens+    , singletons >=3.0+    , singletons-base+    , vinyl   default-language: Haskell2010

@@ -1,17 +1,18 @@ {-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ConstraintKinds     #-}-{-# LANGUAGE DefaultSignatures   #-}-{-# LANGUAGE EmptyCase           #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE FlexibleInstances   #-}-{-# LANGUAGE InstanceSigs        #-}-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE TypeFamilies        #-}-{-# LANGUAGE TypeInType          #-}-{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}  -- | -- Module      : Data.Type.Predicate@@ -24,49 +25,72 @@ -- -- Combinators for working with type-level predicates, along with -- typeclasses for canonical proofs and deciding functions.--- module Data.Type.Predicate (-    -- * Predicates-    Predicate, Wit(..)-    -- ** Construct Predicates-  , TyPred, Evident, EqualTo, BoolPred, Impossible, In-    -- ** Manipulate predicates-  , PMap, type Not, decideNot-    -- * Provable Predicates-  , Prove, type (-->), type (-->#)-  , Provable(..)-  , Disprovable, disprove-  , ProvableTC, proveTC-  , TFunctor(..)-  , compImpl-    -- * Decidable Predicates-  , Decide, type (-?>), type (-?>#)-  , Decidable(..)-  , DecidableTC, decideTC-  , DFunctor(..)+  -- * Predicates+  Predicate,+  Wit (..),++  -- ** Construct Predicates+  TyPred,+  Evident,+  EqualTo,+  BoolPred,+  Impossible,+  In,++  -- ** Manipulate predicates+  PMap,+  type Not,+  decideNot,++  -- * Provable Predicates+  Prove,+  type (-->),+  type (-->#),+  Provable (..),+  Disprovable,+  disprove,+  ProvableTC,+  proveTC,+  TFunctor (..),+  compImpl,++  -- * Decidable Predicates+  Decide,+  type (-?>),+  type (-?>#),+  Decidable (..),+  DecidableTC,+  decideTC,+  DFunctor (..),+   -- * Manipulate Decisions-  , Decision(..)-  , flipDecision, mapDecision-  , elimDisproof-  , forgetDisproof, forgetProof, isProved, isDisproved-  , mapRefuted-  ) where+  Decision (..),+  flipDecision,+  mapDecision,+  elimDisproof,+  forgetDisproof,+  forgetProof,+  isProved,+  isDisproved,+  mapRefuted,+) where -import           Data.Either.Singletons-import           Data.Function.Singletons-import           Data.Functor.Identity-import           Data.Functor.Identity.Singletons-import           Data.Kind-import           Data.List.NonEmpty               (NonEmpty(..))-import           Data.List.Singletons hiding      (ElemSym1)-import           Data.Maybe-import           Data.Maybe.Singletons-import           Data.Singletons-import           Data.Singletons.Decide-import           Data.Tuple.Singletons-import           Data.Type.Functor.Product-import           Data.Void-import qualified Data.List.NonEmpty.Singletons    as NE+import Data.Either.Singletons+import Data.Function.Singletons+import Data.Functor.Identity+import Data.Functor.Identity.Singletons+import Data.Kind+import Data.List.NonEmpty (NonEmpty (..))+import qualified Data.List.NonEmpty.Singletons as NE+import Data.List.Singletons hiding (ElemSym1)+import Data.Maybe+import Data.Maybe.Singletons+import Data.Singletons+import Data.Singletons.Decide+import Data.Tuple.Singletons+import Data.Type.Functor.Product+import Data.Void  -- | A type-level predicate in Haskell.  We say that the predicate @P :: -- 'Predicate' k@ is true/satisfied by input @x :: k@ if there exists@@ -139,6 +163,7 @@ -- 'Evident' :: 'Predicate' k -- @ data Evident :: Predicate k+ type instance Apply Evident a = Sing a  -- | The always-false predicate@@ -177,7 +202,7 @@ -- -- It essentially turns a @k ~> 'Type'@ ("matchable" @'Predicate' k@) /back -- into/ a @k -> 'Type'@ predicate.-newtype Wit p a = Wit { getWit :: p @@ a }+newtype Wit p a = Wit {getWit :: p @@ a}  -- | A decision function for predicate @p@.  See 'Decidable' for more -- information.@@ -224,22 +249,21 @@ --     transformers (predicates parameterized on other predicates) easily, --     by refering to 'Decidable' instances of the transformed predicates. class Decidable p where-    -- | The canonical decision function for predicate @p@.-    ---    -- Note that 'decide' is ambiguously typed, so you /always/ need to call by-    -- specifying the predicate you want to prove using TypeApplications-    -- syntax:-    ---    -- @-    -- '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+  -- | The canonical decision function for predicate @p@.+  --+  -- Note that 'decide' is ambiguously typed, so you /always/ need to call by+  -- specifying the predicate you want to prove using TypeApplications+  -- syntax:+  --+  -- @+  -- '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).  In -- some context, these are also known as "views".@@ -263,20 +287,20 @@ --     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@ (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-    -- syntax:-    ---    -- @-    -- '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+  -- | 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+  -- syntax:+  --+  -- @+  -- '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. type Disprovable p = Provable (Not p)@@ -337,7 +361,7 @@ -- that are GADT type constructors. -- -- @since 0.1.1.0-type ProvableTC  p = Provable  (TyPred p)+type ProvableTC p = Provable (TyPred p)  -- | The canonical proving function for @'DecidableTC' t@. --@@ -352,162 +376,181 @@ -- | Implicatons @p '-?>' q@ can be lifted "through" a 'DFunctor' into an -- @f p '-?>' f q@. class DFunctor f where-    dmap :: forall p q. (p -?> q) -> (f p -?> f q)+  dmap :: forall p q. (p -?> q) -> (f p -?> f q)  -- | Implicatons @p '-->' q@ can be lifted "through" a 'TFunctor' into an -- @f p '-->' f q@. class TFunctor f where-    tmap :: forall p q. (p --> q) -> (f p --> f q)+  tmap :: forall p q. (p --> q) -> (f p --> f q)  instance (SDecide k, SingI (a :: k)) => Decidable (EqualTo a) where-    decide = (sing %~)+  decide = (sing %~)  instance Decidable Evident instance Provable Evident where-    prove = id+  prove = id  -- | @since 3.0.0 instance Decidable (TyPred WrappedSing)+ -- | @since 3.0.0 instance Provable (TyPred WrappedSing) where-    prove = WrapSing-+  prove = WrapSing  -- | @since 3.0.0 instance Provable p => Provable (TyPred (Rec (Wit p))) where-    prove = mapProd (Wit . prove @p) . singProd+  prove = mapProd (Wit . prove @p) . singProd+ -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (Rec (Wit p))) where-    decide = \case-      SNil         -> Proved RNil-      x `SCons` xs -> case decide @p x of-        Proved p -> case decideTC xs of-          Proved ps -> Proved $ Wit p :& ps-          Disproved vs -> Disproved $ \case-            _ :& ps -> vs ps-        Disproved v -> Disproved $ \case-          Wit p :& _ -> v p+  decide = \case+    SNil -> Proved RNil+    x `SCons` xs -> case decide @p x of+      Proved p -> case decideTC xs of+        Proved ps -> Proved $ Wit p :& ps+        Disproved vs -> Disproved $ \case+          _ :& ps -> vs ps+      Disproved v -> Disproved $ \case+        Wit p :& _ -> v p  -- | @since 3.0.0 instance Provable (TyPred (Rec WrappedSing)) where-    prove = mapProd WrapSing . singProd+  prove = mapProd WrapSing . singProd+ -- | @since 3.0.0 instance Decidable (TyPred (Rec WrappedSing))  -- | @since 3.0.0 instance Provable p => Provable (TyPred (PMaybe (Wit p))) where-    prove = mapProd (Wit . prove @p) . singProd+  prove = mapProd (Wit . prove @p) . singProd+ -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (PMaybe (Wit p))) where-    decide = \case-      SNothing -> Proved PNothing-      SJust x  -> mapDecision (PJust . Wit) (\case PJust (Wit p) -> p)-                . decide @p-                $ x+  decide = \case+    SNothing -> Proved PNothing+    SJust x ->+      mapDecision (PJust . Wit) (\case PJust (Wit p) -> p)+        . decide @p+        $ x  -- | @since 3.0.0 instance Provable (TyPred (PMaybe WrappedSing)) where-    prove = mapProd WrapSing . singProd+  prove = mapProd WrapSing . singProd+ -- | @since 3.0.0 instance Decidable (TyPred (PMaybe WrappedSing))  -- | @since 3.0.0 instance Provable p => Provable (TyPred (NERec (Wit p))) where-    prove = mapProd (Wit . prove @p) . singProd+  prove = mapProd (Wit . prove @p) . singProd+ -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (NERec (Wit p))) where-    decide = \case-      x NE.:%| xs -> case decide @p x of-        Proved p -> case decideTC xs of-          Proved ps -> Proved $ Wit p :&| ps-          Disproved vs -> Disproved $ \case-            _ :&| ps -> vs ps-        Disproved v -> Disproved $ \case-          Wit p :&| _ -> v p+  decide = \case+    x NE.:%| xs -> case decide @p x of+      Proved p -> case decideTC xs of+        Proved ps -> Proved $ Wit p :&| ps+        Disproved vs -> Disproved $ \case+          _ :&| ps -> vs ps+      Disproved v -> Disproved $ \case+        Wit p :&| _ -> v p  -- | @since 3.0.0 instance Provable (TyPred (NERec WrappedSing)) where-    prove = mapProd WrapSing . singProd+  prove = mapProd WrapSing . singProd+ -- | @since 3.0.0 instance Decidable (TyPred (NERec WrappedSing))  -- | @since 3.0.0 instance Provable p => Provable (TyPred (PIdentity (Wit p))) where-    prove = mapProd (Wit . prove @p) . singProd+  prove = mapProd (Wit . prove @p) . singProd+ -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (PIdentity (Wit p))) where-    decide = \case-      SIdentity x -> mapDecision (PIdentity . Wit) (\case PIdentity (Wit p) -> p)-                   . decide @p-                   $ x+  decide = \case+    SIdentity x ->+      mapDecision (PIdentity . Wit) (\case PIdentity (Wit p) -> p)+        . decide @p+        $ x  -- | @since 3.0.0 instance Provable (TyPred (PIdentity WrappedSing)) where-    prove = mapProd WrapSing . singProd+  prove = mapProd WrapSing . singProd+ -- | @since 3.0.0 instance Decidable (TyPred (PIdentity WrappedSing))  -- | @since 3.0.0 instance Provable p => Provable (TyPred (PEither (Wit p))) where-    prove = mapProd (Wit . prove @p) . singProd+  prove = mapProd (Wit . prove @p) . singProd+ -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (PEither (Wit p))) where-    decide = \case-      SLeft  x -> Proved $ PLeft x-      SRight y -> mapDecision (PRight . Wit) (\case PRight (Wit p) -> p)-                . decide @p-                $ y+  decide = \case+    SLeft x -> Proved $ PLeft x+    SRight y ->+      mapDecision (PRight . Wit) (\case PRight (Wit p) -> p)+        . decide @p+        $ y  -- | @since 3.0.0 instance Provable (TyPred (PEither WrappedSing)) where-    prove = mapProd WrapSing . singProd+  prove = mapProd WrapSing . singProd+ -- | @since 3.0.0 instance Decidable (TyPred (PEither WrappedSing))  -- | @since 3.0.0 instance Provable p => Provable (TyPred (PTup (Wit p))) where-    prove = mapProd (Wit . prove @p) . singProd+  prove = mapProd (Wit . prove @p) . singProd+ -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (PTup (Wit p))) where-    decide (STuple2 x y) = mapDecision (PTup x . Wit) (\case PTup _ (Wit p) -> p)-                         . decide @p-                         $ y+  decide (STuple2 x y) =+    mapDecision (PTup x . Wit) (\case PTup _ (Wit p) -> p)+      . decide @p+      $ y  -- | @since 3.0.0 instance Provable (TyPred (PTup WrappedSing)) where-    prove = mapProd WrapSing . singProd+  prove = mapProd WrapSing . singProd+ -- | @since 3.0.0 instance Decidable (TyPred (PTup WrappedSing))  instance (Decidable p, SingI f) => Decidable (PMap f p) where-    decide = decide @p . applySing (sing :: Sing f)+  decide = decide @p . applySing (sing :: Sing f)  instance (Provable p, SingI f) => Provable (PMap f p) where-    prove = prove @p . applySing (sing :: Sing f)+  prove = prove @p . applySing (sing :: Sing f)  -- | Compose two implications.-compImpl-    :: forall p q r. ()-    => p --> q-    -> q --> r-    -> p --> r+compImpl ::+  forall p q r.+  () =>+  p --> q ->+  q --> r ->+  p --> r compImpl f g s = g s . f s  -- | @'Not' p@ is the predicate that @p@ is not true. data Not :: Predicate k -> Predicate k+ type instance Apply (Not p) a = Refuted (p @@ a)  instance Decidable p => Decidable (Not p) where-    decide (x :: Sing a) = decideNot @p @a (decide @p x)+  decide (x :: Sing a) = decideNot @p @a (decide @p x)  instance Provable (Not Impossible) where-    prove x v = absurd $ v x+  prove x v = absurd $ v x  -- | Decide @'Not' p@ based on decisions of @p@.-decideNot-    :: forall p a. ()-    => Decision (p @@ a)-    -> Decision (Not p @@ a)+decideNot ::+  forall p a.+  () =>+  Decision (p @@ a) ->+  Decision (Not p @@ a) decideNot = flipDecision  -- | Flip the contents of a decision.  Turn a proof of @a@ into a disproof@@ -517,42 +560,42 @@ -- 'Data.Type.Predicate.Logic.doubleNegation' for a situation where it is. -- -- @since 0.1.1.0-flipDecision-    :: Decision a-    -> Decision (Refuted a)+flipDecision ::+  Decision a ->+  Decision (Refuted a) flipDecision = \case-    Proved    p -> Disproved ($ p)-    Disproved v -> Proved v+  Proved p -> Disproved ($ p)+  Disproved v -> Proved v  -- | Map over the value inside a 'Decision'.-mapDecision-    :: (a -> b)-    -> (b -> a)-    -> Decision a-    -> Decision b+mapDecision ::+  (a -> b) ->+  (b -> a) ->+  Decision a ->+  Decision b mapDecision f g = \case-    Proved    p -> Proved    $ f p-    Disproved v -> Disproved $ mapRefuted g v+  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 -- 'Disproved'. -- -- @since 0.1.1.0-forgetDisproof-    :: Decision a-    -> Maybe a+forgetDisproof ::+  Decision a ->+  Maybe a forgetDisproof = \case-    Proved    p -> Just p-    Disproved _ -> Nothing+  Proved p -> Just p+  Disproved _ -> Nothing  -- | Drop the witness of proof of @a@, returning 'Nothing' if 'Proved' and -- 'Just' if 'Disproved' (with the disproof). -- -- @since 0.1.1.0-forgetProof-    :: Decision a-    -> Maybe (Refuted a)+forgetProof ::+  Decision a ->+  Maybe (Refuted a) forgetProof = forgetDisproof . flipDecision  -- | Boolean test if a 'Decision' is 'Proved'.@@ -571,22 +614,22 @@ -- branch of 'Decision' to certaintify the proof. -- -- @since 0.1.2.0-elimDisproof-    :: Decision a-    -> Refuted (Refuted a)-    -> a+elimDisproof ::+  Decision a ->+  Refuted (Refuted a) ->+  a elimDisproof = \case-    Proved    p -> const p-    Disproved v -> absurd . ($ v)+  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 ::+  (a -> b) ->+  Refuted b ->+  Refuted a mapRefuted = flip (.)  -- | @'In' f as@ is a predicate that a given input @a@ is a member of@@ -594,52 +637,52 @@ type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as  instance (SDecide k, SingI (as :: [k])) => Decidable (In [] as) where-    decide :: forall a. Sing a -> Decision (Index as a)-    decide x = go (sing @as)-      where-        go :: Sing bs -> Decision (Index bs a)-        go = \case-          SNil         -> Disproved $ \case {}-          y `SCons` ys -> case x %~ y of-            Proved Refl -> Proved IZ-            Disproved v -> case go ys of-              Proved i    -> Proved (IS i)-              Disproved u -> Disproved $ \case-                IZ   -> v Refl-                IS i -> u i+  decide :: forall a. Sing a -> Decision (Index as a)+  decide x = go (sing @as)+    where+      go :: Sing bs -> Decision (Index bs a)+      go = \case+        SNil -> Disproved $ \case {}+        y `SCons` ys -> case x %~ y of+          Proved Refl -> Proved IZ+          Disproved v -> case go ys of+            Proved i -> Proved (IS i)+            Disproved u -> Disproved $ \case+              IZ -> v Refl+              IS i -> u i  instance (SDecide k, SingI (as :: Maybe k)) => Decidable (In Maybe as) where-    decide x = case sing @as of-      SNothing -> Disproved $ \case {}-      SJust y  -> case x %~ y of-        Proved Refl -> Proved IJust-        Disproved v -> Disproved $ \case IJust -> v Refl+  decide x = case sing @as of+    SNothing -> Disproved $ \case {}+    SJust y -> case x %~ y of+      Proved Refl -> Proved IJust+      Disproved v -> Disproved $ \case IJust -> v Refl  instance (SDecide k, SingI (as :: Either j k)) => Decidable (In (Either j) as) where-    decide x = case sing @as of-      SLeft _  -> Disproved $ \case {}-      SRight y -> case x %~ y of-        Proved Refl -> Proved IRight-        Disproved v -> Disproved $ \case IRight -> v Refl+  decide x = case sing @as of+    SLeft _ -> Disproved $ \case {}+    SRight y -> case x %~ y of+      Proved Refl -> Proved IRight+      Disproved v -> Disproved $ \case IRight -> v Refl  instance (SDecide k, SingI (as :: NonEmpty k)) => Decidable (In NonEmpty as) where-    decide x = case sing @as of-      y NE.:%| (Sing :: Sing bs) -> case x %~ y of-        Proved Refl -> Proved NEHead-        Disproved v -> case decide @(In [] bs) x of-          Proved i    -> Proved $ NETail i-          Disproved u -> Disproved $ \case-            NEHead   -> v Refl-            NETail i -> u i+  decide x = case sing @as of+    y NE.:%| (Sing :: Sing bs) -> case x %~ y of+      Proved Refl -> Proved NEHead+      Disproved v -> case decide @(In [] bs) x of+        Proved i -> Proved $ NETail i+        Disproved u -> Disproved $ \case+          NEHead -> v Refl+          NETail i -> u i  instance (SDecide k, SingI (as :: (j, k))) => Decidable (In ((,) j) as) where-    decide x = case sing @as of-      STuple2 _ y -> case x %~ y of-        Proved Refl -> Proved ISnd-        Disproved v -> Disproved $ \case ISnd -> v Refl+  decide x = case sing @as of+    STuple2 _ y -> case x %~ y of+      Proved Refl -> Proved ISnd+      Disproved v -> Disproved $ \case ISnd -> v Refl  instance (SDecide k, SingI (as :: Identity k)) => Decidable (In Identity as) where-    decide x = case sing @as of-      SIdentity y -> case x %~ y of-        Proved Refl -> Proved IId-        Disproved v -> Disproved $ \case IId -> v Refl+  decide x = case sing @as of+    SIdentity y -> case x %~ y of+      Proved Refl -> Proved IId+      Disproved v -> Disproved $ \case IId -> v Refl

@@ -1,17 +1,17 @@-{-# LANGUAGE AllowAmbiguousTypes   #-}-{-# LANGUAGE ConstraintKinds       #-}-{-# LANGUAGE EmptyCase             #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE KindSignatures        #-}-{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeApplications      #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeInType            #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}  -- | -- Module      : Data.Type.Predicate.Auto@@ -28,28 +28,30 @@ -- @since 0.1.1.0 module Data.Type.Predicate.Auto (   -- * Automatically generate witnesses at compile-time-    Auto(..)-  , autoTC-  , AutoNot-  , autoNot-  , autoAny, autoNotAll-  , AutoProvable+  Auto (..),+  autoTC,+  AutoNot,+  autoNot,+  autoAny,+  autoNotAll,+  AutoProvable,+   -- ** Helper classes-  , AutoElem(..)-  , AutoAll(..)-  ) where+  AutoElem (..),+  AutoAll (..),+) where -import           Data.Functor.Identity-import           Data.List.NonEmpty                 (NonEmpty(..))-import           Data.Singletons-import           Data.Singletons.Sigma-import           Data.Type.Equality-import           Data.Type.Functor.Product-import           Data.Type.Predicate-import           Data.Type.Predicate.Logic-import           Data.Type.Predicate.Param-import           Data.Type.Predicate.Quantification-import           Data.Type.Universe+import Data.Functor.Identity+import Data.List.NonEmpty (NonEmpty (..))+import Data.Singletons+import Data.Singletons.Sigma+import Data.Type.Equality+import Data.Type.Functor.Product+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 -- @a@.@@ -76,14 +78,14 @@ -- 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@.-    ---    -- Must be called using type application syntax:-    ---    -- @-    -- 'auto' @_ @p @a-    -- @-    auto :: p @@ a+  -- | Have the compiler generate a witness for @p \@\@ a@.+  --+  -- Must be called using type application syntax:+  --+  -- @+  -- 'auto' @_ @p @a+  -- @+  auto :: p @@ a  -- | A version of 'auto' that "just works" with type inference, if the -- predicate is a type constructor.@@ -93,20 +95,20 @@ autoTC = auto @_ @(TyPred t) @a  instance SingI a => Auto Evident a where-    auto = sing+  auto = sing  -- | @since 0.1.2.0 instance SingI a => Auto (Not Impossible) a where-    auto = ($ sing)+  auto = ($ sing)  instance Auto (EqualTo a) a where-    auto = Refl+  auto = Refl  instance (Auto p a, Auto q a) => Auto (p &&& q) a where-    auto = (auto @_ @p @a, auto @_ @q @a)+  auto = (auto @_ @p @a, auto @_ @q @a)  instance Auto q a => Auto (p ==> q) a where-    auto _ = auto @_ @q @a+  auto _ = auto @_ @q @a  -- | Helper "predicate transformer" that gives you an instant 'auto' for -- any 'Provable' instance.@@ -123,10 +125,11 @@ -- -- 'AutoProvable' is essentially the identity function. data AutoProvable :: Predicate k -> Predicate k+ type instance Apply (AutoProvable p) a = p @@ a  instance (Provable p, SingI a) => Auto (AutoProvable p) a where-    auto = prove @p @a sing+  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@.@@ -150,37 +153,37 @@ -- -- IS (IS IZ) -- @ class AutoElem f (as :: f k) (a :: k) where-    -- | Generate the 'Elem' pointing to the @a :: @ in a type-level-    -- collection @as :: f k@.-    autoElem :: Elem f as a+  -- | Generate the 'Elem' pointing to the @a :: @ in a type-level+  -- collection @as :: f k@.+  autoElem :: Elem f as a  instance {-# OVERLAPPING #-} AutoElem [] (a ': as) a where-    autoElem = IZ+  autoElem = IZ  instance {-# OVERLAPPING #-} AutoElem [] as a => AutoElem [] (b ': as) a where-    autoElem = IS autoElem+  autoElem = IS autoElem  instance AutoElem Maybe ('Just a) a where-    autoElem = IJust+  autoElem = IJust  instance AutoElem (Either j) ('Right a) a where-    autoElem = IRight+  autoElem = IRight  instance AutoElem NonEmpty (a ':| as) a where-    autoElem = NEHead+  autoElem = NEHead  instance AutoElem [] as a => AutoElem NonEmpty (b ':| as) a where-    autoElem = NETail autoElem+  autoElem = NETail autoElem  -- | @since 0.1.2.0 instance AutoElem ((,) j) '(w, a) a where-    autoElem = ISnd+  autoElem = ISnd  instance AutoElem Identity ('Identity a) a where-    autoElem = IId+  autoElem = IId  instance AutoElem f as a => Auto (In f as) a where-    auto = autoElem @_ @f @as @a+  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@@ -191,66 +194,66 @@ -- -- @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+  -- | Generate an 'All' for a given predicate over all items in @as@.+  autoAll :: All f p @@ as  instance AutoAll [] p '[] where-    autoAll = WitAll $ \case {}+  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+  autoAll = WitAll $ \case+    IZ -> auto @_ @p @a+    IS i -> runWitAll (autoAll @_ @[] @p @as) i  instance AutoAll Maybe p 'Nothing where-    autoAll = WitAll $ \case {}+  autoAll = WitAll $ \case {}  instance Auto p a => AutoAll Maybe p ('Just a) where-    autoAll = WitAll $ \case IJust -> auto @_ @p @a+  autoAll = WitAll $ \case IJust -> auto @_ @p @a  instance AutoAll (Either j) p ('Left e) where-    autoAll = WitAll $ \case {}+  autoAll = WitAll $ \case {}  instance Auto p a => AutoAll (Either j) p ('Right a) where-    autoAll = WitAll $ \case IRight -> auto @_ @p @a+  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+  autoAll = WitAll $ \case+    NEHead -> auto @_ @p @a+    NETail i -> runWitAll (autoAll @_ @[] @p @as) i  instance Auto p a => AutoAll ((,) j) p '(w, a) where-    autoAll = WitAll $ \case ISnd -> auto @_ @p @a+  autoAll = WitAll $ \case ISnd -> auto @_ @p @a  instance Auto p a => AutoAll Identity p ('Identity a) where-    autoAll = WitAll $ \case IId -> auto @_ @p @a+  autoAll = WitAll $ \case IId -> auto @_ @p @a  -- | @since 0.1.2.0 instance AutoAll f p as => Auto (All f p) as where-    auto = autoAll @_ @f @p @as+  auto = autoAll @_ @f @p @as  -- | @since 0.1.2.0 instance SingI a => Auto (NotNull []) (a ': as) where-    auto = WitAny IZ sing+  auto = WitAny IZ sing  -- | @since 0.1.2.0 instance SingI a => Auto IsJust ('Just a) where-    auto = WitAny IJust sing+  auto = WitAny IJust sing  -- | @since 0.1.2.0 instance SingI a => Auto IsRight ('Right a) where-    auto = WitAny IRight sing+  auto = WitAny IRight sing  -- | @since 0.1.2.0 instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where-    auto = WitAny NEHead sing+  auto = WitAny NEHead sing  -- | @since 0.1.2.0 instance SingI a => Auto (NotNull ((,) j)) '(w, a) where-    auto = WitAny ISnd sing+  auto = WitAny ISnd sing  instance SingI a => Auto (NotNull Identity) ('Identity a) where-    auto = WitAny IId sing+  auto = WitAny IId sing  -- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to -- not be true at compiletime.@@ -270,21 +273,22 @@  -- | @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+  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)+  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)+  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)+  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.@@ -293,15 +297,16 @@ -- 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 ::+  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+  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.@@ -310,51 +315,63 @@ -- 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 ::+  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+  auto =+    mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p)) $+      auto @_ @(Not (Any f (Found p))) @as  -- | @since 3.0.0 instance SingI as => Auto (TyPred (Rec WrappedSing)) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance SingI as => Auto (TyPred (PMaybe WrappedSing)) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance SingI as => Auto (TyPred (NERec WrappedSing)) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance SingI as => Auto (TyPred (PEither WrappedSing)) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance SingI as => Auto (TyPred (PTup WrappedSing)) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance SingI as => Auto (TyPred (PIdentity WrappedSing)) as where-    auto = proveTC sing+  auto = proveTC sing  -- | @since 3.0.0 instance (SingI as, Provable p) => Auto (TyPred (Rec (Wit p))) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance (SingI as, Provable p) => Auto (TyPred (PMaybe (Wit p))) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance (SingI as, Provable p) => Auto (TyPred (NERec (Wit p))) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance (SingI as, Provable p) => Auto (TyPred (PEither (Wit p))) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance (SingI as, Provable p) => Auto (TyPred (PTup (Wit p))) as where-    auto = proveTC sing+  auto = proveTC sing+ -- | @since 3.0.0 instance (SingI as, Provable p) => Auto (TyPred (PIdentity (Wit p))) as where-    auto = proveTC sing+  auto = proveTC sing

@@ -1,15 +1,16 @@ {-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ConstraintKinds     #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE FlexibleInstances   #-}-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TupleSections       #-}-{-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE TypeFamilies        #-}-{-# LANGUAGE TypeInType          #-}-{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}  -- | -- Module      : Data.Type.Predicate.Logic@@ -24,68 +25,94 @@ -- logical combinators. module Data.Type.Predicate.Logic (   -- * Top and bottom-    Evident, Impossible+  Evident,+  Impossible,+   -- * Logical connectives-  , type Not, decideNot-  , type (&&&), decideAnd-  , type (|||), decideOr, type (^||), type (||^)-  , type (^^^), decideXor-  , type (==>), proveImplies, Implies-  , type (<==>), Equiv+  type Not,+  decideNot,+  type (&&&),+  decideAnd,+  type (|||),+  decideOr,+  type (^||),+  type (||^),+  type (^^^),+  decideXor,+  type (==>),+  proveImplies,+  Implies,+  type (<==>),+  Equiv,+   -- * Logical deductions-  , compImpl, explosion, atom-  , complementation, doubleNegation, tripleNegation, negateTwice-  , contrapositive, contrapositive'+  compImpl,+  explosion,+  atom,+  complementation,+  doubleNegation,+  tripleNegation,+  negateTwice,+  contrapositive,+  contrapositive',+   -- ** Lattice-  , projAndFst, projAndSnd, injOrLeft, injOrRight-  ) where+  projAndFst,+  projAndSnd,+  injOrLeft,+  injOrRight,+) where -import           Data.Singletons-import           Data.Singletons.Decide-import           Data.Type.Predicate-import           Data.Void+import Data.Singletons+import Data.Singletons.Decide+import Data.Type.Predicate+import Data.Void  -- | @p '&&&' q@ is a predicate that both @p@ and @q@ are true. data (&&&) :: Predicate k -> Predicate k -> Predicate k+ type instance Apply (p &&& q) a = (p @@ a, q @@ a) infixr 3 &&&  instance (Decidable p, Decidable q) => Decidable (p &&& q) where-    decide (x :: Sing a) = decideAnd @p @q @a (decide @p x) (decide @q x)+  decide (x :: Sing a) = decideAnd @p @q @a (decide @p x) (decide @q x)  instance (Provable p, Provable q) => Provable (p &&& q) where-    prove x = (prove @p x, prove @q x)+  prove x = (prove @p x, prove @q x)  -- | Decide @p '&&&' q@ based on decisions of @p@ and @q@.-decideAnd-    :: forall p q a. ()-    => Decision (p @@ a)-    -> Decision (q @@ a)-    -> Decision ((p &&& q) @@ a)+decideAnd ::+  forall p q a.+  () =>+  Decision (p @@ a) ->+  Decision (q @@ a) ->+  Decision ((p &&& q) @@ a) decideAnd = \case-    Proved p    -> mapDecision (p,) snd-    Disproved v -> \_ -> Disproved $ \(p, _) -> v p+  Proved p -> mapDecision (p,) snd+  Disproved v -> \_ -> Disproved $ \(p, _) -> v p  -- | @p '|||' q@ is a predicate that either @p@ and @q@ are true. data (|||) :: Predicate k -> Predicate k -> Predicate k+ type instance Apply (p ||| q) a = Either (p @@ a) (q @@ a) infixr 2 |||  -- | Prefers @p@ over @q@. instance (Decidable p, Decidable q) => Decidable (p ||| q) where-    decide (x :: Sing a) = decideOr @p @q @a (decide @p x) (decide @q x)+  decide (x :: Sing a) = decideOr @p @q @a (decide @p x) (decide @q x)  -- | Decide @p '|||' q@ based on decisions of @p@ and @q@. -- -- Prefers @p@ over @q@.-decideOr-    :: forall p q a. ()-    => Decision (p @@ a)-    -> Decision (q @@ a)-    -> Decision ((p ||| q) @@ a)+decideOr ::+  forall p q a.+  () =>+  Decision (p @@ a) ->+  Decision (q @@ a) ->+  Decision ((p ||| q) @@ a) decideOr = \case-    Proved p    -> \_ -> Proved $ Left p-    Disproved v -> mapDecision Right (either (absurd . v) id)+  Proved p -> \_ -> Proved $ Left p+  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.@@ -104,78 +131,87 @@ type p ^^^ q = (p &&& Not q) ||| (Not p &&& q)  -- | Decide @p '^^^' q@ based on decisions of @p@ and @q@.-decideXor-    :: forall p q a. ()-    => Decision (p @@ a)-    -> Decision (q @@ a)-    -> Decision ((p ^^^ q) @@ a)-decideXor p q = decideOr @(p &&& Not q) @(Not p &&& q) @a-                  (decideAnd @p @(Not q) @a p (decideNot @q @a q))-                  (decideAnd @(Not p) @q @a (decideNot @p @a p) q)+decideXor ::+  forall p q a.+  () =>+  Decision (p @@ a) ->+  Decision (q @@ a) ->+  Decision ((p ^^^ q) @@ a)+decideXor p q =+  decideOr @(p &&& Not q) @(Not p &&& q) @a+    (decideAnd @p @(Not q) @a p (decideNot @q @a q))+    (decideAnd @(Not p) @q @a (decideNot @p @a p) q)  -- | @p ==> q@ is true if @q@ is provably true under the condition that @p@ -- is true. data (==>) :: Predicate k -> Predicate k -> Predicate k+ type instance Apply (p ==> q) a = p @@ a -> q @@ a  infixr 1 ==> -instance Decidable (Impossible ==> p) where+instance Decidable (Impossible ==> p) instance Provable (Impossible ==> p) where-    prove = explosion @p+  prove = explosion @p  instance (Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p) where-    decide x = case decide @(p ==> q) x of-      Proved pq     -> Proved $ \vq p -> vq (pq p)-      Disproved vpq -> case decide @q x of-        Proved    q  -> Disproved $ \_     -> vpq (const q)-        Disproved vq -> Disproved $ \vnpnq -> vpq (absurd . vnpnq vq)+  decide x = case decide @(p ==> q) x of+    Proved pq -> Proved $ \vq p -> vq (pq p)+    Disproved vpq -> case decide @q x of+      Proved q -> Disproved $ \_ -> vpq (const q)+      Disproved vq -> Disproved $ \vnpnq -> vpq (absurd . vnpnq vq) instance Provable (p ==> q) => Provable (Not q ==> Not p) where-    prove = contrapositive @p @q (prove @(p ==> q))+  prove = contrapositive @p @q (prove @(p ==> q))  -- | @since 0.1.1.0-instance {-# OVERLAPPING #-} Decidable (p &&& q ==> p) where+instance {-# OVERLAPPING #-} Decidable (p &&& q ==> p)+ -- | @since 0.1.1.0 instance {-# OVERLAPPING #-} Provable (p &&& q ==> p) where-    prove = projAndFst @p @q+  prove = projAndFst @p @q  -- | @since 0.1.1.0-instance {-# OVERLAPPING #-} Decidable (p &&& q ==> q) where+instance {-# OVERLAPPING #-} Decidable (p &&& q ==> q)+ -- | @since 0.1.1.0 instance {-# OVERLAPPING #-} Provable (p &&& q ==> q) where-    prove = projAndSnd @p @q+  prove = projAndSnd @p @q  -- | @since 0.1.1.0-instance {-# OVERLAPPING #-} Decidable (p &&& p ==> p) where+instance {-# OVERLAPPING #-} Decidable (p &&& p ==> p)+ -- | @since 0.1.1.0 instance {-# OVERLAPPING #-} Provable (p &&& p ==> p) where-    prove = projAndFst @p @p+  prove = projAndFst @p @p  -- | @since 0.1.1.0 instance {-# OVERLAPPING #-} Decidable (p ==> p ||| q)+ -- | @since 0.1.1.0 instance {-# OVERLAPPING #-} Provable (p ==> p ||| q) where-    prove = injOrLeft @p @q+  prove = injOrLeft @p @q  -- | @since 0.1.1.0 instance {-# OVERLAPPING #-} Decidable (q ==> p ||| q)+ -- | @since 0.1.1.0 instance {-# OVERLAPPING #-} Provable (q ==> p ||| q) where-    prove = injOrRight @p @q+  prove = injOrRight @p @q  -- | @since 0.1.1.0 instance {-# OVERLAPPING #-} Decidable (p ==> p ||| p)+ -- | @since 0.1.1.0 instance {-# OVERLAPPING #-} Provable (p ==> p ||| p) where-    prove = injOrLeft @p @p+  prove = injOrLeft @p @p  -- | @'Implies' p q@ is a constraint that @p '==>' q@ is 'Provable'; that -- is, you can prove that @p@ implies @q@.-type Implies  p q = Provable  (p ==> q)+type Implies p q = Provable (p ==> q)  -- | @'Equiv' p q@ is a constraint that @p '<==>' q@ is 'Provable'; that -- is, you can prove that @p@ is logically equivalent to @q@.-type Equiv  p q = Provable  (p <==> q)+type Equiv p q = Provable (p <==> q)  -- | If @q@ is provable, then so is @p '==>' q@. --@@ -193,7 +229,8 @@ proveImplies q x _ = q x  -- | Two-way implication, or logical equivalence-type (p <==> q) = p ==> q &&& q ==> p+type p <==> q = p ==> q &&& q ==> p+ infixr 1 <==>  -- | From @'Impossible' @@ a@, you can prove anything.  Essentially@@ -215,23 +252,24 @@  -- | @since 0.1.3.0 instance {-# OVERLAPPING #-} Provable (p &&& Not p ==> Impossible) where-    prove = complementation @p+  prove = complementation @p  -- | If p implies q, then not q implies not p.-contrapositive-    :: (p --> q)-    -> (Not q --> Not p)+contrapositive ::+  (p --> q) ->+  (Not q --> Not 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 -- less useful.-contrapositive'-    :: forall p q. Decidable q-    => (Not q --> Not p)-    -> (p --> q)+contrapositive' ::+  forall p q.+  Decidable q =>+  (Not q --> Not p) ->+  (p --> q) contrapositive' f x p = elimDisproof (decide @q x) $ \vQ ->-    f x vQ p+  f x vQ p  -- | Logical double negation.  Only possible if @p@ is 'Decidable'. --@@ -240,7 +278,7 @@ -- 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+  vvP vP  -- | In constructivist logic, not (not (not p)) implies not p. --

@@ -1,13 +1,14 @@-{-# LANGUAGE ConstraintKinds      #-}-{-# LANGUAGE FlexibleContexts     #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE GADTs                #-}-{-# LANGUAGE LambdaCase           #-}-{-# LANGUAGE ScopedTypeVariables  #-}-{-# LANGUAGE TypeApplications     #-}-{-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE TypeInType           #-}-{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}  -- |@@ -21,33 +22,49 @@ -- -- Manipulate "parameterized predicates".  See 'ParamPred' and 'Found' for -- more information.--- module Data.Type.Predicate.Param (   -- * Parameterized Predicates-    ParamPred-  , IsTC, EqBy-  , FlipPP, ConstPP, PPMap, PPMapV, InP, AnyMatch, TyPP+  ParamPred,+  IsTC,+  EqBy,+  FlipPP,+  ConstPP,+  PPMap,+  PPMapV,+  InP,+  AnyMatch,+  TyPP,+   -- * Deciding and Proving-  , Found, NotFound-  , Selectable, select-  , Searchable, search-  , inPNotNull, notNullInP+  Found,+  NotFound,+  Selectable,+  select,+  Searchable,+  search,+  inPNotNull,+  notNullInP,+   -- ** Type Constructors-  , SelectableTC, selectTC-  , SearchableTC, searchTC+  SelectableTC,+  selectTC,+  SearchableTC,+  searchTC,+   -- * Combining-  , OrP, AndP-  ) where+  OrP,+  AndP,+) where -import           Data.Kind-import           Data.Singletons-import           Data.Singletons.Decide-import           Data.Singletons.Sigma-import           Data.Tuple.Singletons-import           Data.Type.Functor.Product-import           Data.Type.Predicate-import           Data.Type.Predicate.Logic-import           Data.Type.Universe+import Data.Kind+import Data.Singletons+import Data.Singletons.Decide+import Data.Singletons.Sigma+import Data.Tuple.Singletons+import Data.Type.Functor.Product+import Data.Type.Predicate+import Data.Type.Predicate.Logic+import Data.Type.Universe  -- | A parameterized predicate.  See 'Found' for more information. type ParamPred k v = k -> Predicate v@@ -72,6 +89,7 @@ -- :: k@, we can prove or disprove the fact that there exists a @y :: v@ -- 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.@@ -97,11 +115,13 @@  -- | Flip the arguments of a 'ParamPred'. data FlipPP :: ParamPred v k -> ParamPred k v+ type instance Apply (FlipPP p x) y = p y @@ x  -- | Promote a @'Predicate' v@ to a @'ParamPred' k v@, ignoring the @k@ -- input. 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,@@ -116,6 +136,7 @@ -- -- @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@@ -158,29 +179,34 @@ -- -- @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. 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)-           . decide @(Found p)-           . applySing (sing :: Sing f)     -- can just be sing @f in singletons 2.5, ghc 8.6++  decide =+    mapDecision+      (\case i :&: p -> i :&: p)+      (\case i :&: p -> i :&: p)+      . decide @(Found p)+      . applySing (sing :: Sing f) -- can just be sing @f in singletons 2.5, ghc 8.6+  instance (Provable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Provable (Found (PPMap f p)) where-    prove (x :: Sing a) = case prove @(Found p) ((sing :: Sing f) @@ x) of-        i :&: p -> i :&: p+  prove (x :: Sing a) = case prove @(Found p) ((sing :: Sing f) @@ x) of+    i :&: p -> i :&: p  -- | A constraint that a @'ParamPred' k v@ is "searchable".  It means that -- for any input @x :: k@, we can prove or disprove that there exists a @y@@ -191,7 +217,7 @@ -- | A constraint that a @'ParamPred' k v@ s "selectable".  It means that -- for any input @x :: k@, we can always find a @y :: v@ that satisfies @P -- x \@\@ y@.  We can "select" that @y@, no matter what.-type Selectable p = Provable  (Found p)+type Selectable p = Provable (Found p)  -- | The deciding/searching function for @'Searchable' p@. --@@ -204,9 +230,10 @@ -- -- 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)+search ::+  forall p.+  Searchable p =>+  Decide (Found p) search = decide @(Found p)  -- | The proving/selecting function for @'Selectable' p@.@@ -220,9 +247,10 @@ -- -- 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)+select ::+  forall p.+  Selectable p =>+  Prove (Found p) select = prove @(Found p)  -- | If @T :: k -> v -> 'Type'@ is a type constructor, then @'SearchableTC'@@ -261,7 +289,7 @@ -- TypeApplications to use. -- -- @since 0.1.4.0-type SelectableTC t = Provable  (Found (TyPP t))+type SelectableTC t = Provable (Found (TyPP t))  -- | The canonical selecting function for @'Searchable' t@. --@@ -270,9 +298,10 @@ -- can be inferred from the result type. -- -- @since 0.1.4.0-searchTC-    :: forall t. SearchableTC t-    => Decide (Found (TyPP t))+searchTC ::+  forall t.+  SearchableTC t =>+  Decide (Found (TyPP t)) searchTC = search @(TyPP t)  -- | The canonical selecting function for @'SelectableTC' t@.@@ -282,9 +311,10 @@ -- can be inferred from the result type. -- -- @since 0.1.4.0-selectTC-    :: forall t. SelectableTC t-    => Prove (Found (TyPP t))+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@@ -306,17 +336,19 @@ 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)-           . decide @(NotNull f)+  decide =+    mapDecision+      (\case WitAny i s -> s :&: i)+      (\case s :&: i -> WitAny i s)+      . decide @(NotNull f)  instance Decidable (NotNull f ==> Found (InP f)) instance Provable (NotNull f ==> Found (InP f)) where-    prove = notNullInP+  prove = notNullInP  instance Decidable (Found (InP f) ==> NotNull f) instance Provable (Found (InP f) ==> NotNull f) where-    prove = inPNotNull+  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@@ -329,18 +361,22 @@ -- A @'ParamPred' k v@ tests if a @k@ can create some @v@.  The resulting -- @'ParamPred' (f k) v@ tests if any @k@ in @f k@ can create some @v@. data AnyMatch f :: ParamPred k v -> ParamPred (f k) v+ type instance Apply (AnyMatch f p as) a = Any f (FlipPP p a) @@ as  instance (Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p)) where-    decide = mapDecision (\case WitAny i (x :&: p) -> x :&: WitAny i p  )-                         (\case x :&: WitAny i p   -> WitAny i (x :&: p))-           . decide @(Any f (Found p))+  decide =+    mapDecision+      (\case WitAny i (x :&: p) -> x :&: WitAny i p)+      (\case x :&: WitAny i p -> WitAny i (x :&: p))+      . decide @(Any f (Found p))  -- | Disjunction on two 'ParamPred's, with appropriate 'Searchable' -- instance.  Priority is given to the left predicate. -- -- @since 0.1.3.0 data OrP :: ParamPred k v -> ParamPred k v -> ParamPred k v+ type instance Apply (OrP p q x) y = (p x ||| q x) @@ y  -- | Conjunction on two 'ParamPred's, with appropriate 'Searchable' and@@ -348,27 +384,28 @@ -- -- @since 0.1.3.0 data AndP :: ParamPred k v -> ParamPred k u -> ParamPred k (v, u)+ type instance Apply (AndP p q x) '(y, z) = (p x @@ y, q x @@ z)  instance (Searchable p, Searchable q) => Decidable (Found (OrP p q)) where-    decide x = case search @p x of-      Proved (s :&: p) -> Proved $ s :&: Left p-      Disproved vp     -> case search @q x of-        Proved (s :&: q) -> Proved $ s :&: Right q-        Disproved vq     -> Disproved $ \case-          s :&: Left  p -> vp (s :&: p)-          s :&: Right q -> vq (s :&: q)+  decide x = case search @p x of+    Proved (s :&: p) -> Proved $ s :&: Left p+    Disproved vp -> case search @q x of+      Proved (s :&: q) -> Proved $ s :&: Right q+      Disproved vq -> Disproved $ \case+        s :&: Left p -> vp (s :&: p)+        s :&: Right q -> vq (s :&: q)  instance (Searchable p, Searchable q) => Decidable (Found (AndP p q)) where-    decide x = case search @p x of-      Proved (s :&: p) -> case search @q x of-        Proved (t :&: q) -> Proved $ STuple2 s t :&: (p, q)-        Disproved vq     -> Disproved $ \case-          STuple2 _ t :&: (_, q) -> vq $ t :&: q-      Disproved vp     -> Disproved $ \case-        STuple2 s _ :&: (p, _) -> vp $ s :&: p+  decide x = case search @p x of+    Proved (s :&: p) -> case search @q x of+      Proved (t :&: q) -> Proved $ STuple2 s t :&: (p, q)+      Disproved vq -> Disproved $ \case+        STuple2 _ t :&: (_, q) -> vq $ t :&: q+    Disproved vp -> Disproved $ \case+      STuple2 s _ :&: (p, _) -> vp $ s :&: p  instance (Selectable p, Selectable q) => Provable (Found (AndP p q)) where-    prove x = case select @p x of-        s :&: p -> case select @q x of-          t :&: q -> STuple2 s t :&: (p, q)+  prove x = case select @p x of+    s :&: p -> case select @q x of+      t :&: q -> STuple2 s t :&: (p, q)

@@ -1,10 +1,11 @@-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE TypeFamilies        #-}-{-# LANGUAGE TypeInType          #-}-{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}  -- | -- Module      : Data.Type.Predicate.Quantification@@ -17,40 +18,66 @@ -- -- Higher-level predicates for quantifying predicates over universes and -- sets.--- module Data.Type.Predicate.Quantification (   -- * Any-    Any, WitAny(..), None, anyImpossible+  Any,+  WitAny (..),+  None,+  anyImpossible,+   -- ** Decision-  , decideAny, idecideAny, decideNone, idecideNone+  decideAny,+  idecideAny,+  decideNone,+  idecideNone,+   -- ** Entailment-  , entailAny, ientailAny, entailAnyF, ientailAnyF+  entailAny,+  ientailAny,+  entailAnyF,+  ientailAnyF,+   -- * All-  , All, WitAll(..), NotAll+  All,+  WitAll (..),+  NotAll,+   -- ** Decision-  , decideAll, idecideAll+  decideAll,+  idecideAll,+   -- ** Entailment-  , entailAll, ientailAll, entailAllF, ientailAllF-  , decideEntailAll, idecideEntailAll+  entailAll,+  ientailAll,+  entailAllF,+  ientailAllF,+  decideEntailAll,+  idecideEntailAll,+   -- * Logical interplay-  , allToAny-  , allNotNone, noneAllNot-  , anyNotNotAll, notAllAnyNot-  ) where+  allToAny,+  allNotNone,+  noneAllNot,+  anyNotNotAll,+  notAllAnyNot,+) where -import           Data.Kind-import           Data.Singletons-import           Data.Singletons.Decide-import           Data.Type.Functor.Product-import           Data.Type.Predicate-import           Data.Type.Predicate.Logic-import           Data.Type.Universe+import Data.Kind+import Data.Singletons+import Data.Singletons.Decide+import Data.Type.Functor.Product+import Data.Type.Predicate+import Data.Type.Predicate.Logic+import Data.Type.Universe  -- | 'decideNone', but providing an 'Elem'.-idecideNone-    :: forall f k (p :: k ~> Type) (as :: f k). Universe f-    => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))    -- ^ predicate on value-    -> (Sing as -> Decision (None f p @@ as))                    -- ^ predicate on collection+idecideNone ::+  forall f k (p :: k ~> Type) (as :: f k).+  Universe f =>+  -- | predicate on value+  (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->+  -- | predicate on collection+  (Sing as -> Decision (None f p @@ as)) idecideNone f xs = decideNot @(Any f p) $ idecideAny f xs  -- | Lifts a predicate @p@ on an individual @a@ into a predicate that on@@ -59,50 +86,61 @@ -- -- That is, it turns a predicate of kind @k ~> Type@ into a predicate -- of kind @f k ~> Type@.-decideNone-    :: forall f k (p :: k ~> Type). Universe f-    => Decide p                         -- ^ predicate on value-    -> Decide (None f p)                -- ^ predicate on collection+decideNone ::+  forall f k (p :: k ~> Type).+  Universe f =>+  -- | predicate on value+  Decide p ->+  -- | predicate on collection+  Decide (None f p) decideNone f = idecideNone (const f)  -- | 'entailAny', but providing an 'Elem'.-ientailAny-    :: forall f p q as. (Universe f, SingI as)-    => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)        -- ^ implication-    -> Any f p @@ as-    -> Any f q @@ as+ientailAny ::+  forall f p q as.+  (Universe f, SingI as) =>+  -- | implication+  (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) ->+  Any f p @@ as ->+  Any f q @@ as ientailAny f (WitAny i x) = WitAny i (f i (indexSing i sing) x)  -- | If there exists an @a@ s.t. @p a@, and if @p@ implies @q@, then there -- must exist an @a@ s.t. @q a@.-entailAny-    :: forall f p q. Universe f-    => (p --> q)-    -> (Any f p --> Any f q)+entailAny ::+  forall f p q.+  Universe f =>+  (p --> q) ->+  (Any f p --> Any f q) entailAny = tmap @(Any f)  -- | 'entailAll', but providing an 'Elem'.-ientailAll-    :: forall f p q as. (Universe f, SingI as)-    => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)      -- ^ implication-    -> All f p @@ as-    -> All f q @@ as+ientailAll ::+  forall f p q as.+  (Universe f, SingI as) =>+  -- | implication+  (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) ->+  All f p @@ as ->+  All f q @@ as ientailAll f a = WitAll $ \i -> f i (indexSing i sing) (runWitAll a i)  -- | If for all @a@ we have @p a@, and if @p@ implies @q@, then for all @a@ -- we must also have @p a@.-entailAll-    :: forall f p q. Universe f-    => (p --> q)-    -> (All f p --> All f q)+entailAll ::+  forall f p q.+  Universe f =>+  (p --> q) ->+  (All f p --> All f q) entailAll = tmap @(All f)  -- | 'entailAnyF', but providing an 'Elem'.-ientailAnyF-    :: forall f p q as h. Functor h-    => (forall a. Elem f as a -> p @@ a -> h (q @@ a))      -- ^ implication in context-    -> Any f p @@ as-    -> h (Any f q @@ as)+ientailAnyF ::+  forall f p q as h.+  Functor h =>+  -- | implication in context+  (forall a. Elem f as a -> p @@ a -> h (q @@ a)) ->+  Any f p @@ as ->+  h (Any f q @@ as) ientailAnyF f = \case WitAny i x -> WitAny i <$> f i x  -- | If @p@ implies @q@ under some context @h@, and if there exists some@@ -116,46 +154,58 @@ -- This is if the @p a -> 'Decision' (q a)@ implication is false, there -- it doesn't mean that there is /no/ @a@ such that @q a@, necessarily. -- There could have been an @a@ where @p@ does not hold, but @q@ does.-entailAnyF-    :: forall f p q h. (Universe f, Functor h)-    => (p --># q) h                                     -- ^ implication in context-    -> (Any f p --># Any f q) h-entailAnyF f x a = withSingI x $+entailAnyF ::+  forall f p q h.+  (Universe f, Functor h) =>+  -- | implication in context+  (p --># q) h ->+  (Any f p --># Any f q) h+entailAnyF f x a =+  withSingI x $     ientailAnyF @f @p @q (\i -> f (indexSing i x)) a  -- | 'entailAllF', but providing an 'Elem'.-ientailAllF-    :: forall f p q as h. (Universe f, Applicative h, SingI as)-    => (forall a. Elem f as a -> p @@ a -> h (q @@ a))    -- ^ implication in context-    -> All f p @@ as-    -> h (All f q @@ as)-ientailAllF f a = fmap (prodAll getWit)-                . itraverseProd (\i _ -> Wit @q <$> f i (runWitAll a i))-                $ singProd (sing @as)+ientailAllF ::+  forall f p q as h.+  (Universe f, Applicative h, SingI as) =>+  -- | implication in context+  (forall a. Elem f as a -> p @@ a -> h (q @@ a)) ->+  All f p @@ as ->+  h (All f q @@ as)+ientailAllF f a =+  fmap (prodAll getWit)+    . itraverseProd (\i _ -> Wit @q <$> f i (runWitAll a i))+    $ singProd (sing @as)  -- | If @p@ implies @q@ under some context @h@, and if we have @p a@ for -- all @a@, then we must have @q a@ for all @a@ under context @h@.-entailAllF-    :: forall f p q h. (Universe f, Applicative h)-    => (p --># q) h                                     -- ^ implication in context-    -> (All f p --># All f q) h-entailAllF f x a = withSingI x $+entailAllF ::+  forall f p q h.+  (Universe f, Applicative h) =>+  -- | implication in context+  (p --># q) h ->+  (All f p --># All f q) h+entailAllF f x a =+  withSingI x $     ientailAllF @f @p @q (\i -> f (indexSing i x)) a  -- | 'entailAllF', but providing an 'Elem'.-idecideEntailAll-    :: forall f p q as. (Universe f, SingI as)-    => (forall a. Elem f as a -> p @@ a -> Decision (q @@ a))     -- ^ decidable implication-    -> All f p @@ as-    -> Decision (All f q @@ as)+idecideEntailAll ::+  forall f p q as.+  (Universe f, SingI as) =>+  -- | decidable implication+  (forall a. Elem f as a -> p @@ a -> Decision (q @@ a)) ->+  All f p @@ as ->+  Decision (All f q @@ as) idecideEntailAll f a = idecideAll (\i _ -> f i (runWitAll a i)) sing  -- | If we have @p a@ for all @a@, and @p a@ can be used to test for @q a@, -- then we can test all @a@s for @q a@.-decideEntailAll-    :: forall f p q. Universe f-    => p -?> q-    -> All f p -?> All f q+decideEntailAll ::+  forall f p q.+  Universe f =>+  p -?> q ->+  All f p -?> All f q decideEntailAll = dmap @(All f)  -- | It is impossible for any value in a collection to be 'Impossible'.@@ -176,13 +226,14 @@ -- 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 ::+  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 (indexSing i xs)) $ \vP ->-        vAny $ WitAny i vP+  vAll $ WitAll $ \i ->+    elimDisproof (decide @p (indexSing i xs)) $ \vP ->+      vAny $ WitAny i vP  -- | If @p@ is false for all @a@ in @as@, then no @a@ in @as@ satisfies -- @p@.@@ -195,11 +246,12 @@ -- @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 ::+  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+  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.

@@ -1,21 +1,16 @@-{-# LANGUAGE CPP                    #-}-{-# 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 CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilyDependencies #-}-{-# LANGUAGE TypeInType             #-}-{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE TypeOperators #-}  -- | -- Module      : Data.Type.Universe@@ -28,47 +23,75 @@ -- -- A type family for "containers", intended for allowing lifting of -- predicates on @k@ to be predicates on containers @f k@.--- module Data.Type.Universe (   -- * Universe-    Elem, In, Universe(..)-  , singAll+  Elem,+  In,+  Universe (..),+  singAll,+   -- ** Instances-  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IIdentity(..)+  Index (..),+  IJust (..),+  IRight (..),+  NEIndex (..),+  ISnd (..),+  IIdentity (..),+   -- ** Predicates-  , All, WitAll(..), NotAll-  , Any, WitAny(..), None-  , Null, NotNull+  All,+  WitAll (..),+  NotAll,+  Any,+  WitAny (..),+  None,+  Null,+  NotNull,+   -- *** Specialized-  , IsJust, IsNothing, IsRight, IsLeft+  IsJust,+  IsNothing,+  IsRight,+  IsLeft,+   -- * Decisions and manipulations-  , decideAny, decideAll-  , genAll, igenAll-  , splitSing-  , pickElem-  ) where+  decideAny,+  decideAll,+  genAll,+  igenAll,+  splitSing,+  pickElem,+) where -import           Data.Either.Singletons hiding    (IsLeft, IsRight)-import           Data.Functor.Identity-import           Data.Functor.Identity.Singletons-import           Data.Kind-import           Data.List.NonEmpty               (NonEmpty(..))-import           Data.List.Singletons hiding      (Elem, ElemSym0, ElemSym1, ElemSym2, All, Any, Null)-import           Data.Maybe.Singletons hiding     (IsJust, IsNothing)-import           Data.Singletons-import           Data.Singletons.Decide-import           Data.Tuple.Singletons-import           Data.Type.Functor.Product-import           Data.Type.Predicate-import           Data.Type.Predicate.Logic-import           GHC.Generics                     ((:*:)(..))-import           Prelude hiding                   (any, all)-import qualified Data.List.NonEmpty.Singletons    as NE+import Data.Either.Singletons hiding (IsLeft, IsRight)+import Data.Functor.Identity+import Data.Functor.Identity.Singletons+import Data.Kind+import Data.List.NonEmpty (NonEmpty (..))+import qualified Data.List.NonEmpty.Singletons as NE+import Data.List.Singletons hiding (+  All,+  Any,+  Elem,+  ElemSym0,+  ElemSym1,+  ElemSym2,+  Null,+ )+import Data.Maybe.Singletons hiding (IsJust, IsNothing)+import Data.Singletons+import Data.Singletons.Decide+import Data.Tuple.Singletons+import Data.Type.Functor.Product+import Data.Type.Predicate+import Data.Type.Predicate.Logic+import GHC.Generics ((:*:) (..))+import Prelude hiding (all, any)  -- | A @'WitAny' p as@ is a witness that, for at least one item @a@ in the -- type-level collection @as@, the predicate @p a@ is true. data WitAny f :: (k ~> Type) -> f k -> Type where-    WitAny :: Elem f as a -> p @@ a -> WitAny f p as+  WitAny :: Elem f as a -> p @@ a -> WitAny f p as  -- | An @'Any' f p@ is a predicate testing a collection @as :: f a@ for the -- fact that at least one item in @as@ satisfies @p@.  Represents the@@ -77,11 +100,12 @@ -- This is mostly useful for its 'Decidable' and 'TFunctor' instances, -- which lets you lift predicates on @p@ to predicates on @'Any' f p@. data Any f :: Predicate k -> Predicate (f k)+ type instance Apply (Any f p) as = WitAny f p as  -- | A @'WitAll' p as@ is a witness that the predicate @p a@ is true for all -- items @a@ in the type-level collection @as@.-newtype WitAll f p (as :: f k) = WitAll { runWitAll :: forall a. Elem f as a -> p @@ a }+newtype WitAll f p (as :: f k) = WitAll {runWitAll :: forall a. Elem f as a -> p @@ a}  -- | An @'All' f p@ is a predicate testing a collection @as :: f a@ for the -- fact that /all/ items in @as@ satisfy @p@.  Represents the "forall"@@ -91,60 +115,68 @@ -- instances, which lets you lift predicates on @p@ to predicates on @'All' -- f p@. data All f :: Predicate k -> Predicate (f k)+ type instance Apply (All f p) as = WitAll f p as  instance (Universe f, Decidable p) => Decidable (Any f p) where-    decide = decideAny @f @_ @p $ decide @p+  decide = decideAny @f @_ @p $ decide @p  instance (Universe f, Decidable p) => Decidable (All f p) where-    decide = decideAll @f @_ @p $ decide @p+  decide = decideAll @f @_ @p $ decide @p -instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p) where+instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p)  instance Provable p => Provable (NotNull f ==> Any f p) where-    prove _ (WitAny i s) = WitAny i (prove @p s)+  prove _ (WitAny i s) = WitAny i (prove @p s)  instance (Universe f, Provable p) => Provable (All f p) where-    prove xs = WitAll $ \i -> prove @p (indexSing i xs)+  prove xs = WitAll $ \i -> prove @p (indexSing i xs)  instance Universe f => TFunctor (Any f) where-    tmap f xs (WitAny i x) = WitAny i (f (indexSing i xs) x)+  tmap f xs (WitAny i x) = WitAny i (f (indexSing i xs) x)  instance Universe f => TFunctor (All f) where-    tmap f xs a = WitAll $ \i -> f (indexSing i xs) (runWitAll a i)+  tmap f xs a = WitAll $ \i -> f (indexSing i xs) (runWitAll a i)  instance Universe f => DFunctor (All f) where-    dmap f xs a = idecideAll (\i x -> f x (runWitAll a i)) xs+  dmap f xs a = idecideAll (\i x -> f x (runWitAll a i)) xs  -- | Typeclass for a type-level container that you can quantify or lift -- type-level predicates over. class FProd f => Universe (f :: Type -> Type) where--    -- | 'decideAny', but providing an 'Elem'.-    idecideAny-        :: forall k (p :: k ~> Type) (as :: f k). ()-        => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))   -- ^ predicate on value-        -> (Sing as -> Decision (Any f p @@ as))                         -- ^ predicate on collection+  -- | 'decideAny', but providing an 'Elem'.+  idecideAny ::+    forall k (p :: k ~> Type) (as :: f k).+    () =>+    -- | predicate on value+    (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->+    -- | predicate on collection+    (Sing as -> Decision (Any f p @@ as)) -    -- | 'decideAll', but providing an 'Elem'.-    idecideAll-        :: forall k (p :: k ~> Type) (as :: f k). ()-        => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))   -- ^ predicate on value-        -> (Sing as -> Decision (All f p @@ as))                         -- ^ predicate on collection+  -- | 'decideAll', but providing an 'Elem'.+  idecideAll ::+    forall k (p :: k ~> Type) (as :: f k).+    () =>+    -- | predicate on value+    (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->+    -- | predicate on collection+    (Sing as -> Decision (All f p @@ as)) -    allProd-        :: forall p g. ()-        => (forall a. Sing a -> p @@ a -> g a)-        -> All f p --> TyPred (Prod f g)+  allProd ::+    forall p g.+    () =>+    (forall a. Sing a -> p @@ a -> g a) ->+    All f p --> TyPred (Prod f g) -    prodAll-        :: forall p g as. ()-        => (forall a. g a -> p @@ a)-        -> Prod f g as-        -> All f p @@ as+  prodAll ::+    forall p g as.+    () =>+    (forall a. g a -> p @@ a) ->+    Prod f g as ->+    All f p @@ as  -- | Predicate that a given @as :: f k@ is empty and has no items in it.-type Null    f = (None f Evident :: Predicate (f k))+type Null f = (None f Evident :: Predicate (f k))  -- | Predicate that a given @as :: f k@ is not empty, and has at least one -- item in it.@@ -166,10 +198,13 @@ -- of kind @f k ~> Type@. -- -- Essentially tests existential quantification.-decideAny-    :: forall f k (p :: k ~> Type). Universe f-    => Decide p                                 -- ^ predicate on value-    -> Decide (Any f p)                -- ^ predicate on collection+decideAny ::+  forall f k (p :: k ~> Type).+  Universe f =>+  -- | predicate on value+  Decide p ->+  -- | predicate on collection+  Decide (Any f p) decideAny f = idecideAny (const f)  -- | Lifts a predicate @p@ on an individual @a@ into a predicate that on@@ -180,59 +215,73 @@ -- of kind @f k ~> Type@. -- -- Essentially tests universal quantification.-decideAll-    :: forall f k (p :: k ~> Type). Universe f-    => Decide p                                 -- ^ predicate on value-    -> Decide (All f p)                -- ^ predicate on collection+decideAll ::+  forall f k (p :: k ~> Type).+  Universe f =>+  -- | predicate on value+  Decide p ->+  -- | predicate on collection+  Decide (All f p) decideAll f = idecideAll (const f)  -- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.-splitSing-    :: forall f k (as :: f k). Universe f-    => Sing as-    -> All f (TyPred Sing) @@ as+splitSing ::+  forall f k (as :: f k).+  Universe f =>+  Sing as ->+  All f (TyPred Sing) @@ as splitSing = prodAll id . singProd  -- | Automatically generate a witness for a member, if possible-pickElem-    :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k)-    => Decision (Elem f as a)-pickElem = mapDecision (\case WitAny i Refl -> i)-                       (\case i -> WitAny i Refl)-         . decide @(Any f (TyPred ((:~:) a)))-         $ sing+pickElem ::+  forall f k (as :: f k) a.+  (Universe f, SingI as, SingI a, SDecide k) =>+  Decision (Elem f as a)+pickElem =+  mapDecision+    (\case WitAny i Refl -> i)+    (\case i -> WitAny i Refl)+    . decide @(Any f (TyPred ((:~:) a)))+    $ sing  -- | 'genAll', but providing an 'Elem'.-igenAll-    :: forall f k (p :: k ~> Type) (as :: f k). Universe f-    => (forall a. Elem f as a -> Sing a -> p @@ a)            -- ^ always-true predicate on value-    -> (Sing as -> All f p @@ as)                                  -- ^ always-true predicate on collection+igenAll ::+  forall f k (p :: k ~> Type) (as :: f k).+  Universe f =>+  -- | always-true predicate on value+  (forall a. Elem f as a -> Sing a -> p @@ a) ->+  -- | always-true predicate on collection+  (Sing as -> All f p @@ as) igenAll f = prodAll (\(i :*: x) -> f i x) . imapProd (:*:) . singProd  -- | If @p a@ is true for all values @a@ in @as@, then we have @'All' -- p as@.  Basically witnesses the definition of 'All'.-genAll-    :: forall f k (p :: k ~> Type). Universe f-    => Prove p                 -- ^ always-true predicate on value-    -> Prove (All f p)         -- ^ always-true predicate on collection+genAll ::+  forall f k (p :: k ~> Type).+  Universe f =>+  -- | always-true predicate on value+  Prove p ->+  -- | always-true predicate on collection+  Prove (All f p) genAll f = prodAll f . singProd  -- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.-singAll-    :: forall f k (as :: f k). Universe f-    => Sing as-    -> All f Evident @@ as+singAll ::+  forall f k (as :: f k).+  Universe f =>+  Sing as ->+  All f Evident @@ as singAll = prodAll id . singProd  -- | Test that a 'Maybe' is 'Just'. -- -- @since 0.1.2.0-type IsJust    = (NotNull Maybe :: Predicate (Maybe k))+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))+type IsNothing = (Null Maybe :: Predicate (Maybe k))  -- | Test that an 'Either' is 'Right' --@@ -242,168 +291,178 @@ -- | Test that an 'Either' is 'Left' -- -- @since 0.1.2.0-type IsLeft  = (Null    (Either j) :: Predicate (Either j k))-+type IsLeft = (Null (Either j) :: Predicate (Either j k))  instance Universe [] where-    idecideAny-        :: forall k (p :: k ~> Type) (as :: [k]). ()-        => (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))-        -> Sing as-        -> Decision (Any [] p @@ as)-    idecideAny f = \case-      SNil -> Disproved $ \case-        WitAny i _ -> case i of {}-      x `SCons` xs -> case f IZ x of-        Proved p    -> Proved $ WitAny IZ p-        Disproved v -> case idecideAny @[] @_ @p (f . IS) xs of-          Proved (WitAny i p) -> Proved $ WitAny (IS i) p-          Disproved vs -> Disproved $ \case-            WitAny IZ     p -> v p-            WitAny (IS i) p -> vs (WitAny i p)+  idecideAny ::+    forall k (p :: k ~> Type) (as :: [k]).+    () =>+    (forall a. Elem [] as a -> Sing a -> Decision (p @@ a)) ->+    Sing as ->+    Decision (Any [] p @@ as)+  idecideAny f = \case+    SNil -> Disproved $ \case+      WitAny i _ -> case i of {}+    x `SCons` xs -> case f IZ x of+      Proved p -> Proved $ WitAny IZ p+      Disproved v -> case idecideAny @[] @_ @p (f . IS) xs of+        Proved (WitAny i p) -> Proved $ WitAny (IS i) p+        Disproved vs -> Disproved $ \case+          WitAny IZ p -> v p+          WitAny (IS i) p -> vs (WitAny i p) -    idecideAll-        :: forall k (p :: k ~> Type) (as :: [k]). ()-        => (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))-        -> Sing as-        -> Decision (All [] p @@ as)-    idecideAll f = \case-      SNil -> Proved $ WitAll $ \case {}-      x `SCons` xs -> case f IZ x of-        Proved p -> case idecideAll @[] @_ @p (f . IS) xs of-          Proved a -> Proved $ WitAll $ \case-            IZ   -> p-            IS i -> runWitAll a i-          Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . IS)-        Disproved v -> Disproved $ \a -> v $ runWitAll a IZ+  idecideAll ::+    forall k (p :: k ~> Type) (as :: [k]).+    () =>+    (forall a. Elem [] as a -> Sing a -> Decision (p @@ a)) ->+    Sing as ->+    Decision (All [] p @@ as)+  idecideAll f = \case+    SNil -> Proved $ WitAll $ \case {}+    x `SCons` xs -> case f IZ x of+      Proved p -> case idecideAll @[] @_ @p (f . IS) xs of+        Proved a -> Proved $ WitAll $ \case+          IZ -> p+          IS i -> runWitAll a i+        Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . IS)+      Disproved v -> Disproved $ \a -> v $ runWitAll a IZ -    allProd-        :: forall p g. ()-        => (forall a. Sing a -> p @@ a -> g a)-        -> All [] p --> TyPred (Prod [] g)-    allProd f = go-      where-        go :: Sing as -> WitAll [] p as -> Prod [] g as-        go = \case-          SNil         -> \_ -> RNil-          x `SCons` xs -> \a -> f x (runWitAll a IZ)-                             :& go xs (WitAll (runWitAll a . IS))+  allProd ::+    forall p g.+    () =>+    (forall a. Sing a -> p @@ a -> g a) ->+    All [] p --> TyPred (Prod [] g)+  allProd f = go+    where+      go :: Sing as -> WitAll [] p as -> Prod [] g as+      go = \case+        SNil -> \_ -> RNil+        x `SCons` xs -> \a ->+          f x (runWitAll a IZ)+            :& go xs (WitAll (runWitAll a . IS)) -    prodAll-        :: forall p g as. ()-        => (forall a. g a -> p @@ a)-        -> Prod [] g as-        -> All [] p @@ as-    prodAll f = go-      where-        go :: Prod [] g bs -> All [] p @@ bs-        go = \case-          RNil    -> WitAll $ \case {}-          x :& xs -> WitAll $ \case-            IZ   -> f x-            IS i -> runWitAll (go xs) i+  prodAll ::+    forall p g as.+    () =>+    (forall a. g a -> p @@ a) ->+    Prod [] g as ->+    All [] p @@ as+  prodAll f = go+    where+      go :: Prod [] g bs -> All [] p @@ bs+      go = \case+        RNil -> WitAll $ \case {}+        x :& xs -> WitAll $ \case+          IZ -> f x+          IS i -> runWitAll (go xs) i  instance Universe Maybe where-    idecideAny f = \case-      SNothing -> Disproved $ \case WitAny i _ -> case i of {}-      SJust x  -> case f IJust x of-        Proved p    -> Proved $ WitAny IJust p-        Disproved v -> Disproved $ \case-          WitAny IJust p -> v p-    idecideAll f = \case-      SNothing -> Proved $ WitAll $ \case {}-      SJust x  -> case f IJust x of-        Proved p    -> Proved $ WitAll $ \case IJust -> p-        Disproved v -> Disproved $ \a -> v $ runWitAll a IJust-    allProd f = \case-      SNothing -> \_ -> PNothing-      SJust x  -> \a -> PJust (f x (runWitAll a IJust))-    prodAll f = \case-      PNothing -> WitAll $ \case {}-      PJust x  -> WitAll $ \case IJust -> f x+  idecideAny f = \case+    SNothing -> Disproved $ \case WitAny i _ -> case i of {}+    SJust x -> case f IJust x of+      Proved p -> Proved $ WitAny IJust p+      Disproved v -> Disproved $ \case+        WitAny IJust p -> v p+  idecideAll f = \case+    SNothing -> Proved $ WitAll $ \case {}+    SJust x -> case f IJust x of+      Proved p -> Proved $ WitAll $ \case IJust -> p+      Disproved v -> Disproved $ \a -> v $ runWitAll a IJust+  allProd f = \case+    SNothing -> \_ -> PNothing+    SJust x -> \a -> PJust (f x (runWitAll a IJust))+  prodAll f = \case+    PNothing -> WitAll $ \case {}+    PJust x -> WitAll $ \case IJust -> f x  instance Universe (Either j) where-    idecideAny f = \case-      SLeft  _ -> Disproved $ \case WitAny i _ -> case i of {}-      SRight x -> case f IRight x of-        Proved p    -> Proved $ WitAny IRight p-        Disproved v -> Disproved $ \case-          WitAny IRight p -> v p-    idecideAll f = \case-      SLeft  _ -> Proved $ WitAll $ \case {}-      SRight x -> case f IRight x of-        Proved p    -> Proved $ WitAll $ \case IRight -> p-        Disproved v -> Disproved $ \a -> v $ runWitAll a IRight-    allProd f = \case-      SLeft  w -> \_ -> PLeft w-      SRight x -> \a -> PRight (f x (runWitAll a IRight))-    prodAll f = \case-      PLeft _  -> WitAll $ \case {}-      PRight x -> WitAll $ \case IRight -> f x+  idecideAny f = \case+    SLeft _ -> Disproved $ \case WitAny i _ -> case i of {}+    SRight x -> case f IRight x of+      Proved p -> Proved $ WitAny IRight p+      Disproved v -> Disproved $ \case+        WitAny IRight p -> v p+  idecideAll f = \case+    SLeft _ -> Proved $ WitAll $ \case {}+    SRight x -> case f IRight x of+      Proved p -> Proved $ WitAll $ \case IRight -> p+      Disproved v -> Disproved $ \a -> v $ runWitAll a IRight+  allProd f = \case+    SLeft w -> \_ -> PLeft w+    SRight x -> \a -> PRight (f x (runWitAll a IRight))+  prodAll f = \case+    PLeft _ -> WitAll $ \case {}+    PRight x -> WitAll $ \case IRight -> f x  instance Universe NonEmpty where-    idecideAny-        :: forall k (p :: k ~> Type) (as :: NonEmpty k). ()-        => (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))-        -> Sing as-        -> Decision (Any NonEmpty p @@ as)-    idecideAny f (x NE.:%| xs) = case f NEHead x of-      Proved p    -> Proved $ WitAny NEHead p-      Disproved v -> case idecideAny @[] @_ @p (f . NETail) xs of-        Proved (WitAny i p) -> Proved $ WitAny (NETail i) p-        Disproved vs     -> Disproved $ \case-          WitAny i p -> case i of-            NEHead    -> v p-            NETail i' -> vs (WitAny i' p)+  idecideAny ::+    forall k (p :: k ~> Type) (as :: NonEmpty k).+    () =>+    (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) ->+    Sing as ->+    Decision (Any NonEmpty p @@ as)+  idecideAny f (x NE.:%| xs) = case f NEHead x of+    Proved p -> Proved $ WitAny NEHead p+    Disproved v -> case idecideAny @[] @_ @p (f . NETail) xs of+      Proved (WitAny i p) -> Proved $ WitAny (NETail i) p+      Disproved vs -> Disproved $ \case+        WitAny i p -> case i of+          NEHead -> v p+          NETail i' -> vs (WitAny i' p) -    idecideAll-        :: forall k (p :: k ~> Type) (as :: NonEmpty k). ()-        => (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))-        -> Sing as-        -> Decision (All NonEmpty p @@ as)-    idecideAll f (x NE.:%| xs) = case f NEHead x of-      Proved p -> case idecideAll @[] @_ @p (f . NETail) xs of-        Proved ps -> Proved $ WitAll $ \case-          NEHead   -> p-          NETail i -> runWitAll ps i-        Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . NETail)-      Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead+  idecideAll ::+    forall k (p :: k ~> Type) (as :: NonEmpty k).+    () =>+    (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) ->+    Sing as ->+    Decision (All NonEmpty p @@ as)+  idecideAll f (x NE.:%| xs) = case f NEHead x of+    Proved p -> case idecideAll @[] @_ @p (f . NETail) xs of+      Proved ps -> Proved $ WitAll $ \case+        NEHead -> p+        NETail i -> runWitAll ps i+      Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . NETail)+    Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead -    allProd-        :: forall p g. ()-        => (forall a. Sing a -> p @@ a -> g a)-        -> All NonEmpty p --> TyPred (Prod NonEmpty g)-    allProd f (x NE.:%| xs) a =-          f x (runWitAll a NEHead)+  allProd ::+    forall p g.+    () =>+    (forall a. Sing a -> p @@ a -> g a) ->+    All NonEmpty p --> TyPred (Prod NonEmpty g)+  allProd f (x NE.:%| xs) a =+    f x (runWitAll a NEHead)       :&| allProd @[] @p f xs (WitAll (runWitAll a . NETail))-    prodAll-        :: forall p g as. ()-        => (forall a. g a -> p @@ a)-        -> Prod NonEmpty g as-        -> All NonEmpty p @@ as-    prodAll f (x :&| xs) = WitAll $ \case-        NEHead   -> f x-        NETail i -> runWitAll (prodAll @[] @p f xs) i+  prodAll ::+    forall p g as.+    () =>+    (forall a. g a -> p @@ a) ->+    Prod NonEmpty g as ->+    All NonEmpty p @@ as+  prodAll f (x :&| xs) = WitAll $ \case+    NEHead -> f x+    NETail i -> runWitAll (prodAll @[] @p f xs) i  instance Universe ((,) j) where-    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 ISnd x of-      Proved p    -> Proved $ WitAll $ \case ISnd -> p-      Disproved v -> Disproved $ \a -> v $ runWitAll a ISnd-    allProd f (STuple2 w x) a = PTup w $ f x (runWitAll a ISnd)-    prodAll f (PTup _ x) = WitAll $ \case ISnd -> f x+  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 ISnd x of+    Proved p -> Proved $ WitAll $ \case ISnd -> p+    Disproved v -> Disproved $ \a -> v $ runWitAll a ISnd+  allProd f (STuple2 w x) a = PTup w $ f x (runWitAll a ISnd)+  prodAll f (PTup _ x) = WitAll $ \case ISnd -> f x  -- | The single-pointed universe. instance Universe Identity where-    idecideAny f (SIdentity x) =-        mapDecision (WitAny IId)-                    (\case WitAny IId p -> p)+  idecideAny f (SIdentity x) =+    mapDecision+      (WitAny IId)+      (\case WitAny IId p -> p)       $ f IId x-    idecideAll f (SIdentity x) =-        mapDecision (\p -> WitAll $ \case IId -> p)-                    (\y -> runWitAll y IId)+  idecideAll f (SIdentity x) =+    mapDecision+      (\p -> WitAll $ \case IId -> p)+      (\y -> runWitAll y IId)       $ f IId x-    allProd f (SIdentity x) a = PIdentity $ f x (runWitAll a IId)-    prodAll f (PIdentity x) = WitAll $ \case IId -> f x+  allProd f (SIdentity x) a = PIdentity $ f x (runWitAll a IId)+  prodAll f (PIdentity x) = WitAll $ \case IId -> f x

@@ -1,10 +1,11 @@ {-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE TypeFamilies        #-}-{-# LANGUAGE TypeInType          #-}-{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}  -- | -- Module      : Data.Type.Universe.Subset@@ -16,72 +17,88 @@ -- Portability : non-portable -- -- Represent a decidable subset of a type-level collection.--- module Data.Type.Universe.Subset (   -- * Subset-    Subset, WitSubset(..)-  , makeSubset+  Subset,+  WitSubset (..),+  makeSubset,+   -- ** Subset manipulation-  , intersection, union, symDiff, mergeSubset, imergeSubset-  , mapSubset, imapSubset+  intersection,+  union,+  symDiff,+  mergeSubset,+  imergeSubset,+  mapSubset,+  imapSubset,+   -- ** Subset extraction-  , subsetToList+  subsetToList,+   -- ** Subset tests-  , subsetToAny, subsetToAll, subsetToNone+  subsetToAny,+  subsetToAll,+  subsetToNone,+   -- ** Subset construction-  , emptySubset, fullSubset-  ) where+  emptySubset,+  fullSubset,+) where -import           Control.Applicative-import           Data.Kind-import           Data.Monoid                        (Alt(..))-import           Data.Singletons-import           Data.Singletons.Decide-import           Data.Type.Functor.Product-import           Data.Type.Predicate-import           Data.Type.Predicate.Logic-import           Data.Type.Predicate.Quantification-import           Data.Type.Universe+import Control.Applicative+import Data.Kind+import Data.Monoid (Alt (..))+import Data.Singletons+import Data.Singletons.Decide+import Data.Type.Functor.Product+import Data.Type.Predicate+import Data.Type.Predicate.Logic+import Data.Type.Predicate.Quantification+import Data.Type.Universe  -- | A @'WitSubset' f p @@ as@ describes a /decidable/ subset of type-level -- collection @as@. newtype WitSubset f p (as :: f k) = WitSubset-    { runWitSubset :: forall a. Elem f as a -> Decision (p @@ a)-    }+  { runWitSubset :: forall a. Elem f as a -> Decision (p @@ a)+  }  -- | A @'Subset' f p@ is a predicate that some decidable subset of an input -- @as@ is true. data Subset f :: (k ~> Type) -> (f k ~> Type)+ type instance Apply (Subset f p) as = WitSubset f p as  instance (Universe f, Decidable p) => Decidable (Subset f p) instance (Universe f, Decidable p) => Provable (Subset f p) where-    prove = makeSubset @f @_ @p (\_ -> decide @p)+  prove = makeSubset @f @_ @p (\_ -> decide @p)  -- | Create a 'Subset' from a predicate.-makeSubset-    :: forall f k p (as :: f k). Universe f-    => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))-    -> Sing as-    -> Subset f p @@ as+makeSubset ::+  forall f k p (as :: f k).+  Universe f =>+  (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->+  Sing as ->+  Subset f p @@ as makeSubset f xs = WitSubset $ \i -> f i (indexSing i xs)  -- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied -- predicates. -- -- List is meant to include no duplicates.-subsetToList-    :: forall f p t. (Universe f, Alternative t)-    => (Subset f p --># Any f p) t+subsetToList ::+  forall f p t.+  (Universe f, Alternative t) =>+  (Subset f p --># Any f p) t subsetToList xs s = getAlt $ (`ifoldMapSing` xs) $ \i _ -> Alt $ case runWitSubset s i of-    Proved p    -> pure $ WitAny i p-    Disproved _ -> empty+  Proved p -> pure $ WitAny i p+  Disproved _ -> empty  -- | Restrict a 'Subset' to a single (arbitrary) member, or fail if none -- exists.-subsetToAny-    :: forall f p. Universe f-    => Subset f p -?> Any f p+subsetToAny ::+  forall f p.+  Universe f =>+  Subset f p -?> Any f p subsetToAny xs s = idecideAny (\i _ -> runWitSubset s i) xs  -- | Construct an empty subset.@@ -97,67 +114,75 @@ subsetToNone xs s = idecideNone (\i _ -> runWitSubset s i) xs  -- | Combine two subsets based on a decision function-imergeSubset-    :: forall f k p q r (as :: f k). ()-    => (forall a. Elem f as a -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))-    -> Subset f p @@ as-    -> Subset f q @@ as-    -> Subset f r @@ as+imergeSubset ::+  forall f k p q r (as :: f k).+  () =>+  (forall a. Elem f as a -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) ->+  Subset f p @@ as ->+  Subset f q @@ as ->+  Subset f r @@ as imergeSubset f ps qs = WitSubset $ \i ->-    f i (runWitSubset ps i) (runWitSubset qs i)+  f i (runWitSubset ps i) (runWitSubset qs i)  -- | Combine two subsets based on a decision function-mergeSubset-    :: forall f k p q r (as :: f k). ()-    => (forall a. Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))-    -> Subset f p @@ as-    -> Subset f q @@ as-    -> Subset f r @@ as+mergeSubset ::+  forall f k p q r (as :: f k).+  () =>+  (forall a. Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) ->+  Subset f p @@ as ->+  Subset f q @@ as ->+  Subset f r @@ as mergeSubset f = imergeSubset (\(_ :: Elem f as a) p -> f @a p)  -- | Subset intersection-intersection-    :: forall f p q. ()-    => ((Subset f p &&& Subset f q) --> Subset f (p &&& q))+intersection ::+  forall f p q.+  () =>+  ((Subset f p &&& Subset f q) --> Subset f (p &&& q)) intersection _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideAnd @p @q @a  -- | Subset union (left-biased)-union-    :: forall f p q. ()-    => ((Subset f p &&& Subset f q) --> Subset f (p ||| q))+union ::+  forall f p q.+  () =>+  ((Subset f p &&& Subset f q) --> Subset f (p ||| q)) union _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideOr @p @q @a  -- | Symmetric subset difference-symDiff-    :: forall f p q. ()-    => ((Subset f p &&& Subset f q) --> Subset f (p ^^^ q))+symDiff ::+  forall f p q.+  () =>+  ((Subset f p &&& Subset f q) --> Subset f (p ^^^ q)) symDiff _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideXor @p @q @a  -- | Test if a subset is equal to the entire original collection-subsetToAll-    :: forall f p. Universe f-    => Subset f p -?> All f p+subsetToAll ::+  forall f p.+  Universe f =>+  Subset f p -?> All f p subsetToAll xs s = idecideAll (\i _ -> runWitSubset s i) xs  -- | 'mapSubset', but providing an 'Elem'.-imapSubset-    :: (forall a. Elem f as a -> p @@ a -> q @@ a)-    -> (forall a. Elem f as a -> q @@ a -> p @@ a)-    -> Subset f p @@ as-    -> Subset f q @@ as+imapSubset ::+  (forall a. Elem f as a -> p @@ a -> q @@ a) ->+  (forall a. Elem f as a -> q @@ a -> p @@ a) ->+  Subset f p @@ as ->+  Subset f q @@ as imapSubset f g s = WitSubset $ \i ->-    mapDecision (f i) (g i) (runWitSubset s i)+  mapDecision (f i) (g i) (runWitSubset s i)  -- | Map a bidirectional implication over a subset described by that -- implication. -- -- Implication needs to be bidirectional, or otherwise we can't produce -- a /decidable/ subset as a result.-mapSubset-    :: Universe f-    => (p --> q)-    -> (q --> p)-    -> (Subset f p --> Subset f q)-mapSubset f g xs = withSingI xs $-    imapSubset (\i -> f (indexSing i xs))-               (\i -> g (indexSing i xs))+mapSubset ::+  Universe f =>+  (p --> q) ->+  (q --> p) ->+  (Subset f p --> Subset f q)+mapSubset f g xs =+  withSingI xs $+    imapSubset+      (\i -> f (indexSing i xs))+      (\i -> g (indexSing i xs))