Day 44 — Types/sets analogy

Day 44 — Types/sets analogy

Stage IV · concept day
Goal: Treat types as sets of values (working analogy); connect product and sum types to \(\times\) and \(\sqcup\); model option/maybe; view predicates as subsets; separate specification from implementation—no coding labs.

Why this matters

Type systems are the industry face of sets, products, unions, and functions \(A\to B\). Thinking “what values inhabit this type?” prevents whole classes of bugs. Option types are “set plus a missing tag”; records are products; enums with data are disjoint unions. This day is conceptual glue between Stage IV math and programming languages—not a tutorial in any one language.

Theory

Types as sets of values (working model)

A type \(T\) determines a set of inhabiting values \([\![T]\!]\) (denotation).
Examples (idealized):

Type idea	Set of values
Bool	\(\{\mathsf{true},\mathsf{false}\}\)
Unit / ()	\(\{ \ast \}\) one point
Void / Never	\(\emptyset\)
Nat	\(\mathbb{N}\)
Byte	\(\{0,\ldots,255\}\)

Caveats: real languages have nontermination, mutability, subtyping, and infinite values (streams). The set model is a map, not the full semantics. Still invaluable.

Product types

A product type \(A \times B\) (struct with fields of types \(A\) and \(B\); tuple) has values that are pairs:
\[[\![A \times B]\!] = [\![A]\!] \times [\![B]\!].\]
\(n\)-ary records ≈ \(n\)-fold products.
Pattern match / field access ≈ projections \(\pi_i\).

Sum types (disjoint union)

A sum type \(A + B\) (enum / variant / tagged union):
\[[\![A + B]\!] = [\![A]\!] \sqcup [\![B]\!] = (\{0\}\times[\![A]\!]) \cup (\{1\}\times[\![B]\!]).\]
Values are either left \(A\) or right \(B\), tagged so the cases do not smash when \([\![A]\!]\cap[\![B]\!]\neq\emptyset\).

Examples: enum Result { Ok(T), Err(E) }; Left/Right; JSON oneOf.

Function types

\([\![A \to B]\!]\) idealized as the set of all functions \([\![A]\!]\to[\![B]\!]\), size \(|B|^{|A|}\) when finite.
In total functional languages, closer to math functions; in general languages, includes partial/nonterminating “functions.”

Option / Maybe

\[\mathsf{Option}(A) \cong A + 1\]
where \(1\) is unit type (“None”).
Values: \(\mathsf{Some}(a)\) for \(a\in[\![A]\!]\), or \(\mathsf{None}\).

Models missing data without null conflation: \([\![A]\!]\cup\{\mathsf{null}\}\) is a sum if null ∉ \(A\), but historically untagged null was unsafe.

Predicates as subsets

A predicate \(P\) on \(A\) defines \(\{ x\in [\![A]\!] : P(x) \}\)—a refinement / subset type idea.
Examples: { n: Nat | n > 0 }, sorted arrays as subset of arrays.
Dependent/refinement type systems make this static; in ordinary languages, it lives in docs and runtime checks.

Specs vs implementation

• Specification: mathematical relation/predicate on inputs-outputs (e.g. \(\forall x,\; f(x)^2 = x\) on nonnegatives for sqrt).
  
• Implementation: particular algorithm/function inhabiting a type \(A\to B\) claimed to satisfy the spec.

Multiple implementations may share a type and even a spec (quicksort vs mergesort: both \(List\to List\) sorted permutation).
Type correctness ≠ full functional correctness—types are coarse specs.

Subtyping (awareness)

\(S\) subtype of \(T\) suggests \([\![S]\!]\subseteq[\![T]\!]\) (simplified).
Variance rules for \(A\to B\) are subtle (contravariance in \(A\))—awareness only.

Algebra of types (arithmetic analogy)

Rough finite counts:

• \(|A\times B| = |A|\cdot|B|\)
  
• \(|A+B| = |A|+|B|\)
  
• \(|A\to B| = |B|^{|A|}\)
  
• \(|\mathsf{Option}(A)| = |A|+1\)

This is why people write type algebra \(A\cdot B\), \(A+B\), \(B^A\).

Recursive types (awareness)

List(A) ≅ 1 + A × List(A) — least fixed point; matches structural induction Day 32.

Worked examples

Example 1 — Bool

Two values; not: Bool → Bool is a function on a \(2\)-set; \(2^2=4\) possible truth functions.

Example 2 — Pair

(Int, Bool) has values like (3, true); projections.

Example 3 — Either

Result<String, ErrorCode>: success string or error—not both, not neither.

Example 4 — Option

Option<User>: logged-in user or absent—force case analysis.

Example 5 — Predicate subset

Even integers \(\subset \mathbb{Z}\); type Even as refinement.

Example 6 — Spec vs type

Type of sort: List[int] → List[int]. Spec: output sorted multiset-equal to input. Type alone allows reverse or constant list.

Example 7 — Void

No values; a function Void → A is unique (empty function) if allowed—logical ex falso vibe.

