decidable 0.1.0.0 → 0.1.1.0

raw patch · 9 files changed

+319/−37 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +16/−0
• README.md +3/−2
• decidable.cabal +4/−3
• src/Data/Type/Predicate.hs +98/−3
• src/Data/Type/Predicate/Auto.hs +139/−0
• src/Data/Type/Predicate/Logic.hs +36/−6
• src/Data/Type/Predicate/Param.hs +10/−13
• src/Data/Type/Universe.hs +9/−8
• src/Data/Type/Universe/Subset.hs +4/−2

@@ -1,6 +1,22 @@ Changelog ========= +Version 0.1.1.0+---------------++*October 12, 2018*++<https://github.com/mstksg/decidable/releases/tag/v0.1.1.0>++*   `flipDecision`, `forgetDisproof`, `forgetProof`, `isProved`, and+    `isDisproved` added to *Data.Type.Predicate* module.+*   `ProvableTC`, `DeccidableTC`, `proveTC`, and `decideTC` helper functions+    and constraints+*   *Data.Type.Predicate.Auto* module, for generating witnesses at+    compile-time.+*   Instances for injection and projection out of `&&&` and `|||`, with some+    tricks to prevent overlapping instance issues.+ Version 0.1.0.0 --------------- 

@@ -1,11 +1,12 @@-# [decidable][]+[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. +[decidable]: http://hackage.haskell.org/package/decidable

@@ -2,10 +2,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: fa635fe6f55a295cab015d273dc723b843bac34ddd35415b9495c1c9306ba671+-- hash: 24f4181ba9122110e3a7d932fd7820c169b392a5cdbc76825cd8f60f5410f0e3  name:           decidable-version:        0.1.0.0+version:        0.1.1.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@@ -30,6 +30,7 @@ library   exposed-modules:       Data.Type.Predicate+      Data.Type.Predicate.Auto       Data.Type.Predicate.Logic       Data.Type.Predicate.Param       Data.Type.Predicate.Quantification@@ -39,7 +40,7 @@       Paths_decidable   hs-source-dirs:       src-  ghc-options: -Wall -Wredundant-constraints+  ghc-options: -Wall -Wredundant-constraints -Wcompat   build-depends:       base >=4.11 && <5     , singletons >=2.4

