heyting-algebras 0.0.1.1 → 0.0.1.2

raw patch · 4 files changed

+60/−13 lines, 4 filesPVP: minor bump suggested

API additions: PVP suggests at least a minor version bump

API changes (from Hackage documentation)

Files

• README.md +36/−0
• heyting-algebras.cabal +4/−2
• src/Algebra/Heyting.hs +7/−2
• test/Main.hs +13/−9

@@ -0,0 +1,36 @@+# Heyting Algebras+[![Maintainer: coot](https://img.shields.io/badge/maintainer-coot-lightgrey.svg)](http://github.com/coot)+[![Travis Build Status](https://travis-ci.org/coot/heyting-algebras.svg?branch=master)](https://travis-ci.org/coot/heyting-algebras)++This package contains type classes and instances for many Heyting algebras+which are in the Haskell eco-system.  It is build on top of+[lattices](https://hackage.haskell.org/package/lattices) and+[free-algebras](https://hackage.haskell.org/package/free-algebras) (to provide+combinators for free Heyting algebras).  The package also defines a type class+for Boolean algebras and comes with a handful of instances.++A very good introduction to Heyting algebras can be found at+[ncatlab](https://ncatlab.org/nlab/show/Heyting%2Balgebra).  Heyting algebras+are the crux of [intuitionistic+logic](https://en.wikipedia.org/wiki/Intuitionistic_logic), which drops the+axiom of exluded middle.  From categorical point of view, Heyting algebras are+posets (categories with at most one arrow between any objects), which are also+Cartesian closed (and finitely (co-)complete).  Note that this makes any+Heyting algebra a simply typed lambda calculus; hence one more incentive to+learn how to use them.++The most important operation is implication `(==>) :: HeytingAlgebra a => a ->+a -> a`; since every Boolean algebra is a Heyting algebra via `a ==>+b = not a \/ b` (using the lattice notation for `or`).  It is very handy in+expression conditional logic.++Some basic examples of Heyting algebras:+* `Bool` is a Boolean algebra+* `(Ord a, Bounded a) => a`; the implication is defined as: if `a ≤ b` then `a+  ⇒ b = maxBound`; otherwise `a ⇒ b = b`; e.g. integers with both `±∞` (it can+  be represented by `Levitated Int`.  This type is not a Boolean algebra.+* The power set is a Boolean algebra, in Haskell it can be represented by `Set+  a` (one might need to require `a` to be finite though, otherwise `not (not+  empty)` might be `undefined` rather than `empty`).+* More generally every type `(Ord k, Finite k, HeytingAlgebra v) => Map k a` is+  a Heyting algebra (though in general not a Boolean one).

@@ -1,5 +1,5 @@ name:                heyting-algebras-version:             0.0.1.1+version:             0.0.1.2 synopsis:            Heyting and Boolean algebras description:   This package provides Heyting and Boolean operations together@@ -11,7 +11,9 @@ copyright:           (c) 2018 Marcin Szamotulski category:            Math build-type:          Simple-extra-source-files:  ChangeLog.md+extra-source-files:+  ChangeLog.md+  README.md cabal-version:       >=1.10 tested-with:         GHC==8.2.2, GHC==8.4.3 

@@ -45,9 +45,10 @@ import Algebra.Lattice.Lifted (Lifted (..)) import Algebra.Lattice.Levitated (Levitated) import qualified Algebra.Lattice.Levitated as L+import Algebra.Lattice.Ordered (Ordered (..)) import Algebra.PartialOrd (leq) #ifdef EXPORT_PROPERTIES-import Test.QuickCheck hiding ((==>))+import Test.QuickCheck hiding (Ordered, (==>)) import qualified Test.QuickCheck as QC #endif @@ -139,7 +140,7 @@   (a0, b0) ==> (a1, b1) = (a0 ==> a1, b0 ==> b1)  ----- Dropped, Lifted, Levitated+-- Dropped, Lifted, Levitated, Ordered --  instance (Eq a, HeytingAlgebra a) => HeytingAlgebra (Dropped a) where@@ -160,6 +161,10 @@   _              ==> L.Top          = L.Top   L.Bottom       ==> _              = L.Top   _              ==> L.Bottom       = L.Bottom++instance (Ord a, Bounded a) => HeytingAlgebra (Ordered a) where+  Ordered a ==> Ordered b | a <= b    = top+                          | otherwise = Ordered b  -- -- containers

