```{-# 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)
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)
```