Documentation

Boolean conjunction forms a semilattice.

Idempotence:

x /\ x == (x :: Bool)

Associativity:

a /\ (b /\ c) == (a /\ b) /\ (c :: Bool)

Commutativity:

a /\ b == b /\ (a :: Bool)

Identity:

upperBound /\ a == (a :: Bool)

Absorption:

lowerBound /\ a == (lowerBound :: Bool)

Orderings form a semilattice.

Idempotence:

x /\ x == (x :: Ordering)

Associativity:

a /\ (b /\ c) == (a /\ b) /\ (c :: Ordering)

Commutativity:

a /\ b == b /\ (a :: Ordering)

Identity:

upperBound /\ a == (a :: Ordering)

Absorption:

lowerBound /\ a == (lowerBound :: Ordering)

IntSet intersection forms a semilattice.

Idempotence:

x /\ x == (x :: IntSet)

Associativity:

a /\ (b /\ c) == (a /\ b) /\ (c :: IntSet)

Commutativity:

a /\ b == b /\ (a :: IntSet)

Absorption:

lowerBound /\ a == (lowerBound :: IntSet)

The greatest lowerBound bound gives rise to a meet semilattice.

Idempotence:

x /\ x == (x :: Min Int)

Associativity:

a /\ (b /\ c) == (a /\ b) /\ (c :: Min Int)

Commutativity:

a /\ b == b /\ (a :: Min Int)

Identity:

upperBound /\ a == (a :: Min Int)

Absorption:

lowerBound /\ a == (lowerBound :: Min Int)

IntMap union with Meetable values forms a semilattice.

Idempotence:

x /\ x == (x :: IntMap (Set Char))

Associativity:

a /\ (b /\ c) == (a /\ b) /\ (c :: IntMap (Set Char))

Commutativity:

a /\ b == b /\ (a :: IntMap (Set Char))

Absorption:

lowerBound /\ a == (lowerBound :: IntMap (Set Char))

Set intersection forms a semilattice.

Idempotence:

x /\ x == (x :: Set Char)

Associativity:

a /\ (b /\ c) == (a /\ b) /\ (c :: Set Char)

Commutativity:

a /\ b == b /\ (a :: Set Char)

Absorption:

lowerBound /\ a == (lowerBound :: Set Char)

HashSet intersection forms a semilattice.

Idempotence:

x /\ x == (x :: HashSet Char)

Associativity:

a /\ (b /\ c) == (a /\ b) /\ (c :: HashSet Char)

Commutativity:

a /\ b == b /\ (a :: HashSet Char)

Absorption:

lowerBound /\ a == (lowerBound :: HashSet Char)

Total Orderings give rise to a meet semilattice satisfying:

Idempotence:

Order x /\ Order x == Order x

Associativity:

Order a /\ (Order b /\ Order c) == (Order a /\ Order b) /\ Order c

Commutativity:

Order a /\ Order b == Order b /\ Order a

Identity:

upperBound /\ Order a == Order (a :: Int)

Absorption:

lowerBound /\ Order a == (lowerBound :: Order Int)

Distributivity:

Order a /\ (Order b \/ Order c) == Order a /\ Order b \/ Order a /\ Order c

Functions with semilattice codomains form a semilattice.

Idempotence:

\ (Fn x) -> x /\ x ~= (x :: Int -> Bool)

Associativity:

\ (Fn a) (Fn b) (Fn c) -> a /\ (b /\ c) ~= (a /\ b) /\ (c :: Int -> Bool)

Commutativity:

\ (Fn a) (Fn b) -> a /\ b ~= b /\ (a :: Int -> Bool)

Identity:

\ (Fn a) -> upperBound /\ a ~= (a :: Int -> Bool)

Absorption:

\ (Fn a) -> lowerBound /\ a ~= (lowerBound :: Int -> Bool)

Map union with Meetable values forms a semilattice.

Idempotence:

x /\ x == (x :: Map Char (Set Char))

Associativity:

a /\ (b /\ c) == (a /\ b) /\ (c :: Map Char (Set Char))

Commutativity:

a /\ b == b /\ (a :: Map Char (Set Char))

Absorption:

lowerBound /\ a == (lowerBound :: Map Char (Set Char))

HashMap union with Meetable values forms a semilattice.

Idempotence:

x /\ x == (x :: HashMap Char (Set Char))

Associativity:

a /\ (b /\ c) == (a /\ b) /\ (c :: HashMap Char (Set Char))

Commutativity:

a /\ b == b /\ (a :: HashMap Char (Set Char))

Absorption:

lowerBound /\ a == (lowerBound :: HashMap Char (Set Char))

Meeting <> is associative.

Meeting a <> (Meeting b <> Meeting c) == (Meeting a <> Meeting b) <> Meeting (c :: IntSet)

Meeting mempty is the left- and right-identity.

let (l, r) = (mappend mempty (Meeting x), mappend (Meeting x) mempty) in l == Meeting x && r == Meeting (x :: Bool)