@@ -39,16 +39,22 @@   , Prove, type (-->), type (-->#)   , Provable(..)   , Disprovable, disprove+  , ProvableTC, proveTC   , TFunctor(..)   , compImpl     -- * Decidable Predicates   , Decide, type (-?>), type (-?>#)   , Decidable(..)+  , DecidableTC, decideTC   , DFunctor(..)-  , mapDecision+  -- * Manipulate Decisions+  , Decision(..)+  , flipDecision, mapDecision+  , forgetDisproof, forgetProof, isProved, isDisproved   ) where  import           Data.Kind+import           Data.Maybe import           Data.Singletons import           Data.Singletons.Decide import           Data.Singletons.Prelude hiding (Not)@@ -150,6 +156,9 @@  -- | 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@.+--+-- It essentially turns a @k ~> 'Type'@ ("matchable" @'Predicate' k@) /back+-- into/ a @k -> 'Type'@ predicate. newtype Wit p a = Wit { getWit :: p @@ a }  -- | A decision function for predicate @p@.  See 'Decidable' for more@@ -253,6 +262,47 @@ disprove :: forall p. Disprovable p => Prove (Not p) disprove = prove @(Not p) +-- | If @T :: k -> 'Type'@ is a type constructor, then @'DecidableTC' T@ is+-- a constraint that @T@ is "decidable", in that you have a canonical+-- function:+--+-- @+-- decideTC :: Sing a -> 'Decision' (T a)+-- @+--+-- Is essentially 'Decidable', except with /type constructors/ @k ->+-- 'Type'@ instead of matchable type-level functions (that are @k ~>+-- 'Type'@).+--+-- @since 0.1.1.0+type DecidableTC p = Decidable (TyPred p)++-- | The canonical deciding function for @'DecidableTC' t@.+--+-- @since 0.1.1.0+decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)+decideTC = decide @(TyPred t)++-- | If @T :: k -> 'Type'@ is a type constructor, then @'ProvableTC' T@ is+-- a constraint that @T@ is "decidable", in that you have a canonical+-- function:+--+-- @+-- proveTC :: Sing a -> T a+-- @+--+-- Is essentially 'Provable', except with /type constructors/ @k -> 'Type'@+-- instead of matchable type-level functions (that are @k ~> 'Type'@).+--+-- @since 0.1.1.0+type ProvableTC  p = Provable  (TyPred p)++-- | The canonical proving function for @'DecidableTC' t@.+--+-- @since 0.1.1.0+proveTC :: forall t a. ProvableTC t => Sing a -> t a+proveTC = prove @(TyPred t)+ -- | Implicatons @p '-?>' q@ can be lifted "through" a 'DFunctor' into an -- @f p '-?>' f q@. class DFunctor f where@@ -299,8 +349,20 @@     :: forall p a. ()     => Decision (p @@ a)     -> Decision (Not p @@ a)-decideNot = \case-    Proved p    -> Disproved ($ p)+decideNot = flipDecision++-- | Flip the contents of a decision.  Turn a proof of @a@ into a disproof+-- of not-@a@.+--+-- Note that this is not reversible in general in Haskell.  See+-- 'doubleNegation' for a situation where it is.+--+-- @since 0.1.1.0+flipDecision+    :: Decision a+    -> Decision (Refuted a)+flipDecision = \case+    Proved    p -> Disproved ($ p)     Disproved v -> Proved v  -- | Map over the value inside a 'Decision'.@@ -312,3 +374,36 @@ mapDecision f g = \case     Proved    p -> Proved $ f p     Disproved v -> Disproved $ v . g++-- | Converts a 'Decision' to a 'Maybe'.  Drop the witness of disproof of+-- @a@, returning 'Just' if 'Proved' (with the proof) and 'Nothing' if+-- 'Disproved'.+--+-- @since 0.1.1.0+forgetDisproof+    :: Decision a+    -> Maybe a+forgetDisproof = \case+    Proved    p -> Just p+    Disproved _ -> Nothing++-- | Drop the witness of proof of @a@, returning 'Nothing' if 'Proved' and+-- 'Just' if 'Disproved' (with the disproof).+--+-- @since 0.1.1.0+forgetProof+    :: Decision a+    -> Maybe (Refuted a)+forgetProof = forgetDisproof . flipDecision++-- | Boolean test if a 'Decision' is 'Proved'.+--+-- @since 0.1.1.0+isProved :: Decision a -> Bool+isProved = isJust . forgetDisproof++-- | Boolean test if a 'Decision' is 'Disproved'.+--+-- @since 0.1.1.0+isDisproved :: Decision a -> Bool+isDisproved = isNothing . forgetDisproof

@@ -0,0 +1,139 @@+{-# LANGUAGE AllowAmbiguousTypes   #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeInType            #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE TypeSynonymInstances  #-}++-- |+-- Module      : Data.Type.Predicate.Auto+-- Copyright   : (c) Justin Le 2018+-- License     : BSD3+--+-- Maintainer  : justin@jle.im+-- Stability   : experimental+-- Portability : non-portable+--+-- Useful utilities for situations where you know that a predicate @P@ is+-- satisfied for a specific @a@ at compile-time.+--+-- @since 0.1.1.0+module Data.Type.Predicate.Auto (+    Auto(..)+  , AutoElem(..)+  , AutoProvable+  ) where++import           Data.List.NonEmpty        (NonEmpty(..))+import           Data.Singletons+import           Data.Type.Equality+import           Data.Type.Predicate+import           Data.Type.Predicate.Logic+import           Data.Type.Universe++-- | Automatically generate a witness for predicate @p@ applied to input+-- @a@.+--+-- Mostly useful for situations where you know @a@ at compile-time, so you+-- can just write 'auto' directly in your source code.  The choice is+-- intended to mirror the @auto@ keyword in languages like Idris.+--+-- Very close in nature to the @Known@ typeclass in the /type-combinators/+-- library.+class Auto (p :: Predicate k) (a :: k) where+    -- | Have the compiler generate a witness for @p \@\@ a@.+    --+    -- Must be called using type application syntax:+    --+    -- @+    -- 'auto' @_ @p @a+    -- @+    auto :: p @@ a++instance SingI a => Auto Evident a where+    auto = sing++instance Auto (EqualTo a) a where+    auto = Refl++instance (Auto p a, Auto q a) => Auto (p &&& q) a where+    auto = (auto @_ @p @a, auto @_ @q @a)++instance Auto q a => Auto (p ==> q) a where+    auto _ = auto @_ @q @a++-- | Helper "predicate transformer" that gives you an instant 'auto' for+-- any 'Provable' instance.+--+-- For example, say you have predicate @P@ that you know is 'Provable', and+-- you wish to generate a @P \@\@ x@, for some specific @x@ you know at+-- compile-time.  You can use:+--+-- @+-- 'auto' @_ @(AutoProvable P) @x+-- @+--+-- to obtain a @P \@\@ x@.+--+-- 'AutoProvable' is essentially the identity function.+data AutoProvable :: Predicate k -> Predicate k+type instance Apply (AutoProvable p) a = p @@ a++instance (Provable p, SingI a) => Auto (AutoProvable p) a where+    auto = prove @p @a sing++-- | Typeclass representing 'Elem's pointing to an @a :: k@ that can be+-- generated automatically from type-level collection @as :: f k@.  +--+-- If GHC knows both the type-level collection and the element you want to+-- find at compile-time, this instance should allow it to find it.+--+-- Used to help in the instance of 'Auto' for the 'In' predicate.+--+-- Example usage:+--+-- @+-- autoElem :: Index '[1,6,2,3] 2+-- -- IS (IS IZ)        -- third spot+-- @+--+-- And when used with 'Auto':+--+-- @+-- auto @_ @(In [] '[1,6,2,3]) @2+-- -- IS (IS IZ)+-- @+class AutoElem f (as :: f k) (a :: k) where+    -- | Generate the 'Elem' pointing to the @a :: @ in a type-level+    -- collection @as :: f k@.+    autoElem :: Elem f as a++instance {-# OVERLAPPING #-} AutoElem [] (a ': as) a where+    autoElem = IZ++instance {-# OVERLAPPING #-} AutoElem [] as a => AutoElem [] (b ': as) a where+    autoElem = IS autoElem++instance AutoElem Maybe ('Just a) a where+    autoElem = IsJust++instance AutoElem (Either j) ('Right a) a where+    autoElem = IsRight++instance AutoElem NonEmpty (a ':| as) a where+    autoElem = NEHead++instance AutoElem [] as a => AutoElem NonEmpty (b ':| as) a where+    autoElem = NETail autoElem++instance AutoElem f as a => Auto (In f as) a where+    auto = autoElem @f @as @a+

@@ -76,12 +76,6 @@ 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. ()@@ -137,6 +131,42 @@         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))++-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Decidable (p &&& q ==> p) where+-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Provable (p &&& q ==> p) where+    prove = projAndFst @p @q++-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Decidable (p &&& q ==> q) where+-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Provable (p &&& q ==> q) where+    prove = projAndSnd @p @q++-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Decidable (p &&& p ==> p) where+-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Provable (p &&& p ==> p) where+    prove = projAndFst @p @p++-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Decidable (p ==> p ||| q)+-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Provable (p ==> p ||| q) where+    prove = injOrLeft @p @q++-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Decidable (q ==> p ||| q)+-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Provable (q ==> p ||| q) where+    prove = injOrRight @p @q++-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Decidable (p ==> p ||| p)+-- | @since 0.1.1.0+instance {-# OVERLAPPING #-} Provable (p ==> p ||| p) where+    prove = injOrLeft @p @p  -- | @'Implies' p q@ is a constraint that @p '==>' q@ is 'Provable'; that -- is, you can prove that @p@ implies @q@.

@@ -35,7 +35,6 @@   ) where  import           Data.Singletons-import           Data.Singletons.Decide import           Data.Singletons.Sigma import           Data.Type.Predicate import           Data.Type.Predicate.Logic@@ -82,9 +81,10 @@ 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)+    decide = mapDecision (\case i :&: p -> i :&: p)+                         (\case i :&: p -> i :&: p)+           . decide @(Found p)+           . applySing (sing :: Sing f)     -- can just be sing @f in singletons 2.5, ghc 8.6+  instance (Provable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Provable (Found (PPMap f p)) where     prove (x :: Sing a) = case prove @(Found p) ((sing :: Sing f) @@ x) of@@ -132,10 +132,9 @@ 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+    decide = mapDecision (\case WitAny i s -> s :&: i    )+                         (\case s :&: i     -> WitAny i s)+           . decide @(NotNull f)  instance Decidable (NotNull f ==> Found (InP f)) instance Provable (NotNull f ==> Found (InP f)) where@@ -159,8 +158,6 @@ 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)-+    decide = mapDecision (\case WitAny i (x :&: p) -> x :&: WitAny i p  )+                         (\case x :&: WitAny i p   -> WitAny i (x :&: p))+           . decide @(Any f (Found p))

