diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,10 @@ # Revision history for heyting-algebra +## 0.1.0.0 + +* Swapped Boolean (now a type class) and BooleanAlgebra (now a data type) +* Reexport Algebra.Heyting and Algebra.Heyting.Free modules from lattices + ## 0.0.2.0 * Added Algebra.Heyting.CounterExample diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,13 +1,12 @@ # 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) +[![POSIX](https://github.com/coot/heyting-algebras/actions/workflows/posix.yml/badge.svg)](https://github.com/coot/heyting-algebras/actions/workflows/posix.yml) -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 many useful instances. + +This package now extends +[lattices](https://hackage.haskell.org/package/lattices) by providing more +Heyting algebras. The package also defines a type class for Boolean algebras +and comes with many useful instances. A note about notation: this package is based on [lattices](https://hackage.haskell.org/package/lattices), and both are using diff --git a/heyting-algebras.cabal b/heyting-algebras.cabal --- a/heyting-algebras.cabal +++ b/heyting-algebras.cabal @@ -1,5 +1,6 @@ +cabal-version: 2.0 name: heyting-algebras -version: 0.0.2.0 +version: 0.2.0.1 synopsis: Heyting and Boolean algebras description: This package provides Heyting and Boolean operations together @@ -8,35 +9,34 @@ license-file: LICENSE author: Marcin Szamotulski maintainer: profunctor@pm.me -copyright: (c) 2018-2019 Marcin Szamotulski +copyright: (c) 2018-2021 Marcin Szamotulski category: Math build-type: Simple extra-source-files: ChangeLog.md README.md -cabal-version: >=1.10 -tested-with: GHC==8.0.2, GHC==8.2.2, GHC==8.4.4, GHC==8.6.3 +tested-with: GHC==8.10.4 library - exposed-modules: Algebra.Heyting - Algebra.Heyting.Free - Algebra.Heyting.Layered + exposed-modules: Algebra.Heyting.Layered Algebra.Heyting.BoolRing Algebra.Heyting.CounterExample Algebra.Heyting.Properties Algebra.Boolean Algebra.Boolean.Free Algebra.Boolean.Properties - build-depends: base >= 4.9 && < 4.13 - , containers >= 0.4.2 && < 0.7 - , free-algebras >= 0.0.4 && < 0.0.8 - , hashable >= 1.2.6.1 && < 1.3 - , lattices >= 1.0 && < 1.8 + reexported-modules: lattices:Algebra.Heyting + , lattices:Algebra.Heyting.Free + build-depends: base >= 4.9 && < 4.16 + , containers >= 0.4.2 && < 0.7 + , free-algebras >= 0.1.0.1 && < 0.1.1.0 + , hashable >= 1.2.6.1 && < 1.4 + , lattices >= 2.0 && < 2.1 , semiring-simple >= 1.0 && < 1.2 - , tagged >= 0.8.5 && < 0.9 + , tagged >= 0.8.5 && < 0.9 , unordered-containers - >= 0.2.6.0 && < 0.3 - , universe-base >= 1.0 && < 1.1 + >= 0.2.6.0 && < 0.3 + , universe-base >= 1.0 && < 1.2 hs-source-dirs: src default-language: Haskell2010 default-extensions: FlexibleInstances @@ -44,7 +44,7 @@ PackageImports ghc-options: -Wall -test-suite tests +test-suite test type: exitcode-stdio-1.0 hs-source-dirs: test main-is: Main.hs diff --git a/src/Algebra/Boolean.hs b/src/Algebra/Boolean.hs --- a/src/Algebra/Boolean.hs +++ b/src/Algebra/Boolean.hs @@ -5,52 +5,79 @@ module Algebra.Boolean ( BooleanAlgebra , (==>) - , not - , iff - , iff' + , neg -- * Adjunction between Boolean and Heyting algebras , Boolean - , runBoolean + , runBooleanAlgebra , boolean ) where -import Prelude hiding (not) - +import Control.Applicative (Const (..)) import Data.Data (Data, Typeable) +import Data.Functor.Identity (Identity (..)) +import Data.Proxy (Proxy (..)) +import Data.Semigroup ( All (..) + , Any (..) + , Endo (..) + ) +import Data.Tagged (Tagged (..)) import GHC.Generics (Generic) +import Algebra.Heyting import Algebra.Lattice ( Lattice - , BoundedLattice - , JoinSemiLattice (..) , BoundedJoinSemiLattice - , MeetSemiLattice (..) , BoundedMeetSemiLattice ) -import Algebra.Heyting ( HeytingAlgebra (..) - , BooleanAlgebra - , iff - , iff' - , not - , toBoolean - ) +class Heyting a => Boolean a +instance Boolean Bool + +instance Boolean All + +instance Boolean Any + +instance Boolean () + +instance Boolean (Proxy a) + +instance Boolean a => Boolean (Tagged t a) + +instance Boolean b => Boolean (a -> b) + +#if MIN_VERSION_base(4,8,0) +instance Boolean a => Boolean (Identity a) +#endif + +instance Boolean a => Boolean (Const a b) + +instance Boolean a => Boolean (Endo a) + +-- | Every Heyting algebra contains a Boolean algebra. @'toBoolean'@ maps onto +-- it; moreover it is a monad (Heyting algebra is a category as every poset is) +-- which preserves finite infima. +-- +toBoolean :: Heyting a => a -> a +toBoolean = neg . neg + -- | -- @'Boolean'@ is the left adjoint functor from the category of Heyting algebras -- to the category of Boolean algebras; its right adjoint is the inclusion. -newtype Boolean a = Boolean - { runBoolean :: a -- ^ extract value from @'Boolean'@ +newtype BooleanAlgebra a = BooleanAlgebra + { runBooleanAlgebra :: a -- ^ extract value from @'Boolean'@ } deriving - ( JoinSemiLattice, BoundedJoinSemiLattice, MeetSemiLattice - , BoundedMeetSemiLattice, Lattice, BoundedLattice, HeytingAlgebra + ( BoundedJoinSemiLattice + , BoundedMeetSemiLattice + , Lattice + , Heyting , Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic ) -instance HeytingAlgebra a => BooleanAlgebra (Boolean a) +instance Heyting a => Boolean (BooleanAlgebra a) -- | -- Smart constructro of the @'Boolean'@ type. -boolean :: HeytingAlgebra a => a -> Boolean a -boolean = Boolean . toBoolean +boolean :: Heyting a => a -> BooleanAlgebra a +boolean = BooleanAlgebra . toBoolean diff --git a/src/Algebra/Boolean/Free.hs b/src/Algebra/Boolean/Free.hs --- a/src/Algebra/Boolean/Free.hs +++ b/src/Algebra/Boolean/Free.hs @@ -5,58 +5,45 @@ import Control.Monad (ap) import Algebra.Lattice ( BoundedJoinSemiLattice (..) - , JoinSemiLattice (..) , BoundedMeetSemiLattice (..) - , MeetSemiLattice (..) - , BoundedLattice - , Lattice + , Lattice (..) ) import Data.Algebra.Free ( AlgebraType0 , AlgebraType , FreeAlgebra (..) - , proof , fmapFree , bindFree ) -import Algebra.Boolean (BooleanAlgebra) -import Algebra.Heyting (HeytingAlgebra (..)) +import Algebra.Boolean (Boolean) +import Algebra.Heyting -- | -- Free Boolean algebra. @'FreeAlgebra'@ instance provides all the usual -- combinators for a free algebra. newtype FreeBoolean a = FreeBoolean - { runFreeBoolean :: forall h . BooleanAlgebra h => (a -> h) -> h } - -instance JoinSemiLattice (FreeBoolean a) where - FreeBoolean f \/ FreeBoolean g = FreeBoolean (\inj -> f inj \/ g inj) + { runFreeBoolean :: forall h . Boolean h => (a -> h) -> h } instance BoundedJoinSemiLattice (FreeBoolean a) where bottom = FreeBoolean (\_ -> bottom) -instance MeetSemiLattice (FreeBoolean a) where - FreeBoolean f /\ FreeBoolean g = FreeBoolean (\inj -> f inj /\ g inj) - instance BoundedMeetSemiLattice (FreeBoolean a) where top = FreeBoolean (\_ -> top) -instance Lattice (FreeBoolean a) - -instance BoundedLattice (FreeBoolean a) +instance Lattice (FreeBoolean a) where + FreeBoolean f /\ FreeBoolean g = FreeBoolean (\inj -> f inj /\ g inj) + FreeBoolean f \/ FreeBoolean g = FreeBoolean (\inj -> f inj \/ g inj) -instance HeytingAlgebra (FreeBoolean a) where +instance Heyting (FreeBoolean a) where FreeBoolean f ==> FreeBoolean g = FreeBoolean (\inj -> f inj ==> g inj) -instance BooleanAlgebra (FreeBoolean a) +instance Boolean (FreeBoolean a) type instance AlgebraType0 FreeBoolean a = () -type instance AlgebraType FreeBoolean a = BooleanAlgebra a +type instance AlgebraType FreeBoolean a = Boolean a instance FreeAlgebra FreeBoolean where returnFree a = FreeBoolean (\inj -> inj a) foldMapFree f (FreeBoolean inj) = inj f - - codom = proof - forget = proof instance Functor FreeBoolean where fmap = fmapFree diff --git a/src/Algebra/Boolean/Properties.hs b/src/Algebra/Boolean/Properties.hs --- a/src/Algebra/Boolean/Properties.hs +++ b/src/Algebra/Boolean/Properties.hs @@ -14,12 +14,17 @@ -- | -- Test that @'not'@ satisfies Boolean algebra axioms. -prop_not :: (HeytingAlgebra a, Ord a, Eq a, Ord e) => a -> CounterExample e -prop_not a = - (not (not a) === a) - /\ (not a /\ a === bottom) - /\ (not a \/ a === top) +prop_neg :: (Heyting a, Ord a, Eq a, Ord e) => a -> CounterExample e +prop_neg a = + (neg (neg a) === a) + /\ (neg a /\ a === bottom) + /\ (neg a \/ a === top) +prop_not :: (Heyting a, Ord a, Eq a, Ord e) => a -> CounterExample e +prop_not = prop_neg + +{-# DEPRECATED prop_not "Use prop_neg" #-} + data BooleanAlgebraLawViolation a = BALVHeytingAlgebraLawViolation (HeytingAlgebraLawViolation a) | BALVNotLawViolation a @@ -29,7 +34,7 @@ -- Test that @a@ is satisfy both @'Algebra.Heyting.prop_HeytingAlgebra'@ and -- @'prop_not'@. prop_BooleanAlgebra - :: (BooleanAlgebra a, Ord a, Eq a, Show a) + :: (Boolean a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (BooleanAlgebraLawViolation a) prop_BooleanAlgebra a b c = (fmapCounterExample BALVHeytingAlgebraLawViolation $ prop_HeytingAlgebra a b c) diff --git a/src/Algebra/Heyting.hs b/src/Algebra/Heyting.hs deleted file mode 100644 --- a/src/Algebra/Heyting.hs +++ /dev/null @@ -1,314 +0,0 @@ -{-# LANGUAGE CPP #-} - -module Algebra.Heyting - ( -- * Heyting algebras - HeytingAlgebra (..) - , implies - , (<=>) - , iff - , iff' - , toBoolean - -- * Boolean algebras - , BooleanAlgebra - ) - where - - -import Prelude hiding (not) -import qualified Prelude - -import Control.Applicative (Const (..)) -import Data.Functor.Identity (Identity (..)) -import Data.Hashable (Hashable) -import Data.Proxy (Proxy (..)) -import Data.Semigroup ( All (..) - , Any (..) - , Endo (..) - ) -import Data.Tagged (Tagged (..)) -import Data.Universe.Class (Finite, universe) -import qualified Data.Map as M -import Data.Set (Set) -import qualified Data.Set as Set -import qualified Data.HashMap.Lazy as HM -import qualified Data.HashSet as HS - -import Algebra.Lattice ( BoundedJoinSemiLattice (..) - , BoundedMeetSemiLattice (..) - , BoundedLattice - , Meet (..) - , bottom - , top - , (/\) - , (\/) - ) -import Algebra.Lattice.Dropped (Dropped (..)) -import Algebra.Lattice.Lifted (Lifted (..)) -import Algebra.Lattice.Levitated (Levitated) -import qualified Algebra.Lattice.Levitated as L -import Algebra.Lattice.Ordered (Ordered (..)) -import Algebra.Lattice.Op (Op (..)) -import Algebra.PartialOrd (leq) - --- --- Heyting algebras --- - --- | --- Heyting algebra is a bounded semi-lattice with implication which should --- satisfy the following law: --- --- prop> x ∧ a ≤ b ⇔ x ≤ (a ⇒ b) --- --- We also require that a Heyting algebra is a distributive lattice, which --- means any of the two equivalent conditions holds: --- --- prop> a ∧ (b ∨ c) = a ∧ b ∨ a ∧ c --- prop> a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c) --- --- This means @a ⇒ b@ is an --- [exponential object](https://ncatlab.org/nlab/show/exponential%2Bobject), --- which makes any Heyting algebra --- a [cartesian --- closed category](https://ncatlab.org/nlab/show/cartesian%2Bclosed%2Bcategory). --- This means that Curry isomorphism holds (which takes a form of an actual --- equality): --- --- prop> a ⇒ (b ⇒ c) = (a ∧ b) ⇒ c --- --- Some other useful properties of Heyting algebras: --- --- prop> (a ⇒ b) ∧ a ≤ b --- prop> b ≤ a ⇒ a ∧ b --- prop> a ≤ b iff a ⇒ b = ⊤ --- prop> b ≤ b' then a ⇒ b ≤ a ⇒ b' --- prop> a'≤ a then a' ⇒ b ≤ a ⇒ b --- prop> not (a ∧ b) = not (a ∨ b) --- prop> not (a ∨ b) = not a ∧ not b -class BoundedLattice a => HeytingAlgebra a where - -- | - -- Default implementation: @a ==> b = not a \/ b@, it requires @not@ to - -- satisfy Boolean axioms, which will make it into a Boolean algebra. - -- - -- Fixity is less than fixity of both @'\/'@ and @'/\'@. - (==>) :: a -> a -> a - (==>) a b = not a \/ b - - -- | - -- Default implementation: @not a = a '==>' 'bottom'@ - -- - -- It is useful for optimisation reasons. - not :: a -> a - not a = a ==> bottom - - {-# MINIMAL (==>) | not #-} - -infixr 4 ==> - --- | --- @'implies'@ is an alias for @'==>'@ -implies :: HeytingAlgebra a => a -> a -> a -implies = (==>) - -(<=>) :: HeytingAlgebra a => a -> a -> a -a <=> b = (a ==> b) /\ (b ==> a) - --- | --- @'iff'@ is an alias for @'<=>'@ -iff :: HeytingAlgebra a => a -> a -> a -iff = (<=>) - -iff' :: (Eq a, HeytingAlgebra a) => a -> a -> Bool -iff' a b = Meet top `leq` Meet (iff a b) - --- | --- Every Heyting algebra contains a Boolean algebra. @'toBoolean'@ maps onto it; --- moreover it is a monad (Heyting algebra is a category as every poset is) which --- preserves finite infima. -toBoolean :: HeytingAlgebra a => a -> a -toBoolean = not . not - -instance HeytingAlgebra Bool where - not = Prelude.not - -instance HeytingAlgebra All where - All a ==> All b = All (a ==> b) - not (All a) = All (not a) - -instance HeytingAlgebra Any where - Any a ==> Any b = Any (a ==> b) - not (Any a) = Any (not a) - -instance HeytingAlgebra () where - _ ==> _ = () - -instance HeytingAlgebra (Proxy a) where - _ ==> _ = Proxy - -instance HeytingAlgebra a => HeytingAlgebra (Tagged t a) where - Tagged a ==> Tagged b = Tagged (a ==> b) - -instance HeytingAlgebra b => HeytingAlgebra (a -> b) where - f ==> g = \a -> f a ==> g a - -#if MIN_VERSION_base(4,8,0) -instance HeytingAlgebra a => HeytingAlgebra (Identity a) where - (Identity a) ==> (Identity b) = Identity (a ==> b) -#endif - -instance HeytingAlgebra a => HeytingAlgebra (Const a b) where - (Const a) ==> (Const b) = Const (a ==> b) - -instance HeytingAlgebra a => HeytingAlgebra (Endo a) where - (Endo f) ==> (Endo g) = Endo (f ==> g) - -instance (HeytingAlgebra a, HeytingAlgebra b) => HeytingAlgebra (a, b) where - (a0, b0) ==> (a1, b1) = (a0 ==> a1, b0 ==> b1) - --- --- Dropped, Lifted, Levitated, Ordered --- - --- | --- Subdirectly irreducible Heyting algebra. -instance (Eq a, HeytingAlgebra a) => HeytingAlgebra (Dropped a) where - (Drop a) ==> (Drop b) | Meet a `leq` Meet b = Top - | otherwise = Drop (a ==> b) - Top ==> a = a - _ ==> Top = Top - -instance HeytingAlgebra a => HeytingAlgebra (Lifted a) where - (Lift a) ==> (Lift b) = Lift (a ==> b) - Bottom ==> _ = Lift top - _ ==> Bottom = Bottom - -instance (Eq a, HeytingAlgebra a) => HeytingAlgebra (Levitated a) where - (L.Levitate a) ==> (L.Levitate b) | Meet a `leq` Meet b = L.Top - | otherwise = L.Levitate (a ==> b) - L.Top ==> a = a - _ ==> 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 --- - --- | --- Power set: the canonical example of a Boolean algebra -instance (Ord a, Finite a) => HeytingAlgebra (Set a) where - not a = Set.fromList universe `Set.difference` a - -instance (Eq a, Finite a, Hashable a) => HeytingAlgebra (HS.HashSet a) where - not a = HS.fromList universe `HS.difference` a - --- | --- It is not a boolean algebra (even if values are). -instance (Ord k, Finite k, HeytingAlgebra v) => HeytingAlgebra (M.Map k v) where - -- _xx__ - -- __yy_ - -- T_iTT where i = x ==> y; T = top; _ missing (or removed key) -#if __GLASOW_HASKELL__ >= 804 - a ==> b = - Merge.merge - Merge.dropMissing -- drop if an element is missing in @b@ - (Merge.mapMissing (\_ _ -> top)) -- put @top@ if an element is missing in @a@ - (Merge.zipWithMatched (\_ -> (==>))) -- merge matching elements with @==>@ - a b - - \/ M.fromList [(k, top) | k <- universe, not (M.member k a), not (M.member k b) ] - -- for elements which are not in a, nor in b add - -- a @top@ key -#else - a ==> b = - M.intersectionWith (==>) a b - `M.union` M.map (const top) (M.difference b a) - `M.union` M.fromList [(k, top) | k <- universe, not (M.member k a), not (M.member k b)] -#endif - -instance (Eq k, Finite k, Hashable k, HeytingAlgebra v) => HeytingAlgebra (HM.HashMap k v) where - a ==> b = HM.intersectionWith (==>) a b - `HM.union` HM.map (const top) (HM.difference b a) - `HM.union` HM.fromList [(k, top) | k <- universe, not (HM.member k a), not (HM.member k b)] - --- --- Boolean algebras --- --- They are defined in the same module, to avoid module dependency: @Op a@ is --- a Boolean algebra (thus Heyting algebra in the first place), whenever @a@ is --- a Boolean algebra. --- - --- | --- Boolean algebra is a Heyting algebra which negation satisfies the law of --- excluded middle, i.e. either of the following: --- --- prop> not . not == not --- --- or --- --- prop> x ∨ not x == top --- --- Another characterisation of Boolean algebras is as --- [complemented](https://en.wikipedia.org/wiki/Complemented_lattice) --- [distributive lattices](https://ncatlab.org/nlab/show/distributive+lattice) --- where the complement satisfies the following three properties: --- --- prop> (not a) ∧ a == bottom and (not a) ∨ a == top -- excluded middle law --- prop> not (not a) == a -- involution law --- prop> a ≤ b ⇒ not b ≤ not a -- order-reversing -class HeytingAlgebra a => BooleanAlgebra a - --- --- Instances --- - -instance BooleanAlgebra Bool - -instance BooleanAlgebra All - -instance BooleanAlgebra Any - -instance BooleanAlgebra () - -instance BooleanAlgebra (Proxy a) - -instance BooleanAlgebra a => BooleanAlgebra (Tagged t a) - -instance BooleanAlgebra b => BooleanAlgebra (a -> b) - -#if MIN_VERSION_base(4,8,0) -instance BooleanAlgebra a => BooleanAlgebra (Identity a) -#endif - -instance BooleanAlgebra a => BooleanAlgebra (Const a b) - -instance BooleanAlgebra a => BooleanAlgebra (Endo a) - -instance (BooleanAlgebra a, BooleanAlgebra b) => BooleanAlgebra (a, b) - --- --- containers --- - -instance (Ord a, Finite a) => BooleanAlgebra (Set a) - - --- --- Op --- - --- | Whenever @a@ is a Boolean Algebra, @Op a@ is a Boolean algebra as well, --- which in particular means that it is a Heyting algebra in the first place. --- -instance BooleanAlgebra a => HeytingAlgebra (Op a) where - (Op a) ==> (Op b) = Op (not a /\ b) - --- | Every boolean algebra is isomorphic to power set @P(X)@ of some set @X@; --- then `not :: Op (P(X)) -> P(X)` is a lattice isomorphism, thus `Op (P(X))` is --- a boolean algebra, since @P(X)@ is. -instance BooleanAlgebra a => BooleanAlgebra (Op a) diff --git a/src/Algebra/Heyting/BoolRing.hs b/src/Algebra/Heyting/BoolRing.hs --- a/src/Algebra/Heyting/BoolRing.hs +++ b/src/Algebra/Heyting/BoolRing.hs @@ -5,9 +5,11 @@ , (<+>) ) where -import Prelude hiding (not) +import Prelude +#if __GLASGOW_HASKELL__ < 808 import Data.Monoid (Monoid (..)) +#endif #if __GLASGOW_HASKELL__ < 804 import Data.Semigroup (Semigroup (..)) #endif @@ -31,11 +33,11 @@ newtype BoolRing a = BoolRing { getBoolRing :: a } -- | Sum is [symmetric differnce](https://en.wikipedia.org/wiki/Symmetric_difference). -instance HeytingAlgebra a => Semigroup (BoolRing a) where - (BoolRing a) <> (BoolRing b) = BoolRing $ (not a /\ b) \/ (a /\ not b) +instance Heyting a => Semigroup (BoolRing a) where + (BoolRing a) <> (BoolRing b) = BoolRing $ (neg a /\ b) \/ (a /\ neg b) -- | In a Boolean ring @a + a = 0@, hence @negate = id@. -instance HeytingAlgebra a => Monoid (BoolRing a) where +instance Heyting a => Monoid (BoolRing a) where mempty = BoolRing bottom #if __GLASGOW_HASKELL__ <= 804 @@ -43,6 +45,6 @@ #endif -- | Multiplication is given by @'/\'@ -instance HeytingAlgebra a => Semiring (BoolRing a) where +instance Heyting a => Semiring (BoolRing a) where BoolRing a <.> BoolRing b = BoolRing (a \/ b) one = BoolRing top diff --git a/src/Algebra/Heyting/Free.hs b/src/Algebra/Heyting/Free.hs deleted file mode 100644 --- a/src/Algebra/Heyting/Free.hs +++ /dev/null @@ -1,83 +0,0 @@ -{-# LANGUAGE TypeFamilies #-} -module Algebra.Heyting.Free - ( FreeHeyting (..) - , atom - ) where - -import Prelude hiding (not) - -import Control.Monad (ap) -import Algebra.Lattice ( BoundedJoinSemiLattice (..) - , JoinSemiLattice (..) - , BoundedMeetSemiLattice (..) - , MeetSemiLattice (..) - , BoundedLattice - , Lattice - ) -import Data.Algebra.Free ( AlgebraType0 - , AlgebraType - , FreeAlgebra (..) - , proof - , fmapFree - , bindFree - ) - -import Algebra.Heyting (HeytingAlgebra (..)) - --- | --- Free Heyting algebra. @'FreeAlgebra'@ instance provides all the usual --- combinators for a free algebra. --- --- The --- [graph](https://en.wikipedia.org/wiki/Heyting_algebra#/media/File:Rieger-Nishimura.svg) --- of free Heyting algebra with one generator\/atom, i.e. @'FreeHeyting' ()@. --- -newtype FreeHeyting a = FreeHeyting - { runFreeHeyting :: forall h . HeytingAlgebra h => (a -> h) -> h } - -instance JoinSemiLattice (FreeHeyting a) where - FreeHeyting f \/ FreeHeyting g = FreeHeyting (\inj -> f inj \/ g inj) - -instance BoundedJoinSemiLattice (FreeHeyting a) where - bottom = FreeHeyting (\_ -> bottom) - -instance MeetSemiLattice (FreeHeyting a) where - FreeHeyting f /\ FreeHeyting g = FreeHeyting (\inj -> f inj /\ g inj) - -instance BoundedMeetSemiLattice (FreeHeyting a) where - top = FreeHeyting (\_ -> top) - -instance Lattice (FreeHeyting a) - -instance BoundedLattice (FreeHeyting a) - -instance HeytingAlgebra (FreeHeyting a) where - FreeHeyting f ==> FreeHeyting g = FreeHeyting (\inj -> f inj ==> g inj) - not (FreeHeyting f) = FreeHeyting (\inj -> not (f inj)) - --- | --- Construct an atom of the @'FreeHeyting'@ lattice (in the laguage of free --- algebra, it is called a generator, e.g. @atom = returnFree@). --- -atom :: a -> FreeHeyting a -atom = \a -> FreeHeyting $ \inj -> inj a - -type instance AlgebraType0 FreeHeyting a = () -type instance AlgebraType FreeHeyting a = HeytingAlgebra a -instance FreeAlgebra FreeHeyting where - returnFree = atom - foldMapFree f (FreeHeyting inj) = inj f - - codom = proof - forget = proof - -instance Functor FreeHeyting where - fmap = fmapFree - -instance Applicative FreeHeyting where - pure = returnFree - (<*>) = ap - -instance Monad FreeHeyting where - return = returnFree - (>>=) = bindFree diff --git a/src/Algebra/Heyting/Layered.hs b/src/Algebra/Heyting/Layered.hs --- a/src/Algebra/Heyting/Layered.hs +++ b/src/Algebra/Heyting/Layered.hs @@ -6,14 +6,11 @@ import Prelude import Algebra.Lattice ( BoundedJoinSemiLattice (..) - , JoinSemiLattice (..) , BoundedMeetSemiLattice (..) - , MeetSemiLattice (..) - , BoundedLattice - , Lattice + , Lattice (..) ) -import Algebra.Heyting (HeytingAlgebra (..)) +import Algebra.Heyting ( Heyting (..) ) -- | -- Layer one Heyting algebra on top of the other. Note: this is not @@ -23,38 +20,29 @@ | Upper b deriving (Show, Eq, Ord) -instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (Layered a b) where +instance ( Lattice a + , Lattice b + ) => Lattice (Layered a b) where + l@Lower{} /\ Upper _ = l + Upper _ /\ l@Lower{} = l + Lower l /\ Lower l' = Lower $ l /\ l' + Upper u /\ Upper u' = Upper $ u /\ u' + Lower _ \/ u@Upper{} = u u@Upper{} \/ Lower _ = u Lower l \/ Lower l' = Lower $ l \/ l' Upper u \/ Upper u' = Upper $ u \/ u' -instance (BoundedJoinSemiLattice a, JoinSemiLattice b) => BoundedJoinSemiLattice (Layered a b) where +instance (BoundedJoinSemiLattice a, Lattice b) => BoundedJoinSemiLattice (Layered a b) where bottom = Lower bottom -instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (Layered a b) where - l@Lower{} /\ Upper _ = l - Upper _ /\ l@Lower{} = l - Lower l /\ Lower l' = Lower $ l /\ l' - Upper u /\ Upper u' = Upper $ u /\ u' - -instance (MeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (Layered a b) where +instance (Lattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (Layered a b) where top = Upper top -instance ( Lattice a - , Lattice b - ) => Lattice (Layered a b) - -instance ( Lattice a - , Lattice b - , BoundedJoinSemiLattice a - , BoundedMeetSemiLattice b - ) => BoundedLattice (Layered a b) - -instance ( HeytingAlgebra a - , HeytingAlgebra b +instance ( Heyting a + , Heyting b , Eq a - ) => HeytingAlgebra (Layered a b) where + ) => Heyting (Layered a b) where Lower _ ==> Upper _ = Upper top Upper _ ==> l@Lower{} = l Upper u ==> Upper u' = Upper $ u ==> u' diff --git a/src/Algebra/Heyting/Properties.hs b/src/Algebra/Heyting/Properties.hs --- a/src/Algebra/Heyting/Properties.hs +++ b/src/Algebra/Heyting/Properties.hs @@ -4,10 +4,9 @@ -- module Algebra.Heyting.Properties where -import Prelude hiding (not) +import Prelude import Data.List (intersperse) -import Data.Semigroup ((<>)) import Algebra.Lattice ( Lattice , BoundedJoinSemiLattice @@ -125,13 +124,13 @@ withArgs "x ∧ a ≤ b then x ≤ (a ⇒ b)" [x, a, b] show (HAVNot a b) = - withArgs "a ≤ b ⇏ not a" [a, b] + withArgs "a ≤ b ⇏ neg a" [a, b] show (HAVNotAndMeet a b) = - withArgs "not (a ∧ b) ≠ not a ∨ not b" [a, b] + withArgs "neg (a ∧ b) ≠ neg a ∨ neg b" [a, b] show (HAVNotAndJoin a b) = - withArgs "not (a ∨ b) ≠ not a ∧ not b" [a, b] + withArgs "neg (a ∨ b) ≠ neg a ∧ neg b" [a, b] show (HAVImplicationAndOrd a b) = withArgs "(a ⇒ b) ∧ a ≰ b" [a, b] @@ -144,7 +143,7 @@ -- Verifies the Heyting algebra law for @==>@: -- for all @a@: @_ /\ a@ is left adjoint to @a ==>@ -- and some other properties that are a consequence of that. -prop_implies :: (HeytingAlgebra a, Ord a, Eq a, Show a) +prop_implies :: (Heyting a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) prop_implies x a b = fromBool @@ -155,25 +154,25 @@ (Meet (x /\ a) `leq` Meet b ==> (Meet x `leq` Meet (a ==> b))) /\ fromBool (HAVNot a b) - (Meet a `leq` Meet b ==> (Meet (not b) `leq` Meet (not a))) + (Meet a `leq` Meet b ==> (Meet (neg b) `leq` Meet (neg a))) /\ annotate (HAVNotAndMeet a b) - (not (a /\ b) === (not a \/ not b)) + (neg (a /\ b) === (neg a \/ neg b)) /\ annotate (HAVNotAndJoin a b) - (not (a \/ b) === (not a /\ not b)) + (neg (a \/ b) === (neg a /\ neg b)) /\ fromBool (HAVImplicationAndOrd a a) (Meet ((a ==> b) /\ a) `leq` Meet b) -- | --- Useful for testing valid instances of @'HeytingAlgebra'@ type class. It +-- Useful for testing valid instances of @'Heyting'@ type class. It -- validates: -- -- * bounded lattice laws -- * @'prop_implies'@ prop_HeytingAlgebra - :: (HeytingAlgebra a, Ord a, Eq a, Show a) + :: (Heyting a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) prop_HeytingAlgebra a b c = diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -1,6 +1,9 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE PackageImports #-} +{-# OPTIONS_GHC -Wno-orphans #-} + module Main where import Data.Universe.Class (Universe (..), Finite) @@ -9,12 +12,12 @@ import Data.Map (Map) import qualified Data.Map as Map -import Algebra.Lattice ( JoinSemiLattice - , BoundedJoinSemiLattice - , MeetSemiLattice +import Algebra.Lattice ( BoundedJoinSemiLattice , BoundedMeetSemiLattice - , Lattice - , BoundedLattice + , Lattice (..) + , Meet (..) + , bottom + , top ) import Algebra.Lattice.Dropped (Dropped (..)) import Algebra.Lattice.Lifted (Lifted (..)) @@ -29,9 +32,10 @@ import Algebra.Heyting.CounterExample import Algebra.Heyting.Properties import Algebra.Heyting.Layered +import Algebra.PartialOrd (leq) import Test.Tasty -import Test.Tasty.QuickCheck hiding (Ordered) +import Test.Tasty.QuickCheck hiding (Ordered, (==>)) main :: IO () main = defaultMain tests @@ -42,6 +46,33 @@ -> Property counterExampleProperty = maybe (property True) (flip counterexample False) . fromCounterExample' +-- +-- Orphan instances +-- issue: https://github.com/haskellari/lattices/pull/112 +-- + +instance Heyting a => Heyting (Lifted a) where + (Lift a) ==> (Lift b) = Lift (a ==> b) + Bottom ==> _ = Lift top + _ ==> Bottom = Bottom + +instance (Eq a, Heyting a) => Heyting (Dropped a) where + (Drop a) ==> (Drop b) | Meet a `leq` Meet b = Top + | otherwise = Drop (a ==> b) + Top ==> a = a + _ ==> Top = Top + +instance Boolean a => Heyting (Op a) where + (Op a) ==> (Op b) = Op (neg a /\ b) + +instance (Eq a, Heyting a) => Heyting (Levitated a) where + (L.Levitate a) ==> (L.Levitate b) | Meet a `leq` Meet b = L.Top + | otherwise = L.Levitate (a ==> b) + L.Top ==> a = a + _ ==> L.Top = L.Top + L.Bottom ==> _ = L.Top + _ ==> L.Bottom = L.Bottom + -- -- List of tast cases -- @@ -51,7 +82,6 @@ testGroup "heyting-algebras tests" [ testGroup "Boolean algebras" [ testProperty "Bool" prop_boolean_Bool - , testProperty "(Bool, Bool)" prop_boolean_BoolBool , testProperty "Boolean (Lifted Bool)" prop_boolean_LiftedBool , testProperty "Boolean (Dropped Bool)" prop_boolean_DroppedBool , testProperty "(Set S5)" prop_boolean_Set @@ -68,12 +98,10 @@ , testProperty "Levitated Bool" prop_heyting_LevitatedBool , testProperty "Sum (Lifted Bool) (Dropped Bool)" prop_heyting_LayeredLiftedDropped , testProperty "Levitated (Ordered Int)" prop_heyting_LevitatedOrderedInt - , testProperty "Map S5 Bool" prop_heyting_MapS5Bool , testProperty "Dropped (Lifted Bool)" prop_heyting_DroppedLiftedBool , testProperty "Lifted (Dropped Bool)" prop_heyting_LiftedDroppedBool , testProperty "Lifted (Lifted Bool)" prop_heyting_LiftedLiftedBool , testProperty "Dropped (Dropped Bool)" prop_heyting_DroppedDroppedBool - , testProperty "CounterExample" prop_heyting_CounterExample ] ] @@ -88,18 +116,13 @@ prop_boolean_Bool = (fmap . fmap) counterExampleProperty . prop_BooleanAlgebra -prop_boolean_BoolBool - :: BooleanProp (Bool, Bool) -prop_boolean_BoolBool = - (fmap . fmap) counterExampleProperty . prop_BooleanAlgebra - prop_boolean_LiftedBool - :: BooleanProp (Arb (Boolean (Arb (Lifted Bool)))) + :: BooleanProp (Arb (BooleanAlgebra (Arb (Lifted Bool)))) prop_boolean_LiftedBool = (fmap . fmap) counterExampleProperty . prop_BooleanAlgebra prop_boolean_DroppedBool - :: BooleanProp (Arb (Boolean (Arb (Dropped Bool)))) + :: BooleanProp (Arb (BooleanAlgebra (Arb (Dropped Bool)))) prop_boolean_DroppedBool = (fmap . fmap) counterExampleProperty . prop_BooleanAlgebra @@ -119,21 +142,21 @@ prop_non_boolean_LiftedBool = expectFailure . counterExampleProperty @String - . prop_not + . prop_neg prop_non_boolean_DroppedBool :: NonBooleanProp (Arb (Dropped Bool)) prop_non_boolean_DroppedBool = expectFailure . counterExampleProperty @String - . prop_not + . prop_neg prop_non_boolean_LevitatedOrderedInt :: NonBooleanProp (Arb (Levitated (Arb (Ordered Int)))) prop_non_boolean_LevitatedOrderedInt = expectFailure . counterExampleProperty @String - . prop_not + . prop_neg -- -- Heyting algebra tests @@ -171,11 +194,6 @@ prop_heyting_LevitatedOrderedInt = (fmap . fmap) counterExampleProperty . prop_HeytingAlgebra -prop_heyting_MapS5Bool - :: HeytingProp (Arb (Map S5 Bool)) -prop_heyting_MapS5Bool = - (fmap . fmap) counterExampleProperty . prop_HeytingAlgebra - prop_heyting_DroppedLiftedBool :: HeytingProp (Composed Dropped Lifted Bool) prop_heyting_DroppedLiftedBool = @@ -196,22 +214,15 @@ prop_heyting_DroppedDroppedBool = (fmap . fmap) counterExampleProperty . prop_HeytingAlgebra -prop_heyting_CounterExample - :: HeytingProp (Composed Lifted Op (Set S5)) -prop_heyting_CounterExample = - (fmap . fmap) counterExampleProperty . prop_HeytingAlgebra -- | Arbitrary wrapper for varous lattices. -- newtype Arb a = Arb a - deriving ( JoinSemiLattice - , BoundedJoinSemiLattice - , MeetSemiLattice + deriving ( BoundedJoinSemiLattice , BoundedMeetSemiLattice , Lattice - , BoundedLattice - , BooleanAlgebra - , HeytingAlgebra + , Boolean + , Heyting , Eq , Ord ) @@ -252,9 +263,9 @@ : [ Arb (L.Levitate a') | a' <- shrink a ] shrink (Arb L.Top) = [] -instance (Arbitrary a, HeytingAlgebra a, Eq a) => Arbitrary (Arb (Boolean a)) where +instance (Arbitrary a, Heyting a, Eq a) => Arbitrary (Arb (BooleanAlgebra a)) where arbitrary = Arb . boolean <$> arbitrary - shrink (Arb a) = filter (/= Arb a) (Arb . boolean <$> shrink (runBoolean a)) + shrink (Arb a) = filter (/= Arb a) (Arb . boolean <$> shrink (runBooleanAlgebra a)) instance Arbitrary a => Arbitrary (Arb (Ordered a)) where @@ -287,14 +298,11 @@ -- | Arbitrary newtype wrapper for compositions of heigher kinded types. -- newtype Composed f g a = Composed (f (g a)) - deriving ( JoinSemiLattice - , BoundedJoinSemiLattice - , MeetSemiLattice + deriving ( BoundedJoinSemiLattice , BoundedMeetSemiLattice , Lattice - , BoundedLattice - , BooleanAlgebra - , HeytingAlgebra + , Boolean + , Heyting , Eq , Ord )