dec (empty) → 0.0.3

raw patch · 4 files changed

+184/−0 lines, 4 filesdep +basedep +void

Dependencies added: base, void

Files

• ChangeLog.md +5/−0
• LICENSE +30/−0
• dec.cabal +42/−0
• src/Data/Type/Dec.hs +107/−0

@@ -0,0 +1,5 @@+# Revision history for dec++## 0.0.3++- First version. Released on an unsuspecting world.

@@ -0,0 +1,30 @@+Copyright (c) 2019, Oleg Grenrus++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 Oleg Grenrus 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.

@@ -0,0 +1,42 @@+cabal-version:      >=1.10+name:               dec+version:            0.0.3+synopsis:           Decidable propositions.+category:           Data, Dependent Types+description:+  This package provides a @Dec@ type.+  .+  @+  type Not a = a -> Void+  .+  data Dec a+  \    = Yes a+  \    | No (Not a)+  @++homepage:           https://github.com/phadej/vec+bug-reports:        https://github.com/phadej/vec/issues+license:            BSD3+license-file:       LICENSE+author:             Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>+copyright:          (c) 2019 Oleg Grenrus+build-type:         Simple+extra-source-files: ChangeLog.md+tested-with:+  GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4++source-repository head+  type:     git+  location: https://github.com/phadej/vec.git++library+  exposed-modules:  Data.Type.Dec+  build-depends:    base >=4.7 && <4.13++  if !impl(ghc >=7.10)+    build-depends: void >=0.7.2 && <0.8++  ghc-options:      -Wall -fprint-explicit-kinds+  hs-source-dirs:   src+  default-language: Haskell2010

@@ -0,0 +1,107 @@+module Data.Type.Dec (+    -- * Types+    Neg,+    Dec (..),+    Decidable (..),+    -- * Neg combinators+    toNegNeg,+    tripleNeg,+    contradict,+    contraposition,+    -- * Dec combinators+    decNeg,+    decShow,+    decToMaybe,+    decToBool,+    ) where++import Data.Void          (Void)++-- | Intuitionistic negation.+type Neg a = a -> Void++-- | Decidable (nullary) relations.+data Dec a+    = Yes a+    | No (Neg a)++-- | Class of decidable types.+--+-- == Law+--+-- @a@ should be a Proposition, i.e. the 'Yes' answers should be unique.+--+-- /Note:/ We'd want to have decidable equality @:~:@ here too,+-- but that seems to be a deep dive into singletons.+class Decidable a where+    decide :: Dec a++-------------------------------------------------------------------------------+-- Neg combinators+-------------------------------------------------------------------------------++-- | We can negate anything twice.+--+-- Double-negation elimination is inverse of 'toNegNeg' and generally+-- impossible.+toNegNeg :: a -> Neg (Neg a)+toNegNeg x = ($ x)++-- | Triple negation can be reduced to a single one.+tripleNeg :: Neg (Neg (Neg a)) -> Neg a+tripleNeg f a = f (toNegNeg a)++-- | Weak contradiction.+contradict :: (a -> Neg b) -> b -> Neg a+contradict f b a = f a b++-- | A variant of contraposition.+contraposition :: (a -> b) -> Neg b -> Neg a+contraposition f nb a = nb (f a)++-------------------------------------------------------------------------------+-- Dec combinators+-------------------------------------------------------------------------------++instance Eq a => Eq (Dec a) where+    Yes x == Yes y = x == y+    Yes _ == No _   = False+    No _  == Yes _  = False+    No _  == No _   = True  -- @'Not a' is a /h-Prop/ so all values are equal.++-- | 'decToBool' respects this ordering.+--+-- /Note:/ yet if you have @p :: a@ and @p :: 'Neg' a@, something is wrong.+--+instance Ord a => Ord (Dec a) where+    compare (Yes a) (Yes b) = compare a b+    compare (No _)  (Yes _) = compare False True+    compare (Yes _) (No _)  = compare True False+    compare (No _)  (No _)  = EQ++-- | Flip 'Dec' branches.+decNeg :: Dec a -> Dec (Neg a)+decNeg (Yes p) = No (toNegNeg p)+decNeg (No np) = Yes np++-- | Show 'Dec'.+--+-- >>> decShow $ Yes ()+-- "Yes ()"+--+-- >>> decShow $ No id+-- "No <toVoid>"+--+decShow :: Show a => Dec a -> String+decShow (Yes x) = "Yes " ++ showsPrec 11 x ""+decShow (No _)  = "No <toVoid>"++-- | Convert @'Dec' a@ to @'Maybe' a@, forgetting the 'No' evidence.+decToMaybe :: Dec a -> Maybe a+decToMaybe (Yes p) = Just p+decToMaybe (No _)  = Nothing++-- | Convert 'Dec' to 'Bool', forgetting the evidence.+decToBool :: Dec a -> Bool+decToBool (Yes _) = True+decToBool (No _)  = False