# The Singleton Kind Calculus

The next type theory we'll be exploring is the calculus of singleton kinds. This is necessary to represent type-fixed signatures, like

sig
type t = int
type u
val a : t
end


How do we kind this? We can't kind the t tycon at $$*$$, because that would allow nonconformant structures (say, those assigning t to string) to ascribe.

The answer is to add a new kind constructor S(c) of singleton kinds, kinds with only one inhabitant. Set-theoretically, S(c) represents the singleton set $${c}$$, but that's about where the similarities end.

It turns out that this simple construct (and its intuitive properties) require a lot more power in its machinery.