Record Type

Definition

A record type (also called a struct in some languages) is a Product Type where each field is named rather than accessed by position. A record with fields ${\ell }_1,{\ell }_2,\dots ,{\ell }_n$ and corresponding types $A_1,A_2,\dots ,A_n$ has type:

$\{{\ell }_1:A_1,{\ell }_2:A_2,\dots ,{\ell }_n:A_n\}$

Type-Theoretic Perspective

Record types have:

• Introduction rule: Given values $a_1:A_1,\dots ,a_n:A_n$, we can form $\{{\ell }_1=a_1,\dots ,{\ell }_n=a_n\}$
• Elimination rules: Field projection $r.{\ell }_i$ extracts the value of field ${\ell }_i$ from record $r$

Unlike ordered tuples, records are accessed by field name rather than position, making them more robust to reordering.

Examples

In various type systems:

• A point record: $\{x:\mathbb{R},y:\mathbb{R}\}$
• A person record: $\{\text{name}:\text{String},\text{age}:\mathbb{N},\text{email}:\text{String}\}$

Properties

• Field access is by name: $r.{\ell }_i$ extracts field ${\ell }_i$
• Field order in the type is typically irrelevant for equality
• Records can be nested: fields may themselves be records
• Some type systems support row polymorphism for extensible records

Related Concepts

• Product Type: The underlying type-theoretic structure
• Ordered Tuple: Records without named fields
• Dependent Pair: Generalization where types may depend on values
• Sum Type: The dual to record types