summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorjle <>2018-10-11 11:27:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-10-11 11:27:00 (GMT)
commita89472c300b45bfdc03e3a42d55ed26872de2490 (patch)
tree67e99cfc79db204ceb843f0578717d7eb78677ea
version 0.1.0.00.1.0.0
-rw-r--r--CHANGELOG.md12
-rw-r--r--LICENSE30
-rw-r--r--README.md11
-rw-r--r--Setup.hs2
-rw-r--r--decidable.cabal46
-rw-r--r--src/Data/Type/Predicate.hs314
-rw-r--r--src/Data/Type/Predicate/Logic.hs224
-rw-r--r--src/Data/Type/Predicate/Param.hs166
-rw-r--r--src/Data/Type/Predicate/Quantification.hs159
-rw-r--r--src/Data/Type/Universe.hs439
-rw-r--r--src/Data/Type/Universe/Subset.hs168
11 files changed, 1571 insertions, 0 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..0b2e699
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,12 @@
+Changelog
+=========
+
+Version 0.1.0.0
+---------------
+
+*October 10, 2018*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.1.0.0>
+
+* Initial release.
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..56568ee
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Justin Le (c) 2018
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ * Redistributions in binary form must reproduce the above
+ copyright notice, this list of conditions and the following
+ disclaimer in the documentation and/or other materials provided
+ with the distribution.
+
+ * Neither the name of Justin Le nor the names of other
+ contributors may be used to endorse or promote products derived
+ from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..ad6256d
--- /dev/null
+++ b/README.md
@@ -0,0 +1,11 @@
+# [decidable][]
+
+[![decidable on Hackage](https://img.shields.io/hackage/v/decidable.svg?maxAge=86400)](https://hackage.haskell.org/package/decidable)
+[![Build Status](https://travis-ci.org/mstksg/decidable.svg?branch=master)](https://travis-ci.org/mstksg/decidable)
+[decidable]: https://mstksg.github.io/decidable/
+
+This library provides combinators and typeclasses for working and manipulating
+type-level predicates in Haskell, which are represented as matchable type-level
+functions `k ~> Type` from the *singletons* library. See *Data.Type.Predicate*
+for a good starting point.
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/decidable.cabal b/decidable.cabal
new file mode 100644
index 0000000..99414b3
--- /dev/null
+++ b/decidable.cabal
@@ -0,0 +1,46 @@
+-- This file has been generated from package.yaml by hpack version 0.28.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: fa635fe6f55a295cab015d273dc723b843bac34ddd35415b9495c1c9306ba671
+
+name: decidable
+version: 0.1.0.0
+synopsis: Combinators for manipulating dependently-typed predicates.
+description: Please see the README on GitHub at <https://github.com/mstksg/decidable#readme>
+category: Dependent Types
+homepage: https://github.com/mstksg/decidable#readme
+bug-reports: https://github.com/mstksg/decidable/issues
+author: Justin Le
+maintainer: justin@jle.im
+copyright: (c) Justin Le 2018
+license: BSD3
+license-file: LICENSE
+tested-with: GHC >= 8.4 && < 8.8
+build-type: Simple
+cabal-version: >= 1.10
+extra-source-files:
+ CHANGELOG.md
+ README.md
+
+source-repository head
+ type: git
+ location: https://github.com/mstksg/decidable
+
+library
+ exposed-modules:
+ Data.Type.Predicate
+ Data.Type.Predicate.Logic
+ Data.Type.Predicate.Param
+ Data.Type.Predicate.Quantification
+ Data.Type.Universe
+ Data.Type.Universe.Subset
+ other-modules:
+ Paths_decidable
+ hs-source-dirs:
+ src
+ ghc-options: -Wall -Wredundant-constraints
+ build-depends:
+ base >=4.11 && <5
+ , singletons >=2.4
+ default-language: Haskell2010
diff --git a/src/Data/Type/Predicate.hs b/src/Data/Type/Predicate.hs
new file mode 100644
index 0000000..cb087c9
--- /dev/null
+++ b/src/Data/Type/Predicate.hs
@@ -0,0 +1,314 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- |
+-- Module : Data.Type.Predicate
+-- Copyright : (c) Justin Le 2018
+-- License : BSD3
+--
+-- Maintainer : justin@jle.im
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- 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
+ -- ** Manipulate predicates
+ , PMap, type Not, decideNot
+ -- * Provable Predicates
+ , Prove, type (-->), type (-->#)
+ , Provable(..)
+ , Disprovable, disprove
+ , TFunctor(..)
+ , compImpl
+ -- * Decidable Predicates
+ , Decide, type (-?>), type (-?>#)
+ , Decidable(..)
+ , DFunctor(..)
+ , mapDecision
+ ) where
+
+import Data.Kind
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Singletons.Prelude hiding (Not)
+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
+-- a value of type @P \@\@ x@, and that it false/disproved if such a value
+-- cannot exist. (Where '@@' is 'Apply', the singleton library's type-level
+-- function application for mathcable functions)
+--
+-- See 'Provable' and 'Decidable' for more information on how to use, prove
+-- and decide these predicates.
+--
+-- The kind @k ~> 'Type'@ is the kind of "matchable" type-level functions
+-- in Haskell. They are type-level functions that are encoded as dummy
+-- type constructors ("defunctionalization symbols") that can be decidedly
+-- "matched" on for things like typeclass instances.
+--
+-- There are two ways to define your own predicates:
+--
+-- 1. Using the predicate combinators and predicate transformers in
+-- this library and the /singletons/ library, which let you construct
+-- pre-made predicates and sometimes create predicates from other
+-- predicates.
+--
+-- 2. Manually creating a data type that acts as a matchable predicate.
+--
+-- For an example of the latter, we can create the "not p" predicate, which
+-- takes a predicate @p@ as input and returns the negation of the
+-- predicate:
+--
+-- @
+-- -- First, create the data type with the kind signature you want
+-- data Not :: Predicate k -> Predicate k
+--
+-- -- Then, write the 'Apply' instance, to specify the type of the
+-- -- witnesses of that predicate
+-- instance 'Apply' (Not p) a = (p '@@' a) -> Void
+-- @
+--
+-- See the source of "Data.Type.Predicate" and "Data.Type.Predicate.Logic"
+-- for simple examples of hand-made predicates. For example, we have the
+-- always-true predicate 'Evident':
+--
+-- @
+-- data Evident :: Predicate k
+-- instance Apply Evident a = Sing a
+-- @
+--
+-- And the "and" predicate combinator:
+--
+-- @
+-- data (&&&) :: Predicate k -> Predicate k -> Predicate k
+-- instance Apply (p &&& q) a = (p '@@' a, q '@@' a)
+-- @
+--
+-- Typically it is recommended to create predicates from the supplied
+-- predicate combinators ('TyPred' can be used for any type constructor to
+-- turn it into a predicate, for instance) whenever possible.
+type Predicate k = k ~> Type
+
+-- | Convert a normal '->' type constructor into a 'Predicate'.
+--
+-- @
+-- 'TyPred' :: (k -> 'Type') -> 'Predicate' k
+-- @
+type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)
+
+-- | The always-true predicate.
+--
+-- @
+-- 'Evident' :: 'Predicate' k
+-- @
+type Evident = (TyPred Sing :: Predicate k)
+
+-- | The always-false predicate
+--
+-- Could also be defined as @'ConstSym1' Void@, but this defintion gives
+-- us a free 'Decidable' instance.
+type Impossible = (Not Evident :: Predicate k)
+
+-- | @'EqualTo' a@ is a predicate that the input is equal to @a@.
+type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)
+
+-- | Convert a tradtional @k ~> 'Bool'@ predicate into a 'Predicate'.
+--
+-- @
+-- 'BoolPred' :: (k ~> Bool) -> Predicate k
+-- @
+type BoolPred (p :: k ~> Bool) = (EqualTo 'True .@#@$$$ p :: Predicate k)
+
+-- | Pre-compose a function to a predicate
+--
+-- @
+-- 'PMap' :: (k ~> j) -> 'Predicate' j -> Predicate k
+-- @
+type PMap (f :: k ~> j) (p :: Predicate j) = (p .@#@$$$ f :: Predicate k)
+
+-- | A @'Wit' p a@ is a value of type @p \@\@ a@ --- that is, it is a proof
+-- or witness that @p@ is satisfied for @a@.
+newtype Wit p a = Wit { getWit :: p @@ a }
+
+-- | A decision function for predicate @p@. See 'Decidable' for more
+-- information.
+type Decide p = forall a. Sing a -> Decision (p @@ a)
+
+-- | Like implication '-->', but knowing @p \@\@ a@ can only let us decidably
+-- prove @q @@ a@ is true or false.
+type p -?> q = forall a. Sing a -> p @@ a -> Decision (q @@ a)
+
+-- | Like '-?>', but only in a specific context @h@.
+type (p -?># q) h = forall a. Sing a -> p @@ a -> h (Decision (q @@ a))
+
+-- | A proving function for predicate @p@. See 'Provable' for more
+-- information.
+type Prove p = forall a. Sing a -> p @@ a
+
+-- | We say that @p@ implies @q@ (@p '-->' q@) if, given @p @@ a@, we can
+-- always prove @q \@\@ a@.
+type p --> q = forall a. Sing a -> p @@ a -> q @@ a
+
+-- | This is implication '-->#', but only in a specific context @h@.
+type (p --># q) h = forall a. Sing a -> p @@ a -> h (q @@ a)
+
+infixr 1 -?>
+infixr 1 -?>#
+infixr 1 -->
+infixr 1 -->#
+
+-- | A typeclass for decidable predicates.
+--
+-- A predicate is decidable if, given any input @a@, you can either prove
+-- or disprove @p \@\@ a@. A @'Decision' (p \@\@ a)@ is a data type
+-- that has a branch @p \@\@ a@ and @'Refuted' (p \@\@ a)@.
+--
+-- This typeclass associates a canonical decision function for every
+-- decidable predicate.
+--
+-- It confers two main advatnages:
+--
+-- 1. The decision function for every predicate is available via the
+-- same name
+--
+-- 2. We can write 'Decidable' instances for polymorphic predicate
+-- 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
+ -- @
+ decide :: Decide p
+
+ default decide :: Provable p => Decide p
+ decide = Proved . prove @p
+
+-- | A typeclass for provable predicates (constructivist tautologies).
+--
+-- A predicate is provable if, given any input @a@, you can generate
+-- a proof of @p \@\@ a@. Essentially, it means that a predicate is "always
+-- true".
+--
+-- This typeclass associates a canonical proof function for every provable
+-- predicate.
+--
+-- It confers two main advatnages:
+--
+-- 1. The proof function for every predicate is available via the same
+-- name
+--
+-- 2. We can write 'Provable' instances for polymorphic predicate
+-- transformers (predicates parameterized on other predicates) easily,
+-- by refering to 'Provable' instances of the transformed predicates.
+class Provable p where
+ -- | The canonical proving function for predicate @p@.
+ --
+ -- 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
+ -- @
+ prove :: Prove p
+
+-- | @'Disprovable' p@ is a constraint that @p@ can be disproven.
+type Disprovable p = Provable (Not p)
+
+-- | The deciding/disproving function for @'Disprovable' p@.
+--
+-- Must be called by applying the 'Predicate' to disprove:
+--
+-- @
+-- 'disprove' \@p
+-- @
+disprove :: forall p. Disprovable p => Prove (Not p)
+disprove = prove @(Not p)
+
+-- | 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)
+
+-- | 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)
+
+instance (SDecide k, SingI (a :: k)) => Decidable (EqualTo a) where
+ decide = (sing %~)
+
+instance Decidable Evident
+instance Provable Evident where
+ prove = id
+
+instance (Decidable f, SingI g) => Decidable (f .@#@$$$ g) where
+ decide = decide @f . ((sing :: Sing g) @@)
+
+instance (Provable f, SingI g) => Provable (f .@#@$$$ g) where
+ prove = prove @f . ((sing :: Sing g) @@)
+
+-- | Compose two implications.
+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)
+
+instance Provable (Not Impossible) where
+ 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 = \case
+ 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 f g = \case
+ Proved p -> Proved $ f p
+ Disproved v -> Disproved $ v . g
diff --git a/src/Data/Type/Predicate/Logic.hs b/src/Data/Type/Predicate/Logic.hs
new file mode 100644
index 0000000..fa8f205
--- /dev/null
+++ b/src/Data/Type/Predicate/Logic.hs
@@ -0,0 +1,224 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- |
+-- Module : Data.Type.Predicate.Logic
+-- Copyright : (c) Justin Le 2018
+-- License : BSD3
+--
+-- Maintainer : justin@jle.im
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- Logical and algebraic connectives for predicates, as well as common
+-- logical combinators.
+module Data.Type.Predicate.Logic (
+ -- * Top and bottom
+ Evident, Impossible
+ -- * Logical connectives
+ , type Not, decideNot
+ , type (&&&), decideAnd
+ , type (|||), decideOr, type (^||), type (||^)
+ , type (^^^), decideXor
+ , type (==>), proveImplies, Implies
+ , type (<==>), Equiv
+ -- * Logical deductions
+ , compImpl, explosion, atom, excludedMiddle, doubleNegation
+ , contrapositive, contrapositive'
+ -- ** Lattice
+ , projAndFst, projAndSnd, injOrLeft, injOrRight
+ ) where
+
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Singletons.Prelude.Bool (Sing(..))
+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)
+
+instance (Provable p, Provable q) => Provable (p &&& q) where
+ 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 = \case
+ Proved p -> \case
+ Proved q -> Proved (p, q)
+ Disproved v -> Disproved $ \(_, q) -> v q
+ 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 |||
+
+instance (Decidable p, Decidable q) => Decidable (p ||| q) where
+ decide (x :: Sing a) = decideOr @p @q @a (decide @p x) (decide @q x)
+
+-- | Picks the proof of @p@. Note that this is instance has stronger
+-- constraints than is strictly necessary; we should really only have to
+-- require that either @p@ or @q@ is true.
+instance Provable p => Provable (p ||| q) where
+ prove x = Left (prove @p x)
+
+-- | Decide @p '|||' q@ based on decisions of @p@ and @q@.
+decideOr
+ :: forall p q a. ()
+ => Decision (p @@ a)
+ -> Decision (q @@ a)
+ -> Decision ((p ||| q) @@ a)
+decideOr = \case
+ Proved p -> \_ -> Proved $ Left p
+ Disproved v -> \case
+ Proved q -> Proved $ Right q
+ Disproved w -> Disproved $ \case
+ Left p -> v p
+ Right q -> w q
+
+-- | Left-biased "or". In proofs, prioritize a proof of the left side over
+-- a proof of the right side.
+type p ^|| q = p ||| Not p &&& q
+
+-- | Right-biased "or". In proofs, prioritize a proof of the right side over
+-- a proof of the left side.
+type p ||^ q = p &&& Not q ||| q
+
+-- | @p '^^^' q@ is a predicate that either @p@ and @q@ are true, but not
+-- both.
+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)
+
+-- | @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 Provable (Impossible ==> p) where
+ 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)
+instance Provable (p ==> q) => Provable (Not q ==> Not p) where
+ prove = contrapositive @p @q (prove @(p ==> q))
+
+-- | @'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)
+
+-- | @'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)
+
+-- | If @q@ is provable, then so is @p '==>' q@.
+--
+-- This can be used as an easy plug-in 'Provable' instance for @p '==>' q@
+-- if @q@ is 'Provable':
+--
+-- @
+-- instance Provable (p ==> MyPred) where
+-- prove = proveImplies @MyPred
+-- @
+--
+-- This instance isn't provided polymorphically because of overlapping
+-- instance issues.
+proveImplies :: Prove q -> Prove (p ==> q)
+proveImplies q x _ = q x
+
+-- | Two-way implication, or logical equivalence
+type (p <==> q) = p ==> q &&& q ==> p
+infixr 1 <==>
+
+-- | From @'Impossible' @@ a@, you can prove anything. Essentially
+-- a lifted version of 'absurd'.
+explosion :: Impossible --> p
+explosion x v = absurd $ v x
+
+-- | 'Evident' can be proven from all predicates.
+atom :: p --> Evident
+atom = const
+
+-- | We cannot have both @p@ and @'Not' p@.
+excludedMiddle :: (p &&& Not p) --> Impossible
+excludedMiddle _ (p, notP) _ = notP p
+
+-- | If only this worked, but darn overlapping instances. Same for p ==>
+-- p ||| q and p &&& q ==> p :(
+-- q) ==>
+-- instance Provable (p &&& Not p ==> Impossible) where
+-- prove = excludedMiddle @p
+
+-- | If p implies q, then not q implies not p.
+contrapositive
+ :: (p --> q)
+ -> (Not q --> Not p)
+contrapositive f x v p = v (f x p)
+
+-- | 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' f x p = case decide @q x of
+ Proved q -> q
+ Disproved vq -> absurd $ f x vq p
+
+-- | Logical double negation. Only possible if @p@ is 'Decidable'.
+doubleNegation :: forall p. Decidable p => Not (Not p) --> p
+doubleNegation x vvp = case decide @p x of
+ Proved p -> p
+ Disproved vp -> absurd $ vvp vp
+
+-- | If @p '&&&' q@ is true, then so is @p@.
+projAndFst :: (p &&& q) --> p
+projAndFst _ = fst
+
+-- | If @p '&&&' q@ is true, then so is @q@.
+projAndSnd :: (p &&& q) --> q
+projAndSnd _ = snd
+
+-- | If @p@ is true, then so is @p '|||' q@.
+injOrLeft :: forall p q. p --> (p ||| q)
+injOrLeft _ = Left
+
+-- | If @q@ is true, then so is @p '|||' q@.
+injOrRight :: forall p q. q --> (p ||| q)
+injOrRight _ = Right
diff --git a/src/Data/Type/Predicate/Param.hs b/src/Data/Type/Predicate/Param.hs
new file mode 100644
index 0000000..3d29016
--- /dev/null
+++ b/src/Data/Type/Predicate/Param.hs
@@ -0,0 +1,166 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- |
+-- Module : Data.Type.Universe.Param
+-- Copyright : (c) Justin Le 2018
+-- License : BSD3
+--
+-- Maintainer : justin@jle.im
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- Manipulate "parameterized predicates". See 'ParamPred' and 'Found' for
+-- more information.
+--
+module Data.Type.Predicate.Param (
+ -- * Parameterized Predicates
+ ParamPred
+ , FlipPP, ConstPP, PPMap, InP, AnyMatch
+ -- * Deciding and Proving
+ , Found
+ , Selectable, select
+ , Searchable, search
+ ) where
+
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Singletons.Sigma
+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
+
+-- | Convert a parameterized predicate into a predicate on the parameter.
+--
+-- A @'Found' p@ is a predicate on @p :: 'ParamPred' k v@ that tests a @k@
+-- for the fact that there exists a @v@ where @'ParamPred' k v@ is satisfied.
+--
+-- Intended as the basic interface for 'ParamPred', since it turns
+-- a 'ParamPred' into a normal 'Predicate', which can have 'Decidable' and
+-- 'Provable' instances.
+--
+-- For some context, an instance of @'Provable' ('Found' P)@, where @P ::
+-- 'ParamPred' k v@, means that for any input @x :: k@, we can always find
+-- a @y :: v@ such that we have @P x @@ y@.
+--
+-- In the language of quantifiers, it means that forall @x :: k@, there
+-- exists a @y :: v@ such that @P x @@ y@.
+--
+-- For an instance of @'Decidable' ('Found' P)@, it means that for all @x
+-- :: k@, we can prove or disprove the fact that there exists a @y :: v@
+-- such that @P x @@ y@.
+data Found :: ParamPred k v -> Predicate k
+type instance Apply (Found (p :: ParamPred k v)) a = Σ v (p a)
+
+-- | 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
+
+-- | 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
+
+instance (Decidable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Decidable (Found (PPMap f p)) where
+ decide (x :: Sing a) = case decide @(Found p) ((sing :: Sing f) @@ x) of
+ Proved (i :&: p) -> Proved $ i :&: p
+ Disproved v -> Disproved $ \case i :&: p -> v (i :&: p)
+
+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
+
+-- | 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
+-- :: v@ that satisfies @P x \@\@ y@. We can "search" for that @y@, and
+-- prove that it can or cannot be found.
+type Searchable p = Decidable (Found p)
+
+-- | 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)
+
+-- | The deciding/searching function for @'Searchable' p@.
+--
+-- Must be called by applying the 'ParamPred':
+--
+-- @
+-- 'search' \@p
+-- @
+search
+ :: forall p. Searchable p
+ => Decide (Found p)
+search = decide @(Found p)
+
+-- | The proving/selecting function for @'Selectable' p@.
+--
+-- Must be called by applying the 'ParamPred':
+--
+-- @
+-- 'select' \@p
+-- @
+select
+ :: forall p. Selectable p
+ => Prove (Found p)
+select = prove @(Found p)
+
+-- | A @'ParamPred' (f k) k@. Parameterized on an @as :: f k@, returns
+-- a predicate that is true if there exists any @a :: k@ in @as@.
+--
+-- Essentially 'NotNull'.
+type InP f = (ElemSym1 f :: ParamPred (f k) k)
+
+instance Universe f => Decidable (Found (InP f)) where
+ decide xs = case decide @(NotNull f) xs of
+ Proved (WitAny i s) -> Proved $ s :&: i
+ Disproved v -> Disproved $ \case
+ s :&: i -> v $ WitAny i s
+
+instance Decidable (NotNull f ==> Found (InP f))
+instance Provable (NotNull f ==> Found (InP f)) where
+ prove _ (WitAny i s) = s :&: i
+
+instance Decidable (Found (InP f) ==> NotNull f)
+instance Provable (Found (InP f) ==> NotNull f) where
+ prove _ (s :&: i) = WitAny i s
+
+-- | @'AnyMatch' f@ takes a parmaeterized predicate on @k@ (testing for
+-- a @v@) and turns it into a parameterized predicate on @f k@ (testing for
+-- a @v@). It "lifts" the domain into @f@.
+--
+-- An @'AnyMatch' f p as@ is a predicate taking an argument @a@ and
+-- testing if @p a :: 'Predicate' k@ is satisfied for any item in @as ::
+-- f k@.
+--
+-- 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 xs = case decide @(Any f (Found p)) xs of
+ Proved (WitAny i (x :&: p)) -> Proved $ x :&: WitAny i p
+ Disproved v -> Disproved $ \case
+ x :&: WitAny i p -> v $ WitAny i (x :&: p)
+
diff --git a/src/Data/Type/Predicate/Quantification.hs b/src/Data/Type/Predicate/Quantification.hs
new file mode 100644
index 0000000..a221448
--- /dev/null
+++ b/src/Data/Type/Predicate/Quantification.hs
@@ -0,0 +1,159 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- |
+-- Module : Data.Type.Predicate.Quantification
+-- Copyright : (c) Justin Le 2018
+-- License : BSD3
+--
+-- Maintainer : justin@jle.im
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- Higher-level predicates for quantifying predicates over universes and
+-- sets.
+--
+module Data.Type.Predicate.Quantification (
+ -- * Any
+ Any, WitAny(..), None
+ -- ** Decision
+ , decideAny, idecideAny, decideNone, idecideNone
+ -- ** Entailment
+ , entailAny, ientailAny, entailAnyF, ientailAnyF
+ -- * All
+ , All, WitAll(..)
+ -- ** Decision
+ , decideAll, idecideAll
+ -- ** Entailment
+ , entailAll, ientailAll, entailAllF, ientailAllF
+ , decideEntailAll, idecideEntailAll
+ ) where
+
+import Data.Kind
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Type.Predicate
+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 f xs = decideNot @(Any f p) $ idecideAny f xs
+
+-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
+-- a collection @as@ that is true if and only if /no/ item in @as@
+-- satisfies the original predicate.
+--
+-- 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 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 f (WitAny i x) = WitAny i (f i (index 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 = 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 f a = WitAll $ \i -> f i (index 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 = 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 f = \case WitAny i x -> WitAny i <$> f i x
+
+-- | If @p@ implies @q@ under some context @h@, and if there exists some
+-- @a@ such that @p a@, then there must exist some @a@ such that @p q@
+-- under that context @h@.
+--
+-- @h@ might be something like, say, 'Maybe', to give predicate that is
+-- either provably true or unprovably false.
+--
+-- Note that it is not possible to do this with @p a -> 'Decision' (q a)@.
+-- 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 $
+ ientailAnyF @f @p @q (\i -> f (index 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 = igenAllA (\i _ -> f i (runWitAll a i)) sing
+
+-- | 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 $
+ ientailAllF @f @p @q (\i -> f (index 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 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 = dmap @(All f)
diff --git a/src/Data/Type/Universe.hs b/src/Data/Type/Universe.hs
new file mode 100644
index 0000000..5d361be
--- /dev/null
+++ b/src/Data/Type/Universe.hs
@@ -0,0 +1,439 @@
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- |
+-- Module : Data.Type.Universe
+-- Copyright : (c) Justin Le 2018
+-- License : BSD3
+--
+-- Maintainer : justin@jle.im
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- Combinators for working with type-level predicates, along with
+-- typeclasses for canonical proofs and deciding functions.
+--
+module Data.Type.Universe (
+ -- * Universe
+ Elem, In, Universe(..)
+ -- ** Instances
+ , Index(..), IsJust(..), IsRight(..), NEIndex(..), Snd(..)
+ -- ** Predicates
+ , All, WitAll(..)
+ , Any, WitAny(..), None
+ , Null, NotNull
+ -- * Decisions and manipulations
+ , decideAny, decideAll, genAllA, genAll, igenAll
+ , foldMapUni, ifoldMapUni, index, pickElem
+ -- * Defunctionalization symbols
+ , ElemSym0, ElemSym1, ElemSym2
+ ) where
+
+import Data.Type.Predicate.Logic
+import Control.Applicative
+import Data.Functor.Identity
+import Data.Kind
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Singletons.Prelude hiding (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Snd, Null, Not)
+import Data.Type.Predicate
+import Prelude hiding (any, all)
+import qualified Data.Singletons.Prelude.List.NonEmpty as NE
+
+-- | A witness for membership of a given item in a type-level collection
+type family Elem (f :: Type -> Type) :: f k -> k -> Type
+
+data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type
+data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
+type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a
+
+type instance Apply (ElemSym0 f) as = ElemSym1 f as
+type instance Apply (ElemSym1 f as) a = Elem f as a
+
+-- | @'In' f as@ is a predicate that a given input @a@ is a member of
+-- collection @as@.
+type In (f :: Type -> Type) (as :: f k) = TyCon1 (Elem f as)
+
+-- | 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
+
+-- | 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
+-- "exists" quantifier over a given universe.
+--
+-- 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 :: (k ~> Type) -> (f k ~> Type)
+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 }
+
+-- | 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"
+-- quantifier over a given universe.
+--
+-- This is mostly useful for its 'Decidable', 'Provable', and 'TFunctor'
+-- instances, which lets you lift predicates on @p@ to predicates on @'All'
+-- f p@.
+data All f :: (k ~> Type) -> (f k ~> Type)
+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
+
+instance (Universe f, Decidable p) => Decidable (All f p) where
+ decide = decideAll @f @_ @p $ decide @p
+
+instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p) where
+
+instance Provable p => Provable (NotNull f ==> Any f p) where
+ 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 (index i xs)
+
+instance Universe f => TFunctor (Any f) where
+ tmap f xs (WitAny i x) = WitAny i (f (index i xs) x)
+
+instance Universe f => TFunctor (All f) where
+ tmap f xs a = WitAll $ \i -> f (index 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
+
+-- | Typeclass for a type-level container that you can quantify or lift
+-- type-level predicates over.
+class 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
+
+ -- | '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
+
+ -- | 'genAllA', but providing an 'Elem'.
+ igenAllA
+ :: forall k (p :: k ~> Type) (as :: f k) h. Applicative h
+ => (forall a. Elem f as a -> Sing a -> h (p @@ a)) -- ^ predicate on value in context
+ -> (Sing as -> h (All f p @@ as)) -- ^ predicate on collection in context
+
+-- | Predicate that a given @as :: f k@ is empty and has no items in it.
+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.
+type NotNull f = (Any f Evident :: Predicate (f k))
+
+-- | A @'None' f p@ is a predicate on a collection @as@ that no @a@ in @as@
+-- satisfies predicate @p@.
+type None f p = (Not (Any f p) :: Predicate (f k))
+
+-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
+-- a collection @as@ that is true if and only if /any/ item in @as@
+-- satisfies the original predicate.
+--
+-- That is, it turns a predicate of kind @k ~> Type@ into a predicate
+-- 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 f = idecideAny (const f)
+
+-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
+-- a collection @as@ that is true if and only if /all/ items in @as@
+-- satisfies the original predicate.
+--
+-- That is, it turns a predicate of kind @k ~> Type@ into a predicate
+-- 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 f = idecideAll (const f)
+
+-- | If @p a@ is true for all values @a@ in @as@ under some
+-- (Applicative) context @h@, then you can create an @'All' p as@ under
+-- that Applicative context @h@.
+--
+-- Can be useful with 'Identity' (which is basically unwrapping and
+-- wrapping 'All'), or with 'Maybe' (which can express predicates that
+-- are either provably true or not provably false).
+--
+-- In practice, this can be used to iterate and traverse and sequence
+-- actions over all "items" in @as@.
+genAllA
+ :: forall k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h)
+ => (forall a. Sing a -> h (p @@ a)) -- ^ predicate on value in context
+ -> (Sing as -> h (All f p @@ as)) -- ^ predicate on collection in context
+genAllA f = igenAllA (const f)
+
+-- | '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 f = runIdentity . igenAllA (\i -> Identity . f i)
+
+-- | 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 f = igenAll (const f)
+
+-- | Extract the item from the container witnessed by the 'Elem'
+index
+ :: forall f as a. Universe f
+ => Elem f as a -- ^ Witness
+ -> Sing as -- ^ Collection
+ -> Sing a
+index i = (`runWitAll` i) . splitSing
+
+-- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.
+splitSing
+ :: forall f (as :: f k). Universe f
+ => Sing as
+ -> All f (TyPred Sing) @@ as
+splitSing = igenAll @f @_ @(TyPred Sing) (\_ x -> x)
+
+-- | 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 = case decide @(Any f (TyPred ((:~:) a))) sing of
+ Proved (WitAny i Refl) -> Proved i
+ Disproved v -> Disproved $ \i -> v $ WitAny i Refl
+
+-- | 'foldMapUni' but with access to the index.
+ifoldMapUni
+ :: forall f k (as :: f k) m. (Universe f, Monoid m)
+ => (forall a. Elem f as a -> Sing a -> m)
+ -> Sing as
+ -> m
+ifoldMapUni f = getConst . igenAllA (\i -> Const . f i)
+
+-- | A 'foldMap' over all items in a collection.
+foldMapUni
+ :: forall f k (as :: f k) m. (Universe f, Monoid m)
+ => (forall (a :: k). Sing a -> m)
+ -> Sing as
+ -> m
+foldMapUni f = ifoldMapUni (const f)
+
+-- | Witness an item in a type-level list by providing its index.
+data Index :: [k] -> k -> Type where
+ IZ :: Index (a ': as) a
+ IS :: Index bs a -> Index (b ': bs) a
+
+deriving instance Show (Index as a)
+instance (SingI (as :: [k]), SDecide k) => Decidable (TyPred (Index as)) where
+ decide x = withSingI x $ pickElem
+
+type instance Elem [] = Index
+
+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)
+
+ 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
+
+ igenAllA
+ :: forall (p :: k ~> Type) (as :: [k]) h. Applicative h
+ => (forall a. Elem [] as a -> Sing a -> h (p @@ a))
+ -> Sing as
+ -> h (All [] p @@ as)
+ igenAllA f = \case
+ SNil -> pure $ WitAll $ \case {}
+ x `SCons` xs -> go <$> f IZ x <*> igenAllA (f . IS) xs
+ where
+ go :: p @@ b -> All [] p @@ bs -> All [] p @@ (b ': bs)
+ go p a = WitAll $ \case
+ IZ -> p
+ IS i -> runWitAll a i
+
+-- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is
+-- 'Just'.
+data IsJust :: Maybe k -> k -> Type where
+ IsJust :: IsJust ('Just a) a
+
+deriving instance Show (IsJust as a)
+instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IsJust as)) where
+ decide x = withSingI x $ pickElem
+
+type instance Elem Maybe = IsJust
+
+instance Universe Maybe where
+ idecideAny f = \case
+ SNothing -> Disproved $ \case WitAny i _ -> case i of {}
+ SJust x -> case f IsJust x of
+ Proved p -> Proved $ WitAny IsJust p
+ Disproved v -> Disproved $ \case
+ WitAny IsJust p -> v p
+
+ idecideAll f = \case
+ SNothing -> Proved $ WitAll $ \case {}
+ SJust x -> case f IsJust x of
+ Proved p -> Proved $ WitAll $ \case IsJust -> p
+ Disproved v -> Disproved $ \a -> v $ runWitAll a IsJust
+
+ igenAllA f = \case
+ SNothing -> pure $ WitAll $ \case {}
+ SJust x -> (\p -> WitAll $ \case IsJust -> p) <$> f IsJust x
+
+-- | Witness an item in a type-level @'Either' j@ by proving the 'Either'
+-- is 'Right'.
+data IsRight :: Either j k -> k -> Type where
+ IsRight :: IsRight ('Right a) a
+
+deriving instance Show (IsRight as a)
+instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IsRight as)) where
+ decide x = withSingI x $ pickElem
+
+type instance Elem (Either j) = IsRight
+
+instance Universe (Either j) where
+ idecideAny f = \case
+ SLeft _ -> Disproved $ \case WitAny i _ -> case i of {}
+ SRight x -> case f IsRight x of
+ Proved p -> Proved $ WitAny IsRight p
+ Disproved v -> Disproved $ \case
+ WitAny IsRight p -> v p
+
+ idecideAll f = \case
+ SLeft _ -> Proved $ WitAll $ \case {}
+ SRight x -> case f IsRight x of
+ Proved p -> Proved $ WitAll $ \case IsRight -> p
+ Disproved v -> Disproved $ \a -> v $ runWitAll a IsRight
+
+ igenAllA f = \case
+ SLeft _ -> pure $ WitAll $ \case {}
+ SRight x -> (\p -> WitAll $ \case IsRight -> p) <$> f IsRight x
+
+-- | Witness an item in a type-level 'NonEmpty' by either indicating that
+-- it is the "head", or by providing an index in the "tail".
+data NEIndex :: NonEmpty k -> k -> Type where
+ NEHead :: NEIndex (a ':| as) a
+ NETail :: Index as a -> NEIndex (b ':| as) a
+
+deriving instance Show (NEIndex as a)
+instance (SingI (as :: NonEmpty k), SDecide k) => Decidable (TyPred (NEIndex as)) where
+ decide x = withSingI x $ pickElem
+
+type instance Elem NonEmpty = NEIndex
+
+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)
+
+ 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
+
+ igenAllA
+ :: forall (p :: k ~> Type) (as :: NonEmpty k) h. Applicative h
+ => (forall a. Elem NonEmpty as a -> Sing a -> h (p @@ a))
+ -> Sing as
+ -> h (All NonEmpty p @@ as)
+ igenAllA f (x NE.:%| xs) = go <$> f NEHead x <*> igenAllA @[] @_ @p (f . NETail) xs
+ where
+ go :: p @@ b -> All [] p @@ bs -> All NonEmpty p @@ (b ':| bs)
+ go p ps = WitAll $ \case
+ NEHead -> p
+ NETail i -> runWitAll ps i
+
+-- | Trivially witness an item in the second field of a type-level tuple.
+data Snd :: (j, k) -> k -> Type where
+ Snd :: Snd '(a, b) b
+
+deriving instance Show (Snd as a)
+instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (Snd as)) where
+ decide x = withSingI x $ pickElem
+
+type instance Elem ((,) j) = Snd
+
+instance Universe ((,) j) where
+ idecideAny f (STuple2 _ x) = case f Snd x of
+ Proved p -> Proved $ WitAny Snd p
+ Disproved v -> Disproved $ \case WitAny Snd p -> v p
+
+ idecideAll f (STuple2 _ x) = case f Snd x of
+ Proved p -> Proved $ WitAll $ \case Snd -> p
+ Disproved v -> Disproved $ \a -> v $ runWitAll a Snd
+
+ igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case Snd -> p) <$> f Snd x
diff --git a/src/Data/Type/Universe/Subset.hs b/src/Data/Type/Universe/Subset.hs
new file mode 100644
index 0000000..fd19d9f
--- /dev/null
+++ b/src/Data/Type/Universe/Subset.hs
@@ -0,0 +1,168 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- |
+-- Module : Data.Type.Universe.Subset
+-- Copyright : (c) Justin Le 2018
+-- License : BSD3
+--
+-- Maintainer : justin@jle.im
+-- Stability : experimental
+-- Portability : non-portable
+--
+-- Represent a decidable subset of a type-level collection.
+--
+module Data.Type.Universe.Subset (
+ -- * Subset
+ Subset, WitSubset(..)
+ , makeSubset
+ -- ** Subset manipulation
+ , intersection, union, symDiff, mergeSubset, imergeSubset
+ , mapSubset, imapSubset
+ -- ** Subset extraction
+ , subsetToList
+ -- ** Subset tests
+ , subsetToAny, subsetToAll, subsetToNone
+ -- ** Subset construction
+ , emptySubset, fullSubset
+ ) where
+
+import Control.Applicative
+import Data.Kind
+import Data.Monoid (Alt(..))
+import Data.Singletons
+import Data.Singletons.Decide
+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)
+ }
+
+-- | 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)
+
+-- | 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 f xs = WitSubset $ \i -> f i (index i xs)
+
+-- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied
+-- predicates.
+subsetToList
+ :: forall f p t. (Universe f, Alternative t)
+ => (Subset f p --># Any f p) t
+subsetToList xs s = getAlt $ (`ifoldMapUni` xs) $ \i _ -> Alt $ case runWitSubset s i of
+ 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 xs s = idecideAny (\i _ -> runWitSubset s i) xs
+
+-- | Construct an empty subset.
+emptySubset :: forall f as. (Universe f, SingI as) => Subset f Impossible @@ as
+emptySubset = prove @(Subset f Impossible) sing
+
+-- | Construct a full subset
+fullSubset :: forall f as. (Universe f, SingI as) => Subset f Evident @@ as
+fullSubset = prove @(Subset f Evident) sing
+
+-- | Test if a subset is empty.
+subsetToNone :: forall f p. Universe f => Subset f p -?> None f p
+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 f ps qs = WitSubset $ \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 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 _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideAnd @p @q @a
+
+-- | Subset union
+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 _ = 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 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 f g s = WitSubset $ \i ->
+ mapDecision (f i) (g i) (runWitSubset s i)
+
+-- | Map a bidirectional implication over a subset described by that
+-- implication.
+--
+-- Implication needs to be bidirection, 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@Sing = withSingI xs $
+ imapSubset (\i -> f (index i xs))
+ (\i -> g (index i xs))