{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Data.Lattice (
Lattice,
Semilattice (..),
Meet,
(/\),
top,
Join,
(\/),
bottom,
Biheyting,
Algebra (..),
Heyting,
(//),
iff,
neg,
middle,
heyting,
booleanR,
Coheyting,
(\\),
equiv,
non,
boundary,
coheyting,
booleanL,
Symmetric (..),
converseL,
converseR,
symmetricL,
symmetricR,
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
type Lattice a = (Join a, Meet a)
type Join = Semilattice 'L
type Meet = Semilattice 'R
class Order a => Semilattice (k :: Kan) a where
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
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 /\
(/\) :: 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
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 \/
(\/) :: 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
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 ()
type Heyting a = (Lattice a, Algebra 'R a)
type Coheyting a = (Lattice a, Algebra 'L a)
type Biheyting a = (Coheyting a, Heyting a)
class Semilattice k a => Algebra k a where
algebra :: a -> Conn k a a
infixr 8 //
(//) :: 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
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)
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
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
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`)
booleanR :: Heyting a => ConnR a a
booleanR :: ConnR a a
booleanR =
let
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
infixl 8 \\
(\\) :: 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
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)
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
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
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)
booleanL :: Coheyting a => ConnL a a
booleanL :: ConnL a a
booleanL =
let
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)
class Biheyting a => Symmetric a where
not :: a -> a
infixl 4 `xor`
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)
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
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
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)
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)
class Symmetric a => Boolean a where
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)
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
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)
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
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)
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
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 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 (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.\\)
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)