{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- | Lattices & algebras
module Data.Lattice (
    -- * Semilattice
    Lattice,
    Semilattice (..),

    -- ** Meet
    Meet,
    (/\),
    top,

    -- ** Join
    Join,
    (\/),
    bottom,

    -- * Algebra
    Biheyting,
    Algebra (..),

    -- ** Heyting
    Heyting,
    (//),
    iff,
    neg,
    middle,
    heyting,
    booleanR,

    -- ** Coheyting
    Coheyting,
    (\\),
    equiv,
    non,
    boundary,
    coheyting,
    booleanL,

    -- ** Symmetric
    Symmetric (..),
    converseL,
    converseR,
    symmetricL,
    symmetricR,

    -- ** Boolean
    Boolean (..),
) where

import safe Data.Bifunctor (bimap)
import safe Data.Bool hiding (not)
import safe Data.Connection.Class
import safe Data.Connection.Conn
import safe Data.Either
import safe Data.Int
import safe qualified Data.IntMap as IntMap
import safe qualified Data.IntSet as IntSet
import safe qualified Data.Map as Map
import safe Data.Order
import safe Data.Order.Extended
import safe Data.Order.Syntax
import safe qualified Data.Set as Set
import safe Data.Word
import safe Prelude hiding (Eq (..), Ord (..), not)
import safe qualified Prelude as P

-------------------------------------------------------------------------------
-- Lattices
-------------------------------------------------------------------------------

type Lattice a = (Join a, Meet a)

-- | A convenience alias for a join semilattice
type Join = Semilattice 'L

-- | A convenience alias for a meet semilattice
type Meet = Semilattice 'R

-- | Bounded < https://ncatlab.org/nlab/show/lattice lattices >.
--
-- A lattice is a partially ordered set in which every two elements have a unique join
-- (least upper bound or supremum) and a unique meet (greatest lower bound or infimum).
--
-- A bounded lattice adds unique elements 'top' and 'bottom', which serve as
-- identities to '\/' and '/\', respectively.
--
-- /Neutrality/:
--
-- @
-- x '\/' 'bottom' = x
-- x '/\' 'top' = x
-- 'glb' 'bottom' x 'top' = x
-- 'lub' 'bottom' x 'top' = x
-- @
--
-- /Associativity/
--
-- @
-- x '\/' (y '\/' z) = (x '\/' y) '\/' z
-- x '/\' (y '/\' z) = (x '/\' y) '/\' z
-- @
--
-- /Commutativity/
--
-- @
-- x '\/' y = y '\/' x
-- x '/\' y = y '/\' x
-- @
--
-- /Idempotency/
--
-- @
-- x '\/' x = x
-- x '/\' x = x
-- @
--
-- /Absorption/
--
-- @
-- (x '\/' y) '/\' y = y
-- (x '/\' y) '\/' y = y
-- @
--
-- See < https://en.wikipedia.org/wiki/Absorption_law Absorption >.
--
-- Note that distributivity is _not_ a requirement for a complete.
-- However when /a/ is distributive we have:
--
-- @
-- 'glb' x y z = 'lub' x y z
-- @
--
-- See < https://en.wikipedia.org/wiki/Lattice_(order) >.
class Order a => Semilattice (k :: Kan) a where
    -- | The defining connection of a bounded semilattice.
    --
    -- 'bottom' and 'top' are defined by the left and right adjoints to /a -> ()/.
    bounded :: Conn k () a
    default bounded :: Connection k () a => Conn k () a
    bounded = Conn k () a
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

    -- | The defining connection of a semilattice.
    --
    -- '\/' and '/\' are defined by the left and right adjoints to /a -> (a, a)/.
    semilattice :: Conn k (a, a) a
    default semilattice :: Connection k (a, a) a => Conn k (a, a) a
    semilattice = Conn k (a, a) a
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

infixr 6 /\ -- comment for the parser

-- | Lattice meet.
--
-- > (/\) = curry $ floorWith semilattice
(/\) :: Meet a => a -> a -> a
/\ :: a -> a -> a
(/\) = ((a, a) -> a) -> a -> a -> a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((a, a) -> a) -> a -> a -> a) -> ((a, a) -> a) -> a -> a -> a
forall a b. (a -> b) -> a -> b
$ ConnR (a, a) a -> (a, a) -> a
forall a b. ConnR a b -> a -> b
floorWith ConnR (a, a) a
forall (k :: Kan) a. Semilattice k a => Conn k (a, a) a
semilattice

-- | The unique top element of a bounded lattice
--
-- > x /\ top = x
-- > x \/ top = top
top :: Meet a => a
top :: a
top = ConnR () a -> () -> a
forall a b. ConnR a b -> a -> b
floorWith ConnR () a
forall (k :: Kan) a. Semilattice k a => Conn k () a
bounded ()

infixr 5 \/

-- | Lattice join.
--
-- > (\/) = curry $ ceilingWith semilattice
(\/) :: Join a => a -> a -> a
\/ :: a -> a -> a
(\/) = ((a, a) -> a) -> a -> a -> a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((a, a) -> a) -> a -> a -> a) -> ((a, a) -> a) -> a -> a -> a
forall a b. (a -> b) -> a -> b
$ ConnL (a, a) a -> (a, a) -> a
forall a b. ConnL a b -> a -> b
ceilingWith ConnL (a, a) a
forall (k :: Kan) a. Semilattice k a => Conn k (a, a) a
semilattice

-- | The unique bottom element of a bounded lattice
--
-- > x /\ bottom = bottom
-- > x \/ bottom = x
bottom :: Join a => a
bottom :: a
bottom = ConnL () a -> () -> a
forall a b. ConnL a b -> a -> b
ceilingWith ConnL () a
forall (k :: Kan) a. Semilattice k a => Conn k () a
bounded ()

-------------------------------------------------------------------------------
-- Heyting algebras
-------------------------------------------------------------------------------

-- | A convenience alias for a Heyting algebra.
type Heyting a = (Lattice a, Algebra 'R a)

-- | A convenience alias for a < https://ncatlab.org/nlab/show/co-Heyting+algebra co-Heyting algebra >.
type Coheyting a = (Lattice a, Algebra 'L a)

-- | A < https://ncatlab.org/nlab/show/co-Heyting+algebra bi-Heyting algebra >.
--
-- /Laws/:
--
-- > neg x <= non x
--
-- with equality occurring iff /a/ is a 'Boolean' algebra.
type Biheyting a = (Coheyting a, Heyting a)

-- | Heyting and co-Heyting algebras
--
-- A Heyting algebra is a bounded, distributive lattice equipped with an
-- implication operation.
--
-- * The complete of closed subsets of a topological space is the primordial
-- example of a /Coheyting/ (co-Algebra) algebra.
--
-- * The dual complete of open subsets of a topological space is likewise
-- the primordial example of a /Heyting/ algebra.
--
-- /Coheyting/:
--
-- Co-implication to /a/ is the lower adjoint of disjunction with /a/:
--
-- > x \\ a <= y <=> x <= y \/ a
--
-- Note that co-Heyting algebras needn't obey the law of non-contradiction:
--
-- > EQ /\ non EQ = EQ /\ GT \\ EQ = EQ /\ GT = EQ /= LT
--
-- See < https://ncatlab.org/nlab/show/co-Algebra+algebra >
--
-- /Heyting/:
--
-- Implication from /a/ is the upper adjoint of conjunction with /a/:
--
-- > x <= a // y <=> a /\ x <= y
--
-- Similarly, Heyting algebras needn't obey the law of the excluded middle:
--
-- > EQ \/ neg EQ = EQ \/ EQ // LT = EQ \/ LT = EQ /= GT
--
-- See < https://ncatlab.org/nlab/show/Heyting+algebra >
class Semilattice k a => Algebra k a where
    -- | The defining connection of a (co-)Heyting algebra.
    --
    -- > algebra @'L x = ConnL (\\ x) (\/ x)
    -- > algebra @'R x = ConnR (x /\) (x //)
    algebra :: a -> Conn k a a

-------------------------------------------------------------------------------
-- Heyting
-------------------------------------------------------------------------------

infixr 8 // -- same as ^

-- | Logical implication:
--
-- \( a \Rightarrow b = \vee \{x \mid x \wedge a \leq b \} \)
--
-- /Laws/:
--
-- > x /\ y <= z <=> x <= y // z
-- > x // y <= x // (y \/ z)
-- > x <= y => z // x <= z // y
-- > y <= x // (x /\ y)
-- > x <= y <=> x // y = top
-- > (x \/ z) // y <= x // y
-- > (x /\ y) // z = x // y // z
-- > x // (y /\ z) = x // y /\ x // z
-- > x /\ x // y = x /\ y
--
-- >>> False // False
-- True
-- >>> False // True
-- True
-- >>> True // False
-- False
-- >>> True // True
-- True
(//) :: Algebra 'R a => a -> a -> a
// :: a -> a -> a
(//) = ConnR a a -> a -> a
forall a b. ConnR a b -> a -> b
floorWith (ConnR a a -> a -> a) -> (a -> ConnR a a) -> a -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ConnR a a
forall (k :: Kan) a. Algebra k a => a -> Conn k a a
algebra

-- | Intuitionistic equivalence.
--
-- When @a@ is /Bool/ this is 'if-and-only-if'.
iff :: Algebra 'R a => a -> a -> a
iff :: a -> a -> a
iff a
x a
y = (a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
y) a -> a -> a
forall a. Meet a => a -> a -> a
/\ (a
y a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
x)

-- | Logical negation.
--
-- @ 'neg' x = x '//' 'bottom' @
--
-- /Laws/:
--
-- > neg bottom = top
-- > neg top = bottom
-- > x <= neg (neg x)
-- > neg (x \/ y) <= neg x
-- > neg (x // y) = neg (neg x) /\ neg y
-- > neg (x \/ y) = neg x /\ neg y
-- > x /\ neg x = bottom
-- > neg (neg (neg x)) = neg x
-- > neg (neg (x \/ neg x)) = top
--
-- Some logics may in addition obey < https://ncatlab.org/nlab/show/De+Morgan+Algebra+algebra De Morgan conditions >.
neg :: Heyting a => a -> a
neg :: a -> a
neg a
x = a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
forall a. Join a => a
bottom

-- | The Algebra (< https://ncatlab.org/nlab/show/excluded+middle not necessarily excluded>) middle operator.
middle :: Heyting a => a -> a
middle :: a -> a
middle a
x = a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a -> a
forall a. Heyting a => a -> a
neg a
x

-- | Default constructor for a Algebra algebra.
heyting :: Meet a => (a -> a -> a) -> a -> ConnR a a
heyting :: (a -> a -> a) -> a -> ConnR a a
heyting a -> a -> a
f a
a = (a -> a) -> (a -> a) -> ConnR a a
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR (a
a a -> a -> a
forall a. Meet a => a -> a -> a
/\) (a
a a -> a -> a
`f`)

-- | An adjunction between a Algebra algebra and its Boolean sub-algebra.
--
-- Double negation is a meet-preserving monad.
booleanR :: Heyting a => ConnR a a
booleanR :: ConnR a a
booleanR =
    let -- Check that /x/ is a regular element
        -- See https://ncatlab.org/nlab/show/regular+element
        inj :: p -> p
inj p
x = if p
x p -> p -> Bool
forall a. Preorder a => a -> a -> Bool
~~ (p -> p
forall a. Heyting a => a -> a
neg (p -> p) -> (p -> p) -> p -> p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p -> p
forall a. Heyting a => a -> a
neg) p
x then p
x else p
forall a. Join a => a
bottom
     in (a -> a) -> (a -> a) -> ConnR a a
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR (a -> a
forall a. Heyting a => a -> a
neg (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Heyting a => a -> a
neg) a -> a
forall p. (Semilattice 'L p, Algebra 'R p) => p -> p
inj

-------------------------------------------------------------------------------
-- Coheyting
-------------------------------------------------------------------------------

infixl 8 \\

-- | Logical co-implication:
--
-- \( a \Rightarrow b = \wedge \{x \mid a \leq b \vee x \} \)
--
-- /Laws/:
--
-- > x \\ y <= z <=> x <= y \/ z
-- > x \\ y >= (x /\ z) \\ y
-- > x >= y => x \\ z >= y \\ z
-- > x >= x \\ y
-- > x >= y <=> y \\ x = bottom
-- > x \\ (y /\ z) >= x \\ y
-- > z \\ (x \/ y) = z \\ x \\ y
-- > (y \/ z) \\ x = y \\ x \/ z \\ x
-- > x \/ y \\ x = x \/ y
--
-- >>> False \\ False
-- False
-- >>> False \\ True
-- False
-- >>> True \\ False
-- True
-- >>> True \\ True
-- False
--
-- For many collections (e.g. 'Data.Set.Set') '\\' coincides with the native 'Data.Set.\\' operator.
--
-- >>> :set -XOverloadedLists
-- >>> [GT,EQ] Set.\\ [LT]
-- fromList [EQ,GT]
-- >>> [GT,EQ] \\ [LT]
-- fromList [EQ,GT]
(\\) :: Algebra 'L a => a -> a -> a
\\ :: a -> a -> a
(\\) = (a -> a -> a) -> a -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> a -> a) -> a -> a -> a) -> (a -> a -> a) -> a -> a -> a
forall a b. (a -> b) -> a -> b
$ ConnL a a -> a -> a
forall a b. ConnL a b -> a -> b
ceilingWith (ConnL a a -> a -> a) -> (a -> ConnL a a) -> a -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ConnL a a
forall (k :: Kan) a. Algebra k a => a -> Conn k a a
algebra

-- | Intuitionistic co-equivalence.
equiv :: Algebra 'L a => a -> a -> a
equiv :: a -> a -> a
equiv a
x a
y = (a
x a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
y) a -> a -> a
forall a. Join a => a -> a -> a
\/ (a
y a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
x)

-- | Logical < https://ncatlab.org/nlab/show/co-Heyting+negation co-negation >.
--
-- @ 'non' x = 'top' '\\' x @
--
-- /Laws/:
--
-- > non bottom = top
-- > non top = bottom
-- > x >= non (non x)
-- > non (x /\ y) >= non x
-- > non (y \\ x) = non (non x) \/ non y
-- > non (x /\ y) = non x \/ non y
-- > x \/ non x = top
-- > non (non (non x)) = non x
-- > non (non (x /\ non x)) = bottom
non :: Coheyting a => a -> a
non :: a -> a
non a
x = a
forall a. Meet a => a
top a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a
x

-- | The co-Heyting < https://ncatlab.org/nlab/show/co-Heyting+boundary boundary > operator.
--
-- > x = boundary x \/ (non . non) x
-- > boundary (x /\ y) = (boundary x /\ y) \/ (x /\ boundary y)  -- (Leibniz rule)
-- > boundary (x \/ y) \/ boundary (x /\ y) = boundary x \/ boundary y
boundary :: Coheyting a => a -> a
boundary :: a -> a
boundary a
x = a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Coheyting a => a -> a
non a
x

-- | Default constructor for a co-Heyting algebra.
coheyting :: Join a => (a -> a -> a) -> a -> ConnL a a
coheyting :: (a -> a -> a) -> a -> ConnL a a
coheyting a -> a -> a
f a
a = (a -> a) -> (a -> a) -> ConnL a a
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (a -> a -> a
`f` a
a) (a -> a -> a
forall a. Join a => a -> a -> a
\/ a
a)

-- | An adjunction between a co-Heyting algebra and its Boolean sub-algebra.
--
-- Double negation is a join-preserving comonad.
booleanL :: Coheyting a => ConnL a a
booleanL :: ConnL a a
booleanL =
    let -- Check that /x/ is a regular element
        -- See https://ncatlab.org/nlab/show/regular+element
        inj :: p -> p
inj p
x = if p
x p -> p -> Bool
forall a. Preorder a => a -> a -> Bool
~~ (p -> p
forall a. Coheyting a => a -> a
non (p -> p) -> (p -> p) -> p -> p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p -> p
forall a. Coheyting a => a -> a
non) p
x then p
x else p
forall a. Meet a => a
top
     in (a -> a) -> (a -> a) -> ConnL a a
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL a -> a
forall p. (Semilattice 'R p, Algebra 'L p) => p -> p
inj (a -> a
forall a. Coheyting a => a -> a
non (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Coheyting a => a -> a
non)

-------------------------------------------------------------------------------
-- Symmetric
-------------------------------------------------------------------------------

-- | Symmetric Heyting algebras
--
-- A symmetric Heyting algebra is a <https://ncatlab.org/nlab/show/De+Morgan+Algebra+algebra De Morgan >
-- bi-Algebra algebra with an idempotent, antitone negation operator.
--
-- /Laws/:
--
-- > x <= y => not y <= not x -- antitone
-- > not . not = id           -- idempotence
-- > x \\ y = not (not y // not x)
-- > x // y = not (not y \\ not x)
--
-- and:
--
-- > converseR x <= converseL x
--
-- with equality occurring iff /a/ is a 'Boolean' algebra.
class Biheyting a => Symmetric a where
    -- | Symmetric negation.
    --
    -- > not . not = id
    -- > neg . neg = converseR . converseL
    -- > non . non = converseL . converseR
    -- > neg . non = converseR . converseR
    -- > non . neg = converseL . converseL
    --
    -- > neg = converseR . not = not . converseL
    -- > non = not . converseR = converseL . not
    -- > x \\ y = not (not y // not x)
    -- > x // y = not (not y \\ not x)
    not :: a -> a

    infixl 4 `xor`

    -- | Exclusive or.
    --
    -- > xor x y = (x \/ y) /\ (not x \/ not y)
    xor :: a -> a -> a
    xor a
x a
y = (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y) a -> a -> a
forall a. Meet a => a -> a -> a
/\ a -> a
forall a. Symmetric a => a -> a
not (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y)

-- | Left converse operator.
converseL :: Symmetric a => a -> a
converseL :: a -> a
converseL a
x = a
forall a. Meet a => a
top a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a -> a
forall a. Symmetric a => a -> a
not a
x

-- | Right converse operator.
converseR :: Symmetric a => a -> a
converseR :: a -> a
converseR a
x = a -> a
forall a. Symmetric a => a -> a
not a
x a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
forall a. Join a => a
bottom

-- | Default constructor for a Heyting algebra.
symmetricR :: Symmetric a => a -> ConnR a a
symmetricR :: a -> ConnR a a
symmetricR = (a -> a -> a) -> a -> ConnR a a
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting ((a -> a -> a) -> a -> ConnR a a)
-> (a -> a -> a) -> a -> ConnR a a
forall a b. (a -> b) -> a -> b
$ \a
x a
y -> a -> a
forall a. Symmetric a => a -> a
not (a -> a
forall a. Symmetric a => a -> a
not a
y a -> a -> a
forall a. Algebra 'L a => a -> a -> a
\\ a -> a
forall a. Symmetric a => a -> a
not a
x)

-- | Default constructor for a co-Heyting algebra.
symmetricL :: Symmetric a => a -> ConnL a a
symmetricL :: a -> ConnL a a
symmetricL = (a -> a -> a) -> a -> ConnL a a
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting ((a -> a -> a) -> a -> ConnL a a)
-> (a -> a -> a) -> a -> ConnL a a
forall a b. (a -> b) -> a -> b
$ \a
x a
y -> a -> a
forall a. Symmetric a => a -> a
not (a -> a
forall a. Symmetric a => a -> a
not a
y a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a -> a
forall a. Symmetric a => a -> a
not a
x)

-------------------------------------------------------------------------------
-- Boolean
-------------------------------------------------------------------------------

-- | Boolean algebras.
--
-- < https://ncatlab.org/nlab/show/Boolean+algebra Boolean algebras > are
-- symmetric Algebra algebras that satisfy both the law of excluded middle
-- and the law of law of non-contradiction:
--
-- > x \/ neg x = top
-- > x /\ non x = bottom
--
-- If /a/ is Boolean we also have:
--
-- > non = not = neg
class Symmetric a => Boolean a where
    -- | A witness to the lawfulness of a boolean algebra.
    boolean :: Conn k a a
    boolean = (a -> a) -> (a -> a) -> (a -> a) -> Conn k a a
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (a -> a
forall a. Symmetric a => a -> a
converseR (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Symmetric a => a -> a
converseL) a -> a
forall a. a -> a
id (a -> a
forall a. Symmetric a => a -> a
converseL (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Symmetric a => a -> a
converseR)

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

instance Semilattice k ()
instance Algebra 'L () where algebra :: () -> Conn 'L () ()
algebra = (() -> () -> ()) -> () -> Conn 'L () ()
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting () -> () -> ()
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R () where algebra :: () -> Conn 'R () ()
algebra = (() -> () -> ()) -> () -> Conn 'R () ()
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting () -> () -> ()
forall a. (Total a, Bounded a) => a -> a -> a
impliesR
instance Symmetric () where not :: () -> ()
not = () -> ()
forall a. a -> a
id
instance Boolean ()

instance Semilattice k Bool
instance Algebra 'L Bool where algebra :: Bool -> Conn 'L Bool Bool
algebra = (Bool -> Bool -> Bool) -> Bool -> Conn 'L Bool Bool
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Bool -> Bool -> Bool
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Bool where algebra :: Bool -> Conn 'R Bool Bool
algebra = (Bool -> Bool -> Bool) -> Bool -> Conn 'R Bool Bool
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Bool -> Bool -> Bool
forall a. (Total a, Bounded a) => a -> a -> a
impliesR
instance Symmetric Bool where not :: Bool -> Bool
not = Bool -> Bool
P.not
instance Boolean Bool

instance Semilattice k Ordering
instance Algebra 'L Ordering where algebra :: Ordering -> Conn 'L Ordering Ordering
algebra = (Ordering -> Ordering -> Ordering)
-> Ordering -> Conn 'L Ordering Ordering
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Ordering -> Ordering -> Ordering
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Ordering where algebra :: Ordering -> Conn 'R Ordering Ordering
algebra = (Ordering -> Ordering -> Ordering)
-> Ordering -> Conn 'R Ordering Ordering
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Ordering -> Ordering -> Ordering
forall a. (Total a, Bounded a) => a -> a -> a
impliesR
instance Symmetric Ordering where
    not :: Ordering -> Ordering
not Ordering
LT = Ordering
GT
    not Ordering
EQ = Ordering
EQ
    not Ordering
GT = Ordering
LT
instance Boolean Ordering

instance Semilattice k Word8
instance Algebra 'L Word8 where algebra :: Word8 -> Conn 'L Word8 Word8
algebra = (Word8 -> Word8 -> Word8) -> Word8 -> Conn 'L Word8 Word8
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Word8 -> Word8 -> Word8
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Word8 where algebra :: Word8 -> Conn 'R Word8 Word8
algebra = (Word8 -> Word8 -> Word8) -> Word8 -> Conn 'R Word8 Word8
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Word8 -> Word8 -> Word8
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

instance Semilattice k Word16
instance Algebra 'L Word16 where algebra :: Word16 -> Conn 'L Word16 Word16
algebra = (Word16 -> Word16 -> Word16) -> Word16 -> Conn 'L Word16 Word16
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Word16 -> Word16 -> Word16
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Word16 where algebra :: Word16 -> Conn 'R Word16 Word16
algebra = (Word16 -> Word16 -> Word16) -> Word16 -> Conn 'R Word16 Word16
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Word16 -> Word16 -> Word16
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

instance Semilattice k Word32
instance Algebra 'L Word32 where algebra :: Word32 -> Conn 'L Word32 Word32
algebra = (Word32 -> Word32 -> Word32) -> Word32 -> Conn 'L Word32 Word32
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Word32 -> Word32 -> Word32
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Word32 where algebra :: Word32 -> Conn 'R Word32 Word32
algebra = (Word32 -> Word32 -> Word32) -> Word32 -> Conn 'R Word32 Word32
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Word32 -> Word32 -> Word32
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

instance Semilattice k Word64
instance Algebra 'L Word64 where algebra :: Word64 -> Conn 'L Word64 Word64
algebra = (Word64 -> Word64 -> Word64) -> Word64 -> Conn 'L Word64 Word64
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Word64 -> Word64 -> Word64
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Word64 where algebra :: Word64 -> Conn 'R Word64 Word64
algebra = (Word64 -> Word64 -> Word64) -> Word64 -> Conn 'R Word64 Word64
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Word64 -> Word64 -> Word64
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

instance Semilattice k Word
instance Algebra 'L Word where algebra :: Word -> Conn 'L Word Word
algebra = (Word -> Word -> Word) -> Word -> Conn 'L Word Word
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Word -> Word -> Word
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Word where algebra :: Word -> Conn 'R Word Word
algebra = (Word -> Word -> Word) -> Word -> Conn 'R Word Word
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Word -> Word -> Word
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

instance Semilattice k Int8
instance Algebra 'L Int8 where algebra :: Int8 -> Conn 'L Int8 Int8
algebra = (Int8 -> Int8 -> Int8) -> Int8 -> Conn 'L Int8 Int8
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Int8 -> Int8 -> Int8
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Int8 where algebra :: Int8 -> Conn 'R Int8 Int8
algebra = (Int8 -> Int8 -> Int8) -> Int8 -> Conn 'R Int8 Int8
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Int8 -> Int8 -> Int8
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

instance Semilattice k Int16
instance Algebra 'L Int16 where algebra :: Int16 -> Conn 'L Int16 Int16
algebra = (Int16 -> Int16 -> Int16) -> Int16 -> Conn 'L Int16 Int16
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Int16 -> Int16 -> Int16
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Int16 where algebra :: Int16 -> Conn 'R Int16 Int16
algebra = (Int16 -> Int16 -> Int16) -> Int16 -> Conn 'R Int16 Int16
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Int16 -> Int16 -> Int16
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

instance Semilattice k Int32
instance Algebra 'L Int32 where algebra :: Int32 -> Conn 'L Int32 Int32
algebra = (Int32 -> Int32 -> Int32) -> Int32 -> Conn 'L Int32 Int32
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Int32 -> Int32 -> Int32
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Int32 where algebra :: Int32 -> Conn 'R Int32 Int32
algebra = (Int32 -> Int32 -> Int32) -> Int32 -> Conn 'R Int32 Int32
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Int32 -> Int32 -> Int32
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

instance Semilattice k Int64
instance Algebra 'L Int64 where algebra :: Int64 -> Conn 'L Int64 Int64
algebra = (Int64 -> Int64 -> Int64) -> Int64 -> Conn 'L Int64 Int64
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Int64 -> Int64 -> Int64
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Int64 where algebra :: Int64 -> Conn 'R Int64 Int64
algebra = (Int64 -> Int64 -> Int64) -> Int64 -> Conn 'R Int64 Int64
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Int64 -> Int64 -> Int64
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

instance Semilattice k Int
instance Algebra 'L Int where algebra :: Int -> Conn 'L Int Int
algebra = (Int -> Int -> Int) -> Int -> Conn 'L Int Int
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Int -> Int -> Int
forall a. (Total a, Bounded a) => a -> a -> a
impliesL
instance Algebra 'R Int where algebra :: Int -> Conn 'R Int Int
algebra = (Int -> Int -> Int) -> Int -> Conn 'R Int Int
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Int -> Int -> Int
forall a. (Total a, Bounded a) => a -> a -> a
impliesR

-------------------------------------------------------------------------------
-- Instances: product types
-------------------------------------------------------------------------------

instance (Lattice a, Lattice b) => Semilattice k (a, b) where
    bounded :: Conn k () (a, b)
bounded = (() -> (a, b))
-> ((a, b) -> ()) -> (() -> (a, b)) -> Conn k () (a, b)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn ((a, b) -> () -> (a, b)
forall a b. a -> b -> a
const (a
forall a. Join a => a
bottom, b
forall a. Join a => a
bottom)) (() -> (a, b) -> ()
forall a b. a -> b -> a
const ()) ((a, b) -> () -> (a, b)
forall a b. a -> b -> a
const (a
forall a. Meet a => a
top, b
forall a. Meet a => a
top))
    semilattice :: Conn k ((a, b), (a, b)) (a, b)
semilattice = (((a, b), (a, b)) -> (a, b))
-> ((a, b) -> ((a, b), (a, b)))
-> (((a, b), (a, b)) -> (a, b))
-> Conn k ((a, b), (a, b)) (a, b)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (((a, b) -> (a, b) -> (a, b)) -> ((a, b), (a, b)) -> (a, b)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (a, b) -> (a, b) -> (a, b)
forall a b.
(Semilattice 'L a, Semilattice 'L b) =>
(a, b) -> (a, b) -> (a, b)
joinTuple) (a, b) -> ((a, b), (a, b))
forall a. a -> (a, a)
fork (((a, b) -> (a, b) -> (a, b)) -> ((a, b), (a, b)) -> (a, b)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (a, b) -> (a, b) -> (a, b)
forall a b.
(Semilattice 'R a, Semilattice 'R b) =>
(a, b) -> (a, b) -> (a, b)
meetTuple)

instance (Heyting a, Heyting b) => Algebra 'R (a, b) where
    algebra :: (a, b) -> Conn 'R (a, b) (a, b)
algebra (a
a, b
b) = a -> Conn 'R a a
forall (k :: Kan) a. Algebra k a => a -> Conn k a a
algebra a
a Conn 'R a a -> Conn 'R b b -> Conn 'R (a, b) (a, b)
forall (k :: Kan) a b c d.
Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)
`strong` b -> Conn 'R b b
forall (k :: Kan) a. Algebra k a => a -> Conn k a a
algebra b
b

instance (Coheyting a, Coheyting b) => Algebra 'L (a, b) where
    algebra :: (a, b) -> Conn 'L (a, b) (a, b)
algebra (a
a, b
b) = a -> Conn 'L a a
forall (k :: Kan) a. Algebra k a => a -> Conn k a a
algebra a
a Conn 'L a a -> Conn 'L b b -> Conn 'L (a, b) (a, b)
forall (k :: Kan) a b c d.
Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)
`strong` b -> Conn 'L b b
forall (k :: Kan) a. Algebra k a => a -> Conn k a a
algebra b
b

instance (Symmetric a, Symmetric b) => Symmetric (a, b) where
    not :: (a, b) -> (a, b)
not = (a -> a) -> (b -> b) -> (a, b) -> (a, b)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> a
forall a. Symmetric a => a -> a
not b -> b
forall a. Symmetric a => a -> a
not

instance (Boolean a, Boolean b) => Boolean (a, b)

-------------------------------------------------------------------------------
-- Instances: sum types
-------------------------------------------------------------------------------

instance Join a => Semilattice 'L (Maybe a) where
    bounded :: Conn 'L () (Maybe a)
bounded = (() -> Maybe a) -> (Maybe a -> ()) -> Conn 'L () (Maybe a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (Maybe a -> () -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing) (() -> Maybe a -> ()
forall a b. a -> b -> a
const ())
    semilattice :: Conn 'L (Maybe a, Maybe a) (Maybe a)
semilattice = ((Maybe a, Maybe a) -> Maybe a)
-> (Maybe a -> (Maybe a, Maybe a))
-> Conn 'L (Maybe a, Maybe a) (Maybe a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL ((Maybe a -> Maybe a -> Maybe a) -> (Maybe a, Maybe a) -> Maybe a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe a -> Maybe a -> Maybe a
forall a. Join a => Maybe a -> Maybe a -> Maybe a
joinMaybe) Maybe a -> (Maybe a, Maybe a)
forall a. a -> (a, a)
fork

instance Meet a => Semilattice 'R (Maybe a) where
    bounded :: Conn 'R () (Maybe a)
bounded = (Maybe a -> ()) -> (() -> Maybe a) -> Conn 'R () (Maybe a)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR (() -> Maybe a -> ()
forall a b. a -> b -> a
const ()) (Maybe a -> () -> Maybe a
forall a b. a -> b -> a
const (Maybe a -> () -> Maybe a) -> Maybe a -> () -> Maybe a
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. Meet a => a
top)
    semilattice :: Conn 'R (Maybe a, Maybe a) (Maybe a)
semilattice = (Maybe a -> (Maybe a, Maybe a))
-> ((Maybe a, Maybe a) -> Maybe a)
-> Conn 'R (Maybe a, Maybe a) (Maybe a)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR Maybe a -> (Maybe a, Maybe a)
forall a. a -> (a, a)
fork ((Maybe a -> Maybe a -> Maybe a) -> (Maybe a, Maybe a) -> Maybe a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe a -> Maybe a -> Maybe a
forall a. Meet a => Maybe a -> Maybe a -> Maybe a
meetMaybe)

instance Heyting a => Algebra 'R (Maybe a) where
    algebra :: Maybe a -> Conn 'R (Maybe a) (Maybe a)
algebra = (Maybe a -> Maybe a -> Maybe a)
-> Maybe a -> Conn 'R (Maybe a) (Maybe a)
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Maybe a -> Maybe a -> Maybe a
forall a. Algebra 'R a => Maybe a -> Maybe a -> Maybe a
f
      where
        f :: Maybe a -> Maybe a -> Maybe a
f (Just a
a) (Just a
b) = a -> Maybe a
forall a. a -> Maybe a
Just (a
a a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
b)
        f Maybe a
Nothing Maybe a
_ = a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. Meet a => a
top
        f Maybe a
_ Maybe a
Nothing = Maybe a
forall a. Maybe a
Nothing

instance Join a => Semilattice 'L (Extended a) where
    bounded :: Conn 'L () (Extended a)
bounded = (() -> Extended a)
-> (Extended a -> ())
-> (() -> Extended a)
-> Conn 'L () (Extended a)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (Extended a -> () -> Extended a
forall a b. a -> b -> a
const Extended a
forall a. Extended a
Bottom) (() -> Extended a -> ()
forall a b. a -> b -> a
const ()) (Extended a -> () -> Extended a
forall a b. a -> b -> a
const Extended a
forall a. Extended a
Top)
    semilattice :: Conn 'L (Extended a, Extended a) (Extended a)
semilattice = ((Extended a, Extended a) -> Extended a)
-> (Extended a -> (Extended a, Extended a))
-> Conn 'L (Extended a, Extended a) (Extended a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL ((Extended a -> Extended a -> Extended a)
-> (Extended a, Extended a) -> Extended a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Extended a -> Extended a -> Extended a
forall a. Join a => Extended a -> Extended a -> Extended a
joinExtended) Extended a -> (Extended a, Extended a)
forall a. a -> (a, a)
fork

instance Meet a => Semilattice 'R (Extended a) where
    bounded :: Conn 'R () (Extended a)
bounded = (() -> Extended a)
-> (Extended a -> ())
-> (() -> Extended a)
-> Conn 'R () (Extended a)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (Extended a -> () -> Extended a
forall a b. a -> b -> a
const Extended a
forall a. Extended a
Bottom) (() -> Extended a -> ()
forall a b. a -> b -> a
const ()) (Extended a -> () -> Extended a
forall a b. a -> b -> a
const Extended a
forall a. Extended a
Top)
    semilattice :: Conn 'R (Extended a, Extended a) (Extended a)
semilattice = (Extended a -> (Extended a, Extended a))
-> ((Extended a, Extended a) -> Extended a)
-> Conn 'R (Extended a, Extended a) (Extended a)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR Extended a -> (Extended a, Extended a)
forall a. a -> (a, a)
fork ((Extended a -> Extended a -> Extended a)
-> (Extended a, Extended a) -> Extended a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Extended a -> Extended a -> Extended a
forall a. Meet a => Extended a -> Extended a -> Extended a
meetExtended)

instance Heyting a => Algebra 'R (Extended a) where
    algebra :: Extended a -> Conn 'R (Extended a) (Extended a)
algebra = (Extended a -> Extended a -> Extended a)
-> Extended a -> Conn 'R (Extended a) (Extended a)
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Extended a -> Extended a -> Extended a
forall a. Algebra 'R a => Extended a -> Extended a -> Extended a
f
      where
        Extended a
a f :: Extended a -> Extended a -> Extended a
`f` Extended a
b
            | a
a a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
<~ a
b = Extended a
forall a. Extended a
Top
            | Bool
otherwise = a -> Extended a
forall a. a -> Extended a
Extended (a
a a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
b)
        Extended a
Top `f` Extended a
a = Extended a
a
        Extended a
_ `f` Extended a
Top = Extended a
forall a. Extended a
Top
        Extended a
Bottom `f` Extended a
_ = Extended a
forall a. Extended a
Top
        Extended a
_ `f` Extended a
Bottom = Extended a
forall a. Extended a
Bottom

-- | All minimal elements of the upper lattice cover all maximal elements of the lower lattice.
instance (Join a, Join b) => Semilattice 'L (Either a b) where
    bounded :: Conn 'L () (Either a b)
bounded = (() -> Either a b) -> (Either a b -> ()) -> Conn 'L () (Either a b)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (Either a b -> () -> Either a b
forall a b. a -> b -> a
const (Either a b -> () -> Either a b) -> Either a b -> () -> Either a b
forall a b. (a -> b) -> a -> b
$ a -> Either a b
forall a b. a -> Either a b
Left a
forall a. Join a => a
bottom) (() -> Either a b -> ()
forall a b. a -> b -> a
const ())
    semilattice :: Conn 'L (Either a b, Either a b) (Either a b)
semilattice = ((Either a b, Either a b) -> Either a b)
-> (Either a b -> (Either a b, Either a b))
-> Conn 'L (Either a b, Either a b) (Either a b)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL ((Either a b -> Either a b -> Either a b)
-> (Either a b, Either a b) -> Either a b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Either a b -> Either a b -> Either a b
forall a b.
(Join a, Join b) =>
Either a b -> Either a b -> Either a b
joinEither) Either a b -> (Either a b, Either a b)
forall a. a -> (a, a)
fork

instance (Meet a, Meet b) => Semilattice 'R (Either a b) where
    bounded :: Conn 'R () (Either a b)
bounded = (Either a b -> ()) -> (() -> Either a b) -> Conn 'R () (Either a b)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR (() -> Either a b -> ()
forall a b. a -> b -> a
const ()) (Either a b -> () -> Either a b
forall a b. a -> b -> a
const (Either a b -> () -> Either a b) -> Either a b -> () -> Either a b
forall a b. (a -> b) -> a -> b
$ b -> Either a b
forall a b. b -> Either a b
Right b
forall a. Meet a => a
top)
    semilattice :: Conn 'R (Either a b, Either a b) (Either a b)
