semi-proof.md

Proof that if (S, ⊕) forms a semilattice, then so does (case class C(s: S), ⊕')

A Semilattice consists of a set S and a closed binary operation ⊕ which is

1. associative, ie ∀ x, y, z ∈ S: x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z
2. commutative, ie ∀ x, y ∈ S: x ⊕ y = y ⊕ x
3. idempotent, ie ∀ x ∈ S: x ⊕ x = x

if we have some type S and some binary function ⊕ which together form a Semilattice, then can we define a case class C(s: S) which is also a Semilattice?

Let's define the instance like this

implicit def cSemilattice = new Semilattice[C] {
  def combine(c1: C, c2: C): C = C(c1.s |+| c2.s)
}

ie:

C(s1) ⊕' C(s2) = C(s1 ⊕ s2)    (**)

and test the laws

closure: The type system shows this is closed

associativity:

if ∀ x, y, z ∈ S, then

∀ x', y', z' ∈ C: x' ⊕' (y' ⊕' z') = C(x) ⊕' (C(y) ⊕' C(z))
                                 = C(x) ⊕' (C(y ⊕ z))
                                 = C(x ⊕ (y ⊕ z))
                                 = C((x ⊕ y) ⊕ z)           by 1)
                                 = C(x ⊕ y) ⊕' C(z)          by (**)
                                 = (C(x) ⊕' C(y)) ⊕' C(z)     QED

commutativity:

similarly, if ∀ x, y ∈ S, then

∀ x', y' ∈ C: x' ⊕' y' = C(x) ⊕' C(y)
                      = C(x ⊕ y)
                      = C(y ⊕ x)          by 2)
                      = C(y) ⊕' C(x)      by (**) QED

idempotence:

similarly, if ∀ x ∈ S, then

∀ x' ∈ C: x' ⊕' x' = C(x) ⊕' C(x)
                      = C(x ⊕ x)
                      = C(x)             by 3)
                      = C(x)             QED

this is easily expandable to case classes with an arbitary number of arguments like so

case class C'(s1: S, s2: S', ... sN: S''')

where (S, |+|), (S', |+|'), ... (S''', |+|''') form semilattices

implicit def c'Semilattice = new Semilattice[C'] {
  def combine(c1: C', c2: C'): C' = C'(c1.s1 |+|' c2.s1, ... c1.sn |+|''' c2.sn)
}