A Semilattice consists of a set S
and a closed binary operation ⊕
which is
- associative, ie ∀ x, y, z ∈ S: x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z
- commutative, ie ∀ x, y ∈ S: x ⊕ y = y ⊕ x
- 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)
}