semilattice = (Either a b -> (Either a b, Either a b))
-> ((Either a b, Either a b) -> Either a b)
-> Conn 'R (Either a b, Either a b) (Either a b)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR Either a b -> (Either a b, Either a b)
forall a. a -> (a, a)
fork ((Either a b -> Either a b -> Either a b)
-> (Either a b, Either a b) -> Either a b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Either a b -> Either a b -> Either a b
forall a b.
(Meet a, Meet b) =>
Either a b -> Either a b -> Either a b
meetEither)

-- |
-- Subdirectly irreducible Algebra algebra.
instance Heyting a => Algebra 'R (Lowered a) where
    algebra :: Lowered a -> Conn 'R (Lowered a) (Lowered a)
algebra = (Lowered a -> Lowered a -> Lowered a)
-> Lowered a -> Conn 'R (Lowered a) (Lowered a)
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Lowered a -> Lowered a -> Lowered a
forall a b b.
(Semilattice 'R b, Algebra 'R a) =>
Either a b -> Either a b -> Either a b
f
      where
        (Left a
a) f :: Either a b -> Either a b -> Either a b
`f` (Left a
b)
            | a
a a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
<~ a
b = Either a b
forall a. Meet a => a
top
            | Bool
otherwise = a -> Either a b
forall a b. a -> Either a b
Left (a
a a -> a -> a
forall a. Algebra 'R a => a -> a -> a
// a
b)
        (Right b
_) `f` Either a b
a = Either a b
a
        Either a b
