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.