Sigma Types in Procedural Languages

I'm exploring how to embed dependent type theory features into a compiled procedural language. I've already stumbled into Σ-types represent dependent pairs where the type of the second value depends on the value of the first. These are naturally unrepresentable in Python, C++, C, Rust, etc.

A Sigma type is written:

\[ Σ (x : A). B(x) \]

This denotes the type of pairs \( (a, b) \) where:

\[ a : A \] \[ b : B(a) \]

It’s the dependent analogue of a pair or tuple, but with extra expressiveness: the second value is type-indexed by the first.

What would Σ-types look like in procedural languages?

Classical procedural languages lack the mathematical expressiveness to compose such dynamics. Furthermore, procedural languages rely heavily on static memory layouts and predictable compilation paths which don't translate well into such a dynamic type system.

If we imagined that python was dependently typed, this is what it might look like:

# Σ (x: int) . List[bool]
type MySigmaType = Tuple[x, List[bool]] 
# where the List will have length x

x: MySigmaType = (1, [False])
y: MySigmaType = (2, [True,False])

many: List[MySigmaType] = [
    (1, [False]),
    (1, [True]),
    (2, [False,False])
]

Importantly, the list many contains items all of the same type. Furthermore, notice that MySigmaType doesn't take a type parameter. This is because MySigmaType isn't a template type like we find in C++. Instead, values of type MySigmaType, are themselves, a pair for which the second element is a different type. The fact that the type of values can depend on other values is what a dependent type system apart.

When B(x) Gets Weird

Recall that \( Σ (x : A). B(x) \) equates to \( (a : A, b : B(a) ) \).

So \( B(a) \) is a function that maps an \( A \) to some type:

\[ B : A \to \mathbb{T} \]

Where \( \mathbb{T} \) is the set of all types \( T \in \mathbb{T} \).

Piecewise Type Families

Now imagine a more exotic \( B(x) \):

\[ B(x) = \text{if } x = 1 \text{ then } \texttt{int}\text{ else } \texttt{string} \]

This is still a valid type family \( T \in \mathbb{T} \). We could write:

\[ \Sigma (x : \mathbb{N}). B(x) \]

This creates a type whose second component can dynamically switch between int and string, depending on the runtime value of x.

It’s totally valid in type theory. But...

The Problem of Indeterminate Size

This kind of Σ (x : ℕ). B(x) becomes a problem when you try to implement it in a procedural language. Why?

Because the compiler can't determine the memory layout ahead of time. It doesn’t know whether to allocate an int or a string.

In type theory, there's no need to lay out memory. We care only about logical correctness, type soundness, and proof construction. The size of B(x) is irrelevant—it could be metaphysically infinite for all we care.

But procedural languages are built around memory layout, type predictability, and compile-time constraints. We need to know what a value looks like in memory before we can build or call it.

Sizeably Sane Functors

We wish to define a constrained set of \( B(x) \) that avoids this issue. However, defining the property of sizeable sanity mathematically is non-trivial.

What precisely does it mean to be a uniform mapping of types?

A proposed definition of type map uniformity

This leads to the idea that only a restricted class of Sigma types—ones where:

• B(x) is injective,
• B(x) preserves structural or ordering uniformity,
• and where x can be recovered statically from the type of B(x)