In a finite universe of N objects, fully-static types correspond to
subsets of that universe. For example, the type {1,3} can hold either
object 1 or object 3. There are 2N such types, forming a lattice ordered
by set inclusion (⊆).
A gradual type represents an unknown static type. It can be
characterized as an interval [l, u] in the lattice, where l ⊆ u.
The gradual type could be any static type s with l ⊆ s ⊆ u.
These are called its materializations.
The dynamic type Any is the largest interval [Never, object], containing
all possible materializations. Intersecting Any with a static type puts
an upper bound on the interval; taking the union puts a lower bound.
There are 3N gradual types in total.
Click any node to select the bottom of the interval, then click a second
node to select the top. The highlighted nodes are the materializations
of the resulting gradual type.