_ `f` (Right b
_) = Either a b
forall a. Meet a => a
top

instance Heyting a => Algebra 'R (Lifted a) where
    algebra :: Lifted a -> Conn 'R (Lifted a) (Lifted a)
algebra = (Lifted a -> Lifted a -> Lifted a)
-> Lifted a -> Conn 'R (Lifted a) (Lifted a)
forall a. Meet a => (a -> a -> a) -> a -> ConnR a a
heyting Lifted a -> Lifted a -> Lifted a
forall b a a a.
(Algebra 'R b, Semilattice 'L a, Semilattice 'L b) =>
Either a b -> Either a b -> Either a b
f
      where
        f :: Either a b -> Either a b -> Either a b
f (Right b
a) (Right b
b) = b -> Either a b
forall a b. b -> Either a b
Right (b
a b -> b -> b
forall a. Algebra 'R a => a -> a -> a
// b
b)
        f (Left a
_) Either a b
_ = b -> Either a b
forall a b. b -> Either a b
Right b
forall a. Meet a => a
top
        f Either a b
_ (Left a
_) = Either a b
forall a. Join a => a
bottom

-------------------------------------------------------------------------------
-- Instances: collections
-------------------------------------------------------------------------------

instance Total a => Semilattice 'L (Set.Set a)

instance Total a => Algebra 'L (Set.Set a) where
    algebra :: Set a -> Conn 'L (Set a) (Set a)
algebra = (Set a -> Set a -> Set a) -> Set a -> Conn 'L (Set a) (Set a)
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
(Set.\\)

--instance (Total a, U.Finite a) => Algebra 'R (Set.Set a) where
--  algebra = symmetricR

--instance (Total a, U.Finite a) => Symmetric (Set.Set a) where
--  not = non --(U.universe Set.\\)

--instance (Total a, U.Finite a) => Boolean (Set.Set a) where

instance Semilattice 'L IntSet.IntSet

instance Algebra 'L IntSet.IntSet where
    algebra :: IntSet -> Conn 'L IntSet IntSet
algebra = (IntSet -> IntSet -> IntSet) -> IntSet -> Conn 'L IntSet IntSet
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting IntSet -> IntSet -> IntSet
(IntSet.\\)

{-
instance Algebra 'R IntSet.IntSet where
  --heyting = heyting $ \x y -> non x \/ y
  algebra = symmetricR

instance Symmetric IntSet.IntSet where
  not = non --(U.universe IntSet.\\)

instance Boolean IntSet.IntSet where

-}

instance (Total k, Join a) => Semilattice 'L (Map.Map k a) where
    bounded :: Conn 'L () (Map k a)
bounded = (() -> Map k a) -> (Map k a -> ()) -> Conn 'L () (Map k a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (Map k a -> () -> Map k a
forall a b. a -> b -> a
const Map k a
forall k a. Map k a
Map.empty) (() -> Map k a -> ()
forall a b. a -> b -> a
const ())

    semilattice :: Conn 'L (Map k a, Map k a) (Map k a)
