decidable (empty) → 0.1.0.0

raw patch · 11 files changed

+1571/−0 lines, 11 filesdep +basedep +singletonssetup-changed

Dependencies added: base, singletons

Files

CHANGELOG.md +12/−0
LICENSE +30/−0
README.md +11/−0
Setup.hs +2/−0
decidable.cabal +46/−0
src/Data/Type/Predicate.hs +314/−0
src/Data/Type/Predicate/Logic.hs +224/−0
src/Data/Type/Predicate/Param.hs +166/−0
src/Data/Type/Predicate/Quantification.hs +159/−0
src/Data/Type/Universe.hs +439/−0
src/Data/Type/Universe/Subset.hs +168/−0

+ CHANGELOG.md view

@@ -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.+

+ LICENSE view

@@ -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.

+ README.md view

@@ -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.+

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ decidable.cabal view

@@ -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

+ src/Data/Type/Predicate.hs view

@@ -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

+ src/Data/Type/Predicate/Logic.hs view

@@ -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

+ src/Data/Type/Predicate/Param.hs view

@@ -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)+

+ src/Data/Type/Predicate/Quantification.hs view

@@ -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)

+ src/Data/Type/Universe.hs view

@@ -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

+ src/Data/Type/Universe/Subset.hs view

@@ -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))