¶Constraints on sets
Much of the set-theoretic typing literature talks about constraints on typevars.
A value (numbers, e.g. 0, 1) are the runtime objects that we're using types to track.
A type (lowercase Roman letters, e.g. s, t) is a set of values. These are just sets, so we can use the usual set operators (⊆, ∩) on them.
A typevar (lowercase Greek letters, e.g. α, β) can specialize to a type; we can think of it as the set of types that it can specialize to.
A constraint (uppercase Roman letters, e.g. C, D) places a limit on which types the typevar can specialize to; it helps define which particular set of types the typevar represents.
Since types are just sets (of values), they form a Boolean algebra / complemented distributive lattice. We can use the laws of a Boolean algebra to work out various relationships between types, typevars, and constraints.
¶Constraints
There are four kinds of constraint:
lower bound: (s ≤) upper bound: (≤ t) non-equivalent: (≠ t) incomparable: (≁ t)
We can define an interpretation function ⟦C⟧ that yields the set of types that a typevar bound by that constraint can specialize to.
⟦s ≤⟧ ≜ {x | s ⊆ x}
⟦≤ t⟧ ≜ {x | x ⊆ t}
⟦≠ t⟧ ≜ {x | x ≠ t} = {x | x ⊈ t ∨ t ⊈ x}
⟦≁ t⟧ ≜ {x | x ≁ t} = {x | x ⊈ t ∧ t ⊈ x}
We can define conjunction, disjunction, and negation for constraints:
⟦C ∧ D⟧ ≜ ⟦C⟧ ∩ ⟦D⟧ ⟦C ∨ D⟧ ≜ ⟦C⟧ ∪ ⟦D⟧ ⟦¬C⟧ ≜ ¬⟦C⟧
There some derived constraints, which can be defined in terms of the four basic kinds of constraint:
range: (s..t) ≜ (s ≤) ∧ (≤ t) equivalent: (= t) ≜ (t ≤) ∧ (≤ t)