semilattice = ((Map k a, Map k a) -> Map k a)
-> (Map k a -> (Map k a, Map k a))
-> Conn 'L (Map k a, Map k a) (Map k a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (Map k a, Map k a) -> Map k a
f Map k a -> (Map k a, Map k a)
forall a. a -> (a, a)
fork
      where
        f :: (Map k a, Map k a) -> Map k a
f = (Map k a -> Map k a -> Map k a) -> (Map k a, Map k a) -> Map k a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Map k a -> Map k a -> Map k a) -> (Map k a, Map k a) -> Map k a)
-> (Map k a -> Map k a -> Map k a) -> (Map k a, Map k a) -> Map k a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Map k a -> Map k a -> Map k a
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (((a, a) -> a) -> a -> a -> a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((a, a) -> a) -> a -> a -> a) -> ((a, a) -> a) -> a -> a -> a
forall a b. (a -> b) -> a -> b
$ ConnL (a, a) a -> (a, a) -> a
forall a b. ConnL a b -> a -> b
ceilingWith ConnL (a, a) a
forall (k :: Kan) a. Semilattice k a => Conn k (a, a) a
semilattice)

instance (Total k, Join a) => Algebra 'L (Map.Map k a) where
    algebra :: Map k a -> Conn 'L (Map k a) (Map k a)