Example 8 — Unit

One value; A → Unit has one total function (ignore input)—void returning unit.

Example 9 — Counting

Byte → Bool has \(2^{256}\) mathematical functions—not all written as programs.

Example 10 — Sum not union

Untagged Int ∪ Bool if both encode as bits can confuse; tags disambiguate.

Example 11 — Product of options

Option(A)×Option(B) vs Option(A×B): different—\((None, Some(b))\) vs missing pair.

Example 12 — JSON schema

object with required fields ≈ product; enum ≈ sum of units; optional field ≈ option.

Example 13 — List recursion

[] or cons(h,t) matches \(1 + A\times L\).

Example 14 — Pipeline types

\(f:A\to B\), \(g:B\to C\) compose when types match—Day 42 with type-checker enforcement.

Exercises

1. Give \([\![Bool]\!]\), \([\![Unit]\!]\), idealized \([\![Byte]\!]\).
   
2. Explain why \(A+A \not\cong A\) in general as types/sets.
   
3. Write \(\mathsf{Option}(A)\) as a sum.
   
4. How many values does Bool × Bool have? Bool + Bool?
   
5. How many mathematical functions Bool → Bool?
   
6. Why is null dangerous as untagged inhabitant of every type?
   
7. Distinguish type of sort from its full spec.
   
8. Model a coin-flip outcome as a sum type.
   
9. Model a 2D point as a product.
   
10. Option(Option(A)) vs Option(A)—different? Give values.
    
11. Translate: “function that may fail” as \(A\to (B+E)\).
    
12. List recursive equation for binary trees.
    
13. If \(|A|=2\), \(|B|=3\), compute \(|A\times B|\), \(|A+B|\), \(|A\to B|\).
    
14. Spec: f is inverse of g—write with composition.
    
15. Subset type: positive integers as \(\{n\in\mathbb{Z}: n>0\}\).
    
16. Why \(|A\to B| = |B|^{|A|}\) matches function counting Day 41?
    
17. Explain product vs sum for “name and age” vs “name or age.”
    
18. Is every element of \(A\to B\) (math) a possible program? Why not (countability)?
    
19. Model HTTP method as a finite sum of units (GET+POST+…).
    
20. Result type: show map as a function \((A\to B)\to (A+E)\to(B+E)\) conceptually.
    
21. Compare \(A\times(B+C)\) and \((A\times B)+(A\times C)\)—isomorphic?
    
22. Spec vs impl: two different algorithms inhabiting same type and spec.
    
23. What set is the denotation of an empty enum?
    
24. Explain tagging: why \(\{0\}\times A \cup \{1\}\times B\) not just \(A\cup B\).
    
25. One paragraph: how Stage IV sets/products/sums appear in the type system you use most.

CS connection

• Static types catch \(\in\) errors before runtime.
  
• Algebraic data types = products + sums + recursion.
  
• Null safety / option types = explicit sums.
  
• API design: product request bodies; sum error codes.
  
• Formal verification strengthens types toward full specs.
  
• Generics ≈ families of sets indexed by types (parametricity awareness).

Common pitfalls

Pitfall	What to do instead
Types = full specs	Types are coarse invariants
Union vs tagged sum	Prefer tagged for safety
Option(A×B) vs product of options	Different shapes
Ignoring nontermination	Set model is partial truth
Counting programs as all functions	Only countable programs
Forcing one language’s syntax	Keep conceptual

Checkpoint

• Types as sets: examples
  
• Product ↔︎ \(\times\), sum ↔︎ \(\sqcup\)
  
• Option as \(A+1\)
  
• Predicate as subset
  
• Spec vs type vs implementation
  
• Type arithmetic for finite sizes
  
• Exercises done or logged

Two takeaways:

1. …
   
2. …

Deep dive — ADT equations as set equations

Solving \(L = 1 + A\times L\) in finite sets only for free when infinite structures allowed—lists are the least fixed point of \(F(X)=1+A\times X\) in domain theory/set theory with infinity. Finite approximations: lists of length \(\le n\).

Homomorphisms (awareness)

A function \(h: List(A)\to B\) is determined by \(h(\mathrm{nil})\) and a step \(A\times B\to B\) (fold). Structural recursion = unique map out of an initial algebra—vocabulary for later PL theory.

Specs layered

Layer	Example
Type	int → int
Refinement	maps nonneg to nonneg
Full contract	\(f(n)=n(n+1)/2\) for \(n\ge 0\)
Complexity	\(O(1)\) arithmetic ops

Types catch layer 1; tests approximate lower layers; proofs cover contracts.

More worked examples

Example 15 — Either count
\(|A+B|=|A|+|B|\) with tags; if untagged union and \(A,B\) overlap, count less.

Example 16 — Callback type
\((A\to B)\to C\) as nested function type—set of functionals.

Example 17 — Maybe map
\(\mathrm{map}: (A\to B)\to (A+1)\to(B+1)\).

Example 18 — Void absurd
No closed term of type Void in total languages—empty set.