@@ -67,7 +67,7 @@  -- | @'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)+type In (f :: Type -> Type) (as :: f k) = ElemSym1 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.@@ -191,7 +191,7 @@ -- 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 f 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)@@ -221,7 +221,7 @@  -- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist. splitSing-    :: forall f (as :: f k). Universe f+    :: forall f k (as :: f k). Universe f     => Sing as     -> All f (TyPred Sing) @@ as splitSing = igenAll @f @_ @(TyPred Sing) (\_ x -> x)@@ -230,9 +230,10 @@ 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+pickElem = mapDecision (\case WitAny i Refl -> i)+                       (\case i -> WitAny i Refl)+         . decide @(Any f (TyPred ((:~:) a)))+         $ sing  -- | 'foldMapUni' but with access to the index. ifoldMapUni@@ -294,7 +295,7 @@         Disproved v -> Disproved $ \a -> v $ runWitAll a IZ      igenAllA-        :: forall (p :: k ~> Type) (as :: [k]) h. Applicative h+        :: forall k (p :: k ~> Type) (as :: [k]) h. Applicative h         => (forall a. Elem [] as a -> Sing a -> h (p @@ a))         -> Sing as         -> h (All [] p @@ as)@@ -406,7 +407,7 @@       Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead      igenAllA-        :: forall (p :: k ~> Type) (as :: NonEmpty k) h. Applicative h+        :: forall k (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)

@@ -75,6 +75,8 @@  -- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied -- predicates.+--+-- List is meant to include no duplicates. subsetToList     :: forall f p t. (Universe f, Alternative t)     => (Subset f p --># Any f p) t@@ -156,13 +158,13 @@ -- | Map a bidirectional implication over a subset described by that -- implication. ----- Implication needs to be bidirection, or otherwise we can't produce+-- Implication needs to be bidirectional, or otherwise we can't produce -- a /decidable/ subset as a result. mapSubset     :: Universe f     => (p --> q)     -> (q --> p)     -> (Subset f p --> Subset f q)-mapSubset f g xs@Sing = withSingI xs $+mapSubset f g xs = withSingI xs $     imapSubset (\i -> f (index i xs))                (\i -> g (index i xs))