algebra = (Map k a -> Map k a -> Map k a)
-> Map k a -> Conn 'L (Map k a) (Map k a)
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting Map k a -> Map k a -> Map k a
forall k a b. Ord k => Map k a -> Map k b -> Map k a
(Map.\\)

instance (Join a) => Semilattice 'L (IntMap.IntMap a) where
    bounded :: Conn 'L () (IntMap a)
bounded = (() -> IntMap a) -> (IntMap a -> ()) -> Conn 'L () (IntMap a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (IntMap a -> () -> IntMap a
forall a b. a -> b -> a
const IntMap a
forall a. IntMap a
IntMap.empty) (() -> IntMap a -> ()
forall a b. a -> b -> a
const ())

    semilattice :: Conn 'L (IntMap a, IntMap a) (IntMap a)
semilattice = ((IntMap a, IntMap a) -> IntMap a)
-> (IntMap a -> (IntMap a, IntMap a))
-> Conn 'L (IntMap a, IntMap a) (IntMap a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (IntMap a, IntMap a) -> IntMap a
f IntMap a -> (IntMap a, IntMap a)
forall a. a -> (a, a)
fork
      where
        f :: (IntMap a, IntMap a) -> IntMap a
f = (IntMap a -> IntMap a -> IntMap a)
-> (IntMap a, IntMap a) -> IntMap a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((IntMap a -> IntMap a -> IntMap a)
 -> (IntMap a, IntMap a) -> IntMap a)
