dec 0.0.4 → 0.0.5

raw patch · 3 files changed

+71/−7 lines, 3 filesdep +boringdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: boring

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +6/−0
• dec.cabal +10/−7
• src/Data/Type/Dec.hs +55/−0

@@ -1,5 +1,11 @@ # Revision history for dec +## 0.0.5++- Add `boringYes` and `absurdNo`.+- Add `Decidable a => Boring (Dec a)` instance.+- Add `Decidable ()`, `Decidable Void`, `Decidable (a, b)` instances.+ ## 0.0.4  - Mark module as explicitly `Safe`.

@@ -1,6 +1,6 @@ cabal-version:      >=1.10 name:               dec-version:            0.0.4+version:            0.0.5 synopsis:           Decidable propositions. category:           Data, Dependent Types description:@@ -31,25 +31,28 @@    || ==8.4.4    || ==8.6.5    || ==8.8.4-   || ==8.10.3-   || ==9.0.1+   || ==8.10.4+   || ==9.0.2+   || ==9.2.4+   || ==9.4.1  source-repository head   type:     git-  location: https://github.com/phadej/vec.git-  subdir:   dec+  location: https://github.com/phadej/dec.git  library   default-language: Haskell2010   hs-source-dirs:   src   ghc-options:      -Wall -fprint-explicit-kinds   exposed-modules:  Data.Type.Dec-  build-depends:    base >=4.7 && <4.16+  build-depends:+      base    >=4.7 && <4.18+    , boring  >=0.2 && <0.3    if !impl(ghc >=7.10)     build-depends: void >=0.7.3 && <0.8 -  if impl(ghc >= 9.0)+  if impl(ghc >=9.0)     -- these flags may abort compilation with GHC-8.10     -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295     ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode

@@ -1,4 +1,5 @@ {-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-} module Data.Type.Dec (     -- * Types     Neg,@@ -14,9 +15,15 @@     decShow,     decToMaybe,     decToBool,++    -- * Boring+    -- | @'Dec' a@ can be 'Boring' in two ways: When 'a' is 'Boring' or 'Absurd'.+    boringYes,+    absurdNo,     ) where  import Data.Void (Void)+import Data.Boring (Absurd (..), Boring (..))  -- | Intuitionistic negation. type Neg a = a -> Void@@ -38,6 +45,32 @@     decide :: Dec a  -------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++-- | @()@ is truth.+--+-- @since 0.0.5+instance Decidable () where+    decide = Yes ()++-- | 'Void' is falsehood.+--+-- @since 0.0.5+instance Decidable Void where+    decide = No id++-- | Products of decidable propositions are decidable+--+-- @since 0.0.5+instance (Decidable a, Decidable b) => Decidable (a, b) where+    decide = case decide :: Dec a of+        No nx -> No (\c -> nx (fst c))+        Yes x -> case decide :: Dec b of+            No ny -> No (\c -> ny (snd c))+            Yes y -> Yes (x, y)++------------------------------------------------------------------------------- -- Neg combinators ------------------------------------------------------------------------------- @@ -106,3 +139,25 @@ decToBool :: Dec a -> Bool decToBool (Yes _) = True decToBool (No _)  = False++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | This relies on the fact that @a@ is /proposition/ in h-Prop sense.+--+-- @since 0.0.5+instance Decidable a => Boring (Dec a) where+    boring = decide++-- | 'Yes', it's 'boring'.+--+-- @since 0.0.5+boringYes :: Boring a => Dec a+boringYes = Yes boring++-- | 'No', it's 'absurd'.+--+-- @since 0.0.5+absurdNo :: Absurd a => Dec a+absurdNo = No absurd