型のタグ集合と排他的ユニオン

Tが型表現、またはその意味であるインスタンス領域だとして、tags(T) は、Tのインスタンスに付いている可能性のあるタグの集合。次のことを保証したい。

• tags(T) は空ではない。
• x∈T ならば tag(x) ∈ tags(T)

そうなれば、S|T に対して、tags(S)∩tags(T) = 空 という命題が意味をもつから、排他性を定義できる。