-> (IntMap a -> IntMap a -> IntMap a)
-> (IntMap a, IntMap a)
-> IntMap a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith (((a, a) -> a) -> a -> a -> a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((a, a) -> a) -> a -> a -> a) -> ((a, a) -> a) -> a -> a -> a
forall a b. (a -> b) -> a -> b
$ ConnL (a, a) a -> (a, a) -> a
forall a b. ConnL a b -> a -> b
ceilingWith ConnL (a, a) a
forall (k :: Kan) a. Semilattice k a => Conn k (a, a) a
semilattice)

instance (Join a) => Algebra 'L (IntMap.IntMap a) where
    algebra :: IntMap a -> Conn 'L (IntMap a) (IntMap a)
algebra = (IntMap a -> IntMap a -> IntMap a)
-> IntMap a -> Conn 'L (IntMap a) (IntMap a)
forall a. Join a => (a -> a -> a) -> a -> ConnL a a
coheyting IntMap a -> IntMap a -> IntMap a
forall a b. IntMap a -> IntMap b -> IntMap a
(IntMap.\\)

{- TODO pick an instance either key-aware or no

instance (Total a, U.Finite a, Heyting b) => Algebra 'R (Map.Map a b) where

  algebra = heyting $ \a b ->
    let
      x = Map.merge
            Map.dropMissing                    -- drop if an element is missing in @b@
            (Map.mapMissing (\_ _ -> true))     -- put @true@ if an element is missing in @a@
            (Map.zipWithMatched (\_ -> (//) )) -- merge  matching elements with @`implies`@
            a b

      y = Map.fromList [(k, true) | k <- U.universeF, not (Map.member k a), not (Map.member k b) ]
        -- for elements which are not in a, nor in b add
        -- a @true@ key
    in
      Map.union x y

-- TODO: compare performance
impliesMap a b =
  Map.intersection (`implies`) a b
    `Map.union` Map.map (const true) (Map.difference b a)
    `Map.union` Map.fromList [(k, true) | k <- universeF, not (Map.member k a), not (Map.member k b)]

-}

{-

-- A symmetric Heyting algebra
--
-- λ> implies (False ... True) (False ... True)
-- Interval True True
-- λ> implies (False ... True) (singleton False)
-- Interval False False
-- λ> implies (singleton True) (False ... True)
-- Interval False True
--
-- λ> implies ([EQ,GT] ... [EQ,GT]) ([LT] ... [LT,EQ])  :: Interval (Set.Set Ordering)
-- Interval (fromList [LT]) (fromList [LT,EQ])
--
-- TODO: may need /a/ to be boolean here.
implies :: Symmetric a => Interval a -> Interval a -> Interval a
implies i1 i2 = maybe iempty (uncurry (...)) $ liftA2 f (endpts i1) (endpts i2) where
  f (x1,x2) (y1,y2) = (x1 // y1 /\ x2 // y2, x2 // y2)

  --TODO: would this work for interval orders?
  f (x1,x2) (y1,y2) = (x1 // y1 /\ x2 // y2, x1 // y1 \/ x2 // y2)

coimplies i1 i2 = not (not i1 `implies` not i2)

-- The symmetry
-- neg x = top \\ not x
-- non x = not x // bottom
-- λ> not ([LT] ... [LT,GT]) :: Interval (Set.Set Ordering)
-- Interval (fromList [EQ]) (fromList [EQ,GT])
--
not :: Symmetric a => Interval a -> Interval a
not = maybe iempty (\(x1, x2) -> neg x2 ... neg x1) . endpts

-- λ> neg' (False ... True)
-- Interval False False
-- λ> (False ... True) `implies` (singleton False)
-- Interval False False
--
neg' x = (bottom ... top) `coimplies` (not x)

-- λ> non' (False ... True)
-- Interval False False
-- λ> (singleton True) `coimplies` (False ... True)
-- Interval False False
--
non' x = not x `implies` (singleton bottom)

-}

-- Internal

-------------------------
fork :: a -> (a, a)
fork :: a -> (a, a)
fork a
x = (a
x, a
x)

impliesL :: (Total a, P.Bounded a) => a -> a -> a
impliesL :: a -> a -> a
impliesL a
x a
y = if a
y a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
< a
x then a
x else a
forall a. Bounded a => a
P.minBound

impliesR :: (Total a, P.Bounded a) => a -> a -> a
impliesR :: a -> a -> a
impliesR a
x a
y = if a
x a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
> a
y then a
y else a
forall a. Bounded a => a
P.maxBound

joinTuple :: (Semilattice 'L a, Semilattice 'L b) => (a, b) -> (a, b) -> (a, b)
joinTuple :: (a, b) -> (a, b) -> (a, b)
joinTuple (a
x1, b
y1) (a
x2, b
y2) = (a
x1 a -> a -> a
forall a. Join a => a -> a -> a
\/ a
x2, b
y1 b -> b -> b
forall a. Join a => a -> a -> a
\/ b
y2)

meetTuple :: (Semilattice 'R a, Semilattice 'R b) => (a, b) -> (a, b) -> (a, b)
meetTuple :: (a, b) -> (a, b) -> (a, b)
meetTuple (a
x1, b
y1) (a
x2, b
y2) = (a
x1 a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
x2, b
y1 b -> b -> b
forall a. Meet a => a -> a -> a
/\ b
y2)

joinMaybe :: Join a => Maybe a -> Maybe a -> Maybe a
joinMaybe :: Maybe a -> Maybe a -> Maybe a
joinMaybe (Just a
x) (Just a
y) = a -> Maybe a
forall a. a -> Maybe a
Just (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y)
joinMaybe u :: Maybe a
u@(Just a
_) Maybe a
_ = Maybe a
u
joinMaybe Maybe a
_ u :: Maybe a
u@(Just a
_) = Maybe a
u
joinMaybe Maybe a
Nothing Maybe a
Nothing = Maybe a
forall a. Maybe a
Nothing

meetMaybe :: Meet a => Maybe a -> Maybe a -> Maybe a
meetMaybe :: Maybe a -> Maybe a -> Maybe a
meetMaybe Maybe a
Nothing Maybe a
Nothing = Maybe a
forall a. Maybe a
Nothing
meetMaybe Maybe a
Nothing Maybe a
_ = Maybe a
forall a. Maybe a
Nothing
meetMaybe Maybe a
_ Maybe a
Nothing = Maybe a
forall a. Maybe a
Nothing
meetMaybe (Just a
x) (Just a
y) = a -> Maybe a
forall a. a -> Maybe a
Just (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y)

joinExtended :: Join a => Extended a -> Extended a -> Extended a
joinExtended :: Extended a -> Extended a -> Extended a
joinExtended Extended a
Top Extended a
_ = Extended a
forall a. Extended a
Top
joinExtended Extended a
_ Extended a
Top = Extended a
forall a. Extended a
Top
joinExtended (Extended a
x) (Extended a
y) = a -> Extended a
forall a. a -> Extended a
Extended (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y)
joinExtended Extended a
Bottom Extended a
y = Extended a
y
joinExtended Extended a
x Extended a
Bottom = Extended a
x

meetExtended :: Meet a => Extended a -> Extended a -> Extended a
meetExtended :: Extended a -> Extended a -> Extended a
meetExtended Extended a
Top Extended a
y = Extended a
y
meetExtended Extended a
x Extended a
Top = Extended a
x
meetExtended (Extended a
x) (Extended a
y) = a -> Extended a
forall a. a -> Extended a
Extended (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y)
meetExtended Extended a
Bottom Extended a
_ = Extended a
forall a. Extended a
Bottom
meetExtended Extended a
_ Extended a
Bottom = Extended a
forall a. Extended a
Bottom

joinEither :: (Join a, Join b) => Either a b -> Either a b -> Either a b
joinEither :: Either a b -> Either a b -> Either a b
joinEither (Right b
x) (Right b
y) = b -> Either a b
forall a b. b -> Either a b
Right (b
x b -> b -> b
forall a. Join a => a -> a -> a
\/ b
y)
joinEither u :: Either a b
u@(Right b
_) Either a b
_ = Either a b
u
joinEither Either a b
_ u :: Either a b
u@(Right b
_) = Either a b
u
joinEither (Left a
x) (Left a
y) = a -> Either a b
forall a b. a -> Either a b
Left (a
x a -> a -> a
forall a. Join a => a -> a -> a
\/ a
y)

meetEither :: (Meet a, Meet b) => Either a b -> Either a b -> Either a b
meetEither :: Either a b -> Either a b -> Either a b
meetEither (Left a
x) (Left a
y) = a -> Either a b
forall a b. a -> Either a b
Left (a
x a -> a -> a
forall a. Meet a => a -> a -> a
/\ a
y)
meetEither l :: Either a b
l@(Left a
_) Either a b
_ = Either a b
l
meetEither Either a b
_ l :: Either a b
l@(Left a
_) = Either a b
l
meetEither (Right b
x) (Right b
y) = b -> Either a b
forall a b. b -> Either a b
Right (b
x b -> b -> b
forall a. Meet a => a -> a -> a
/\ b
y)