Dependent products: Sigma types

A dependent product stores fields where a later field’s type may mention an earlier value. In the two-field mathematical view this is a Sigma type; tulam generalizes it directly to an n-ary telescope.

A length-indexed package

type SizedVector(a:Type) =
    size:Nat * values:Vec(a,size);

The constructor checks size first and uses its accepted value while checking values. Projection preserves the relationship:

function contents[a:Type](item:SizedVector(a))
    : Vec(a,item.size) = item.values;

Type-expression form

(n:Nat) * Vec(a,n)

The name n scopes over the second component. Longer products remain one flat telescope:

(rows:Nat) * (cols:Nat) * Matrix(a,rows,cols)

They are not compiler-generated binary Sigma chains.

Explicit nesting

{rows, cols, matrix}
{rows, {cols, matrix}}

The first is one three-field value. The second is a two-field value whose second field is nested. Checking, layout, reflection, and debugging preserve the difference.

Sigma packages and existentials

A visible Sigma exposes its witness for projection. exists hides the witness behind an abstraction boundary:

exists (a:Type). { value:a, display:a -> String }

Both use the same dependent product foundation; Chapter 17 explains the escape rule introduced by hiding the witness.

Representation

Erased fields and runtime fields are connected by one stable map. Backends may unbox or scalar-replace values but may not reconstruct a different semantic pair tree. The LLVM provider’s current 255-retained-field limit is a layout constraint, not a Sigma-type restriction.

Practical uses

Sigma values package a value with evidence or metadata that depends on it: dimensions with storage, a target profile with a handle of that profile, or a type with operations valid for that type.

Common mistakes

Do not reassociate a flat telescope into nested binary products, and do not hide a witness with exists when callers need to project it. Explicit nesting is meaningful and must remain visible.

Recap

A Sigma type stores a witness and data whose type depends on that witness. tulam preserves the same ordered n-ary telescope from checking through runtime layout.

Normative details: Language Reference §4.4.