Quote from AntC on November 4, 2025, 10:57 am

Tuples are (Cartesian) Product types [Codd 1970 §1.3, footnote 1]. In TTM tuples, each factor of the Product type is tagged with a label [Codd's role name].

Within type theory, the counterpart of Product types is 'Sum types' aka 'tagged/disjoint/discriminated union'. I want to focus on the sub-category variant type:

Each variant has a name, called a constructor, which can also carry data.

A shape type could be either a Circle (which stores a radius) or a Square (which stores a width).

[or a Rectangle (which holds both width and height), etc]

• The data carried might be at different types for different constructors. (A different domain, in Codd terminology.)
• There might be a different number of sub-fields for different constructors. (A different degree.)

In TTM, this can be represented as labelled fields/nested tuples all the way down:

circA := {Centroid {X 1, Y 2}, Shape {Circle {Radius 3}} }
squB  := {Centroid {X 4, Y 5}, Shape {Square {Width  6}} }
rectC := {Centroid {X 7, Y 8}, Shape {Rectangle {Width 9, Height 10}} }
// there are probably other fields, or at least the tuples might get Extended with (say) Colour. // this design is (arguably) over-fussy -- which I'll argue below

Suppose we want to apply some function to a variant type (say calculate the Shape's Area). It needs to discriminate by tag/label/Constructor to choose a different calculation depending on the applicable sub-fields, and do that type-safely -- that is, not request the Radius for a Square. Programming languages typically use discriminated despatch via a case or switch construct, or similar:

def area s = case s.Shape of                     // using dot notation to extract a field via label
    {Circle {Radius r}}   = pi * r ^ 2           // LHS using a 'pattern match' to bind var r
    {Square squ}          = squ.Width ^ 2        // combo of pattern match with field access
    {Rectangle {...}}     = ...

The squ.Width access is type safe (can't fail at run time) because we know squ is the subfield of a Square-tagged tuple.

First Observation: this makes the field labels not arbitrary, but part of the type of each (sub-)tuple. The benefit we get is type-safe access. The downside is we must pre-declare Shape as a variant type with fixed, known choice of tags.

Second observation: the case construct and its branches is rather hard-coded/not easily extensible as different Shapes (Triangle, Rhombus, ...) get added to the 'business area'.

It's common for the case construct to have a 'catchall'/default/otherwise branch for expressions not matching any of the explicit tags. OTOH many style guides warn against this practice as a frequent cause of run-time misery. It's too easy to add an extra tag to Shape's declaration, but not add it to all the cases that despatch on Shape.

Indeed this overbearing bondage-and-discipline was evident back at the tuple values (in DRY terms the tag Shape is repeating what we already know from the appearance of Circle/Square/Rectangle). I'd rather write those tuples more succinctly as:

circA := {Centroid {X 1, Y 2}, Circle {Radius 3}}  
squB :=  {Centroid {X 4, Y 5}, Square {Width 6}} 
rectC := {Centroid {X 7, Y 8}, Rectangle {Width 9, Height 10}} 
// Note that still the label is part of the type for each record, per First Observation

And I'd rather write the case branches as a set of pairings label-function -- indeed as a tuple:

areaCase := {Circle (λ{Radius r} -> pi * r ^ 2),
             Square (λsqu        -> squ.Width ^ 2),
             Rectangle (λ{...}   -> ...)
            }

• areaCase is a tuple (fields written vertically).
• The set of labels correspond to the possible Constructors for Shape.
• The (λ   ->   ) is functional programming's 'anonymous function' lambda expression: bind the vars appearing under the λ, reference them in the expression on RHS of the ->.
• And we need a caseApply operator (which I'll spell ??): circA ?? areaCase returns the area for circA's shape, discriminating by the appearance of the Circle label/Constructor.
• This is type-safe (won't fail at run-time) because we can statically check circA includes a label that appears amongst those in areaCase.
• Or type-rejection if they have no label in common;
• just as much type-rejection if there's not a unique label in common.
• Because areaCase is a (first-class) tuple, we can EXTEND it to cater for further Shapes.
• Or if we add further Shapes but forget to add corresponding cases, triangleD ?? areaCase gets type-rejected.

Is this demanding pie-in-the-sky type theory? This 1998 thesis implemented the idea [Chapter 7.3 Casting, and ff]. I have a (crude) prototype running in a Haskell.