Singleton kinds

This is a breakdown explanation of the singleton kinds used in the core language of phase distinction calculus in paper What is a recursive module?

First, to understand the example, we need to grasp two key concepts from the text: singleton kinds and dependent kinds.

Core Concepts

1. Singleton Kind: $\mathfrak{S}(c)$ Think of a regular kind like $T$ (the kind of simple types) as a big box containing many different types (like int, bool, string, etc.). [cite_start]A singleton kind, written as $\mathfrak{S}(c)$, is a very specific “box” that contains only one thing: the type constructor $c$ and anything definitionally equal to it[cite: 113].

   The paper states: “if c has kind $\mathfrak{S}(c^{\prime })$, the calculus permits the deduction of the equation $c=c^{\prime }:T$.” This is the crucial takeaway: if something is in the singleton kind $\mathfrak{S}(c^{\prime })$, it must be equal to $c^{\prime }$.

2. Dependent Kind (Product): $\Pi \alpha :{\kappa }_1.{\kappa }_2$ [cite_start]This represents a function at the kind level[cite: 111]. It describes a constructor function that takes a constructor $\alpha$ of kind ${\kappa }_1$ and produces a result of kind ${\kappa }_2$. [cite_start]The key is that the result kind ${\kappa }_2$ can depend on the input $\alpha$[cite: 111]. [cite_start]If $\alpha$ doesn’t appear in ${\kappa }_2$, it simplifies to a regular function kind ${\kappa }_1\to {\kappa }_2$[cite: 112].

---

Breaking Down the Example

Now, let’s look at the example provided in the paper: a constructor $c$ that has the kind $\Pi \alpha :T.\mathfrak{S}(list(\alpha ))$[cite: 116].

Let’s dissect this kind piece by piece:

• $\Pi \alpha :T...$: This tells us that $c$ is a function. It takes a type constructor $\alpha$ of kind $T$ (a simple monotype like int) as input.
• $...\mathfrak{S}(list(\alpha ))$: This describes the result of the function $c$. For any given input $\alpha$, the function returns something whose kind is the singleton kind $\mathfrak{S}(list(\alpha ))$.

Putting it together: The constructor $c$ is a function that, when you give it any type $\alpha$, produces a result that is definitionally equal to $list(\alpha )$.

Since this holds true for any type $\alpha$ we pass in, the only possible function that satisfies this property is the list function itself. Therefore, the calculus allows us to conclude that the constructor $c$ must be the list constructor.

So, we can deduce the equality: $c=list:T\to T$

[cite_start]This is what the paper means by “higher-order sharing”: we’re not just sharing a single type, but we’re sharing a type constructor function (a “higher-order” entity) by precisely describing its behavior using a combination of dependent kinds and singleton kinds[cite: 115]. [cite_start]Figure 2 in the paper you provided shows the formal rules for generalizing this principle[cite: 105].

A comment on the generalization of the singleton kind function

The footnote explains a technical but important design choice in the paper’s type theory: it restricts how “higher-order singletons” can be formed to prevent certain logical inconsistencies.

---

The Core Issue: Preserving Well-Formedness

[cite_start]The footnote states: “Note that higher-order singletons are not defined for kinds containing strictly positive singleton or dependent sum kinds; this would eliminate the useful property that $\kappa$ is a kind whenever $\mathfrak{S}(c:\kappa )$ is.” [cite: 117, 118]

Let’s break this down:

• “Strictly positive singleton or dependent sum kinds”: This refers to complex kinds where a singleton ($\mathfrak{S}$) or a dependent sum ($\Sigma$) appears in a “positive” position, meaning it’s not on the input side of a function arrow ($\Pi$). For example, a kind like $\Sigma \alpha :T.\mathfrak{S}(\alpha )$ would be problematic.

• “The useful property that $\kappa$ is a kind whenever $\mathfrak{S}(c:\kappa )$ is”: This is a sanity check for the type system. In simple terms, the “type” of a singleton should be a valid “type” itself. The singleton definition $\mathfrak{S}(c:\kappa )$ should break down into a structure of other valid kinds. If you allow the problematic kinds mentioned above, this property breaks down, and the system can’t guarantee that all its kind definitions are well-formed.

Think of it like a rule in grammar. A rule might state, “An adjective can describe a noun.” The system needs to ensure that what it identifies as an “adjective” and a “noun” are always valid categories. The restriction in the footnote is like a grammatical rule to prevent nonsensical sentence structures from being considered valid.

---

Expressive Power is Not Reduced

[cite_start]The footnote concludes by saying this restriction doesn’t limit what the language can express: “any constructor whose kind contains strictly positive singletons or dependent sums can be given a kind (exactly as coarse) without them.” [cite: 119, 120]

This means that even if you have a complex constructor with one of these “forbidden” kinds, you can always find an alternative, simpler kind for it that is just as useful for typechecking. The system can rewrite the more complex kind into a simpler, well-behaved one without losing essential type information. It’s a way of ensuring the internal logic of the type system remains sound without sacrificing practical programming power. 🤓