{-# LANGUAGE CPP #-}
module Algebra.Heyting
( HeytingAlgebra (..)
, iff
, iff'
, toBoolean
, prop_BoundedMeetSemiLattice
, prop_BoundedJoinSemiLattice
, prop_HeytingAlgebra
, prop_implies
)
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
#if __GLASGOW_HASKELL__ >= 822
import qualified Data.Map.Merge.Lazy as Merge
#endif
import qualified Data.Set as S
import qualified Data.HashMap.Lazy as HM
import qualified Data.HashSet as HS
import Algebra.Lattice ( BoundedJoinSemiLattice (..)
, BoundedMeetSemiLattice (..)
, BoundedLattice
, Meet (..)
, Join (..)
, (/\)
, (\/)
)
import Algebra.Lattice.Dropped (Dropped (..))
import Algebra.Lattice.Lifted (Lifted (..))
import Algebra.Lattice.Levitated (Levitated)
import qualified Algebra.Lattice.Levitated as L
import Algebra.PartialOrd (leq)
#ifdef EXPORT_PROPERTIES
import Test.QuickCheck hiding ((==>))
import qualified Test.QuickCheck as QC
#endif
class BoundedLattice a => HeytingAlgebra a where
(==>) :: a -> a -> a
(==>) a b = not a \/ b
not :: a -> a
not a = a ==> bottom
{-# MINIMAL (==>) | not #-}
infixr 4 ==>
iff :: HeytingAlgebra a => a -> a -> a
iff a b = (a ==> b) /\ (b ==> a)
iff' :: (Eq a, HeytingAlgebra a) => a -> a -> Bool
iff' a b = Meet top `leq` Meet (iff a b)
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
instance HeytingAlgebra a => HeytingAlgebra (Identity a) where
(Identity a) ==> (Identity b) = Identity (a ==> b)
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)
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, Finite a) => HeytingAlgebra (S.Set a) where
not a = S.fromList universe `S.difference` a
instance (Eq a, Finite a, Hashable a) => HeytingAlgebra (HS.HashSet a) where
not a = HS.fromList universe `HS.difference` a
instance (Ord k, Finite k, HeytingAlgebra v) => HeytingAlgebra (M.Map k v) where
#if __GLASOW_HASKELL__ >= 822
a ==> b =
Merge.merge
Merge.dropMissing
(Merge.mapMissing (\_ _ -> top))
(Merge.zipWithMatched (\_ -> (==>)))
a b
\/ M.fromList [(k, top) | k <- universe, not (M.member k a), not (M.member k b) ]
#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)]
#ifdef EXPORT_PROPERTIES
prop_BoundedMeetSemiLattice :: (BoundedMeetSemiLattice a, Eq a, Show a)
=> a -> a -> a -> Property
prop_BoundedMeetSemiLattice a b c =
counterexample "meet associativity" ((a /\ (b /\ c)) === ((a /\ b) /\ c))
.&&. counterexample "meet commutativity" ((a /\ b) === (b /\ a))
.&&. counterexample "meet idempotent" ((a /\ a) === a)
.&&. counterexample "meet identity" ((top /\ a) === a)
.&&. counterexample "meet order" (Meet (a /\ b) `leq` Meet a)
prop_BoundedJoinSemiLattice :: (BoundedJoinSemiLattice a, Eq a, Show a) => a -> a -> a -> Property
prop_BoundedJoinSemiLattice a b c =
counterexample "join associativity" ((a \/ (b \/ c)) === ((a \/ b) \/ c))
.&&. counterexample "join commutativity" ((a \/ b) === (b \/ a))
.&&. counterexample "join idempotent" ((a \/ a) === a)
.&&. counterexample "join identity" ((bottom \/ a) === a)
.&&. counterexample "join order" (Join a `leq` Join (a \/ b))
prop_implies :: (HeytingAlgebra a, Eq a, Show a)
=> a -> a -> a -> Property
prop_implies x a b =
counterexample ("Failed: x ≤ (a ⇒ b) then x ∧ a ≤ b\n\ta ⇒ b = " ++ show (a ==> b))
(Meet x `leq` Meet (a ==> b) QC.==> (Meet (x /\ a) `leq` Meet b))
.&&.
counterexample ("Failed: x ∧ a ≤ b then x ≤ (a ⇒ b)\n\ta ⇒ b = " ++ show (a ==> b))
(Meet (x /\ a) `leq` Meet b QC.==> (Meet x `leq` Meet (a ==> b)))
prop_HeytingAlgebra :: (HeytingAlgebra a, Eq a, Show a)
=> a -> a -> a -> Property
prop_HeytingAlgebra a b c =
prop_BoundedJoinSemiLattice a b c
.&&. prop_BoundedMeetSemiLattice a b c
.&&. prop_implies a b c
#endif