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.