@@ -13,18 +13,17 @@ import Algebra.Lattice.Lifted (Lifted (..)) import Algebra.Lattice.Levitated (Levitated) import qualified Algebra.Lattice.Levitated as L+import Algebra.Lattice.Ordered (Ordered (..)) import Data.Universe.Class (Universe (..), Finite) import qualified Data.Set as S import qualified Data.Map as M -import Test.QuickCheck- import Algebra.Boolean import Algebra.Heyting import Algebra.Heyting.Layered  import Test.Tasty-import Test.Tasty.QuickCheck+import Test.Tasty.QuickCheck hiding (Ordered)  -- | Arbitrary wrapper newtype Arb a = Arb a@@ -76,6 +75,10 @@     : [ Arb (L.Levitate a') | a' <- shrink a ]   shrink (Arb L.Top) = [] +instance Arbitrary a => Arbitrary (Arb (Ordered a)) where+  arbitrary = Arb . Ordered <$> arbitrary+  shrink (Arb (Ordered a)) = [ Arb (Ordered a') | a' <- shrink a ]+ data S5 = S1 | S2 | S3 | S4 | S5   deriving (Ord, Eq, Show) @@ -170,24 +173,25 @@ tests :: TestTree tests =   testGroup "heyting-algebras tests"-    [ testGroup "BooleanAlgebra tests"+    [ testGroup "Boolean algebras"         [ testProperty "Bool"                  $ prop_BooleanAlgebra @Bool         , testProperty "(Bool, Bool)"          $ prop_BooleanAlgebra @(Bool, Bool)         , testProperty "Boolean (Lifted Bool)" $ prop_BooleanAlgebra @(Boolean (Arb (Lifted Bool)))         , testProperty "(Set S5)"              $ prop_BooleanAlgebra @(Arb (S.Set S5))         ]-    , testGroup "Not BooleanAlgebra tests"-        [ testProperty "Not BooleanAlgebra (Lifted Bool)"    $ expectFailure $ prop_not @(Arb (Lifted Bool))-        , testProperty "Not BooleanAlgebra (Dropped Bool)"   $ expectFailure $ prop_not @(Arb (Dropped Bool))-        , testProperty "Not BooleanAlgebra (Levitated Bool)" $ expectFailure $ prop_not @(Arb (Levitated Bool))+    , testGroup "Non Boolean algebras"+        [ testProperty "Not a BooleanAlgebra (Lifted Bool)"    $ expectFailure $ prop_not @(Arb (Lifted Bool))+        , testProperty "Not a BooleanAlgebra (Dropped Bool)"   $ expectFailure $ prop_not @(Arb (Dropped Bool))+        , testProperty "Not a BooleanAlgebra Levitated (Ordered Int)" $ expectFailure $ prop_BooleanAlgebra @(Arb (Levitated (Arb (Ordered Int))))         ]-    , testGroup "HeytingAlgebra tests"+    , testGroup "Heyting algebras"         [ testProperty "Lifted Bool"            $ prop_HeytingAlgebra @(Arb (Lifted Bool))         , testProperty "Dropped Bool"           $ prop_HeytingAlgebra @(Arb (Dropped Bool))         , testProperty "Layered Bool Bool"      $ prop_HeytingAlgebra @(Arb (Layered Bool Bool))         , testProperty "Levitated Bool"         $ prop_HeytingAlgebra @(Arb (Levitated Bool))         , testProperty "Sum (Lifted Bool) (Dropped Bool)"                                                 $ prop_HeytingAlgebra @(Arb (Layered (Arb (Lifted Bool)) (Arb (Dropped Bool))))+        , testProperty "Levitated (Ordered Int)" $ prop_HeytingAlgebra @(Arb (Levitated (Arb (Ordered Int))))         , testProperty "Map S5 Bool"            $ prop_HeytingAlgebra @(Arb (M.Map S5 Bool))         , testProperty "Dropped (Lifted Bool)"  $ prop_HeytingAlgebra @(Composed Dropped Lifted Bool)         , testProperty "Lifted (Dropped Bool)"  $ prop_HeytingAlgebra @(Composed Lifted Dropped Bool)