# the algebra of dependent types

DevFeed: [the algebra of dependent types](<https://devfeed.tech/articles/the-algebra-of-dependent-types-36214.md>)

Original publisher: [Read original article](<https://dotat.at/@/2025-05-28-types.html>)

Published: 2025-05-29T00:07:51Z

Content type: article

Language: en

Sources: [Tony Finch's blog](<https://devfeed.tech/sources/tony-finch-s-blog.md>)

Topics: [Programming](<https://devfeed.tech/topics/programming.md>), [Functional programming](<https://devfeed.tech/topics/functional-programming.md>), [Standard ML](<https://devfeed.tech/topics/standard-ml.md>), [Rust](<https://devfeed.tech/topics/rust.md>)

Tags: [algebra](<https://devfeed.tech/tags/algebra.md>), [enum](<https://devfeed.tech/tags/enum.md>), [functional-programming](<https://devfeed.tech/tags/functional-programming.md>), [languages](<https://devfeed.tech/tags/languages.md>), [programming-languages](<https://devfeed.tech/tags/programming-languages.md>), [type-system](<https://devfeed.tech/tags/type-system.md>), [type-theory](<https://devfeed.tech/tags/type-theory.md>), [types](<https://devfeed.tech/tags/types.md>)

## AI overview

An explanation of why big-sigma and big-pi notation appears in dependent type theory. It connects dependent functions and dependent pairs to algebraic data types, showing how products correspond to multiplication and sum types to addition, with examples from type theory, Standard ML, Haskell, and Rust.

## Source excerpt

TIL (or this week-ish I learned) why big-sigma and big-pi turn up in the notation of dependent type theory. I've long been aware of the zoo of more obscure Greek letters that turn up in papers about type system features of functional programming languages, μ, Λ, Π, Σ. Their meaning is usually clear from context but the reason for the choice of notation is usually not explained. I recently stumbled on an explanation for Π (dependent functions) and Σ (dependent pairs) which turn out to be nicer than I expected, and closely related to every-day algebraic data types. sizes of types The easiest way to understand algebraic data types is by counting the inhabitants of a type. For example: the unit type () has one inhabitant, (), and the number 1 is why it's called the unit type; the bool type hass two inhabitants, false and true. I have even seen these types called 1 and 2 (cruelly, without explanation) in occasional papers. product types Or pairs or (more generally) tuples or records. Usually written, (A, B) The pair contains an A and a B, so the number of possible values is the number of possible A values multiplied by the number of possible B values. So it is spelled in type theory (and in Standard ML) like, A * B sum types Or disjoint union, or variant record. Declared in Haskell like, data Either a b = Left a | Right b Or in Rust like, enum Either<A, B> { Left(A), Right(B), } A value of the type is either an A or a B, so the number of possible values is the number of A values plus the number of B values. So it is spelled in type theory like, A + B dependent pairs In a dependent pair, the type of the second element depends on the value of the first. The classic example is a slice, roughly, struct IntSlice { len: usize, elem: &[i64; len], } (This might look a bit circular, but the idea is that an array [i64; N] must be told how big it is - its size is an explicit part of its type - but an IntSlice knows its own size. The traditional dependent "vector" type is a sized li