Additional exercises

26. Count values of Bool → Option(Bool).
    
27. Isomorphism sketch: \(A\times(B+C)\cong (A\times B)+(A\times C)\).
    
28. Spec for max: List[int]→int including empty-list behavior as Option.
    
29. Explain subtyping Cat ⊆ Animal vs function variance one sentence.
    
30. Write denotations for a tiny enum enum Color { R, G, B }.

Extended practice workshop

Denotation drills

1. \([\![Bool]\!]\), \([\![Unit]\!]\), \([\![Void]\!]\)
   
2. \([\![Bool\times Bool]\!]\) count
   
3. \([\![Bool+Bool]\!]\) count
   
4. \([\![Bool\to Bool]\!]\) count
   
5. \([\![Option(Byte)]\!]\) count idealized

Modeling drills

6. Product type for {x: int, y: int}.
   
7. Sum type for success/error.
   
8. Option for missing user.
   
9. Result[T,E] as sum.
   
10. Recursive list equation.

Spec vs type

11. Type of sort vs full sort contract.
    
12. Type of sqrt vs domain restriction.
    
13. Two algorithms same type and contract.
    
14. Type-correct but wrong program example (English).

Algebra

15. \(|A\times(B+C)|\) vs \(|(A\times B)+(A\times C)|\)
    
16. \(|A\to B\times C|\) vs \(|(A\to B)\times(A\to C)|\)
    
17. \(Option(A\times B)\) vs \(Option(A)\times Option(B)\)—compare

CS design

18. Why tagged unions beat untagged null.
    
19. JSON schema object ≈ product; oneOf ≈ sum.
    
20. API: product request body; sum error codes.

Layer cake

full proof of contract
        ↑
   tests / property tests
        ↑
 refinement types (optional)
        ↑
    static types  ← you are here often
        ↑
      raw bits

Synthesis

Types are sets of values with operations, and type constructors are set constructions: product \(\times\), sum \(+\), function space \(A\to B\), option \(A+1\). Static types catch a slice of bugs; full contracts (sortedness, bounds) are predicates—subsets of the typed value space. This day is conceptual glue between Stage IV sets and real programming languages—not a coding lab.

Denotation dictionary

Type idea	Set-theoretic denotation (idealized)
Bool	\(\{0,1\}\) or \(\{\mathsf{tt},\mathsf{ff}\}\)
Unit	\(1=\{\ast\}\)
Void / never	\(0=\emptyset\)
\(A\times B\)	cartesian product
\(A+B\)	disjoint union \(A\sqcup B\)
\(A\to B\)	set of functions
Option(A)	\(A+1\)
List(A)	\(\bigcup_n A^n\) (or initial algebra awareness)

More worked examples

Example — Counts.
\(|Bool\times Bool|=4\), \(|Bool+Bool|=4\), \(|Bool\to Bool|=4\). Same cardinality, different structure (pairing vs tagging vs maps).

Example — Option vs nullable.
Option(A) forces a tag: \(\mathsf{None}\) or \(\mathsf{Some}(a)\). Untagged null confuses “no value” with a value that happens to be null-ish—sum types beat untagged bottoms.

Example — Spec finer than type.
Type of sort: List[Int] → List[Int]. Contract: output permutation of input and nondecreasing. Many type-correct functions violate the contract.

Example — Distributivity iso.
\(A\times(B+C)\cong (A\times B)+(A\times C)\): a pair of an \(A\) and a tagged \(B\) or \(C\) is a tagged pair. Counts match: \(|A|(|B|+|C|)=|A||B|+|A||C|\).

Example — Function into product.
\(A\to(B\times C)\cong (A\to B)\times(A\to C)\): giving both components separately. Curry: \(A\times B\to C \cong A\to(B\to C)\) (exponential).

Extra exercises (synthesis)

31. Idealized count: \(|Byte\to Bool|\) if \(|Byte|=256\).
    
32. Write denotation of Result[T,E] as a sum.
    
33. Why \(Option(A\times B)\not\cong Option(A)\times Option(B)\) (counterexample elements).
    
34. Spec: div: Int × Int → Option(Int) for division by zero—type vs total function on pairs with nonzero second.
    
35. Explain subtyping \(A\subseteq B\) for values vs variance of \(A\to C\) (contravariance awareness in one sentence).
    
36. JSON: object fields ≈ product; oneOf ≈ sum—give a tiny schema example in English.

Spec vs type checklist

Layer	Catches
Type \(f:A\to B\)	Wrong shape of data
Predicate subset \(P\subseteq A\)	Domain restrictions
Full Hoare contract	Pre/post relationships
Tests	Some counterexamples to \(\forall\)

Types are not proofs of full correctness—but they are set-level invariants the compiler checks. Tomorrow: forcing collisions and crowded holes with the pigeonhole principle.

Tomorrow

Day 45 — Pigeonhole principle. Basic + generalized; Dirichlet; collisions, birthday bound, hair/friends, Erdős–Szekeres statement, modular pigeon.