diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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). diff --git a/heyting-algebras.cabal b/heyting-algebras.cabal --- a/heyting-algebras.cabal +++ b/heyting-algebras.cabal @@ -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 diff --git a/src/Algebra/Heyting.hs b/src/Algebra/Heyting.hs --- a/src/Algebra/Heyting.hs +++ b/src/Algebra/Heyting.hs @@ -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 diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -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)