The above explanation omits a lot of details, but it's a start. To get more
precise, we must drill down into several aspects of what I've said so far.
The first of them is, __how can we compare program information using an order?__
### Lattices
Let's start with a question: when it comes to our specificity-based order,
is `-` less than, greater than, or equal to `+`? Surely it's not less specific;
knowing that a number is negative doesn't give you less information than
knowing if that number is positive. Similarly, it's not any more specific, for
the same reason. You could consider it equally specific, but that doesn't
seem quite right either; the information is different, so comparing specificity
feels apples-to-oranges. On the other hand, both `+` and `-` are clearly
more specific than `unknown`.
The solution to this conundrum is to simply refuse to compare certain elements:
`+` is neither less than, greater than, nor equal to `-`, but `+ < unknown` and
`- < unknown`. Such an ordering is called a [partial order](https://en.wikipedia.org/wiki/Partially_ordered_set).
Next, another question. Suppose that the user writes code like this:
```
if someCondition {
x = exprA;
} else {
x = exprB;
}
y = x;
```
If `exprA` has sign `s1`, and `exprB` has sign `s2`, what's the sign of `y`?
It's not necessarily `s1` nor `s2`, since they might not match: `s1` could be `+`,
and `s2` could be `-`, and using either `+` or `-` for `y` would be incorrect.
We're looking for something that can encompass _both_`s1` and `s2`.
Necessarily, it would be either equally specific or less specific than
either `s1` or `s2`: there isn't any new information coming in about `x`,
and since we don't know which branch is taken, we stand to lose a little
bit of info. However, our goal is always to maximize specificity, since
more specific signs give us more information about our program.
This gives us the following constraints. Since the combined sign `s` has to
be equally or less specific than either `s1` and `s2`, we have `s1 <= s` and
`s2 <= s`. However, we want to pick `s` such that it's more specific than
any other "combined sign" candidate. Thus, if there's another sign `t`,
with `s1 <= t` and `s2 <= t`, then it must be less specific than `s`: `s <= t`.
At first, the above constraints might seem quite complicated. We can interpret
them in more familiar territory by looking at numbers instead of signs.
If we have two numbers `n1` and `n2`, what number is the smallest number
that's bigger than either `n1` or `n2`? Why, the maximum of the two, of course!
There is a reason why I used the constraints above instead of just saying
"maximum". For numbers, `max(a,b)` is either `a` or `b`. However, we saw earlier
that neither `+` nor `-` works as the sign for `y` in our program. Moreover,
we agreed above that our order is _partial_: how can we pick "the bigger of two
elements" if neither is bigger than the other? `max` itself doesn't quite work,
but what we're looking for is something similar. Instead, we simply require a
similar function for our signs. We call this function "[least upper bound](https://en.wikipedia.org/wiki/Least-upper-bound_property)",
since it is the "least (most specific)
element that's greater (less specific) than either `s1` or `s2`". Conventionally,
this function is written as \\(a \\sqcup b\\) (or in our case, \\(s_1 \\sqcup s_2\\)).
We can define it for our signs so far using the following [Cayley table](https://en.wikipedia.org/wiki/Cayley_table).
{{<latex>}}
\begin{array}{c|cccc}
\sqcup & - & 0 & + & ? \\
\hline
-& - & ? & ? & ? \\
0 & ? & 0 & ? & ? \\
+ & ? & ? & + & ? \\
? & ? & ? & ? & ? \\
\end{array}
{{</latex>}}
By using the above table, we can see that \\((+\ \\sqcup\ -)\ =\ ?\\) (aka `unknown`).
This is correct; given the four signs we're working with, that's the most we can say.
Let's explore the analogy to the `max` function a little bit more, by observing
that this function has certain properties:
*`max(a, a) = a`. The maximum of one number is just that number.
Mathematically, this property is called _idempotence_. Note that
by inspecting the diagonal of the above table, we can confirm that our
\\((\\sqcup)\\) function is idempotent.
*`max(a, b) = max(b, a)`. If you're taking the maximum of two numbers,
it doesn't matter which one you consider first. This property is called
_commutativity_. Note that if you mirror the table along the diagonal,
it doesn't change; this shows that our \\((\\sqcup)\\) function is
commutative.
*`max(a, max(b, c)) = max(max(a, b), c)`. When you have three numbers,
and you're determining the maximum value, it doesn't matter which pair of
numbers you compare first. This property is called _associativity_. You
can use the table above to verify the \\((\\sqcup)\\) is associative, too.
A set that has a binary operation (like `max` or \\((\\sqcup)\\)) that
satisfies the above properties is called a [semilattice](https://en.wikipedia.org/wiki/Semilattice). In Agda, we can write this definition roughly as follows:
```Agda
record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where
field
⊔-assoc : (x y z : A) → ((x ⊔ y) ⊔ z) ≡ (x ⊔ (y ⊔ z))
