language: en kae3g ← back to index
(unlisted) β€” This essay is not shown on the main index but remains accessible via direct link

kae3g 9540: Types and Sets - Mathematical Foundations of Programming

Phase 1: Foundations & Philosophy | Week 3 | Reading Time: 15 minutes

What You'll Learn

Prerequisites

What Is a Type?

Informal definition: A type is a collection of values that share common properties.

Examples:

In mathematics: Types are sets.

In programming: Types classify what operations are valid:

;; Integer: can add, multiply
(+ 3 5)  ; => 8

;; String: can concatenate, can't add
(+ "hello" "world")  ; Error! (in typed languages)
(str "hello" "world")  ; => "helloworld" (correct operation)

Types prevent nonsense operations.

Sets: The Mathematical Foundation

Set theory (Georg Cantor, 1870s) underlies all mathematicsβ€”and programming.

Basic Sets

Natural numbers: β„• = {0, 1, 2, 3, ...}

Integers: β„€ = {..., -2, -1, 0, 1, 2, ...}

Real numbers: ℝ = {Ο€, √2, -5.7, ...}

Booleans: 𝔹 = {true, false}

Set Operations

Union (A βˆͺ B): Elements in A or B

{1, 2} βˆͺ {2, 3} = {1, 2, 3}

Intersection (A ∩ B): Elements in A and B

{1, 2} ∩ {2, 3} = {2}

Cartesian Product (A Γ— B): Pairs from A and B

{1, 2} Γ— {a, b} = {(1,a), (1,b), (2,a), (2,b)}

Programming parallel:

;; Union: "or" types (we'll see this in sum types)
;; Intersection: "and" types (refinement types)
;; Product: tuples, records, structs

Types in Programming

Primitive Types

Most languages have:

Integer:  42, -17, 0
Float:    3.14, -0.5
Boolean:  true, false
Character: 'a', 'ε­—', 'πŸŒ™'
String:   "hello valley"

These are built-in. Everything else is composed from these.

Composite Types

Product types (A and B):

;; Tuple (ordered pair)
[42 "Alice"]  ; Integer AND String

;; Record/Map (labeled fields)
{:name "Alice" :age 30}  ; String AND Integer (labeled)

Product = Cartesian product (all combinations).

Sum types (A or B):

-- Haskell (has native sum types)
data Result = Success Int | Failure String

-- Value is EITHER Success(42) OR Failure("error")
-- Never both!

Sum = union (one of several options).

(Clojure doesn't have native sum types, but can encode them with maps: {:type :success :value 42})

Static vs Dynamic Typing

The great debate: Should types be checked at compile-time or runtime?

Static Typing

Examples: Java, Haskell, Rust, TypeScript

Type errors caught before running:

fn add(x: i32, y: i32) -> i32 {
    x + y
}

add(3, "hello")  // Compile error: expected i32, got &str

Pros:

Cons:

Dynamic Typing

Examples: Python, JavaScript, Clojure, Ruby

Type errors caught when code runs:

def add(x, y):
    return x + y

add(3, "hello")  # Runtime error: unsupported operand types

Pros:

Cons:

The Middle Ground

Gradual typing: Optional types (TypeScript, Python type hints, Clojure spec).

// TypeScript: add types to JavaScript
function add(x: number, y: number): number {
    return x + y;
}

add(3, 5)  // OK
add(3, "hello")  // Error!

;; Clojure spec: runtime validation
(require '[clojure.spec.alpha :as s])

(s/def ::age (s/and int? #(>= % 0)))
(s/def ::user (s/keys :req-un [::name ::age]))

(s/valid? ::user {:name "Alice" :age 30})  ; => true
(s/valid? ::user {:name "Bob" :age -5})    ; => false

Best of both worlds: Flexibility of dynamic + safety of static (when you want it).

Algebraic Data Types

"Algebraic" = composed using algebra-like operations (product, sum).

Product Types (AND)

Tuple:

-- Haskell
type Point = (Int, Int)

-- Value: (3, 5)
-- Has TWO components (x AND y)

Record:

;; Clojure
{:x 3 :y 5}

;; Has TWO labeled fields

Cardinality (size of set):

|Bool| = 2  (true, false)
|Int| = ∞  (unbounded integers)

|Bool Γ— Int| = 2 Γ— ∞ = ∞  (product = multiplication)

Sum Types (OR)

Enumeration:

// Rust
enum Status {
    Pending,
    Approved,
    Rejected
}

// Value is ONE OF: Pending OR Approved OR Rejected

Tagged union:

-- Haskell
data Maybe a = Nothing | Just a

-- Value is EITHER Nothing OR Just(value)

Cardinality:

|Status| = 3  (three options)
|Maybe Bool| = 1 + 2 = 3  (Nothing OR Just true OR Just false)

|Sum| = |A| + |B|  (sum = addition)

Why "algebraic": Types combine via arithmetic!

Types Prevent Errors

Example: Optional Values

Problem: Handling missing data.

Bad (no types, null everywhere):

function getUser(id) {
    return database.find(id);  // Might return null!
}

const user = getUser(42);
console.log(user.name);  // CRASH if user is null!

Billion-dollar mistake (Tony Hoare invented null in 1965, called it his "billion-dollar mistake").

Good (types enforce handling):

// Rust: Option type
fn get_user(id: u32) -> Option<User> {
    database.find(id)
}

match get_user(42) {
    Some(user) => println!("{}", user.name),
    None => println!("User not found")
}

// Compiler forces you to handle None case!

Even better (Haskell with Maybe):

-- Type signature documents possibility of absence
getUser :: Int -> Maybe User

-- Must pattern match
case getUser 42 of
    Just user -> userName user
    Nothing -> "Unknown"

Types make absence explicit (can't forget to check).

Function Types

Functions have types too:

-- Haskell type signature
add :: Int -> Int -> Int
add x y = x + y

-- Reads: "add takes Int, takes another Int, returns Int"

Arrow notation (β†’):

f :: A β†’ B   ; Function from A to B
g :: B β†’ C   ; Function from B to C
g ∘ f :: A β†’ C   ; Composition (feeds A to f, result to g, produces C)

This is category theory: Functions are morphisms between types (objects).

(We'll explore this in Essay 9730: Category Theory)

Higher-Order Function Types

-- map takes a function (a β†’ b) and a list [a], returns list [b]
map :: (a -> b) -> [a] -> [b]

-- Examples:
map :: (Int -> String) -> [Int] -> [String]
map show [1,2,3]  -- => ["1","2","3"]

The type signature is documentation: "Give me a transformer and a list, I'll transform every element."

The Curry-Howard Correspondence

Mind-bending connection between logic and types:

Logic           ↔  Programming
─────────────────────────────────
Proposition     ↔  Type
Proof           ↔  Program
Theorem         ↔  Type signature

"A implies B"   ↔  Function type A β†’ B
"A and B"       ↔  Product type A Γ— B  
"A or B"        ↔  Sum type A + B

Example:

Proposition: "If you give me an integer, I can give you a string."

Type: Int β†’ String

Proof: Write a function with that type!

intToString :: Int -> String
intToString n = show n

-- This program IS a proof of the proposition!

Profound implication: Programs are proofs. Types are theorems. Compiling is theorem-checking.

Constructive mathematics (build the object to prove existence) is programming!

Type Inference

Some languages infer types (you don't write them, compiler figures them out):

-- Haskell (no type annotations)
add x y = x + y

-- Compiler infers:
add :: Num a => a -> a -> a
-- "For any numeric type a, add takes a and a, returns a"

(* OCaml *)
let add x y = x + y

(* Inferred: int -> int -> int *)

Benefits:

Limitation: Complex types can be hard to infer (need annotations for clarity).

Hands-On: Type Thinking

Exercise 1: Determine Types

What are the types?

;; 1.
(defn double [x] (* 2 x))
;; Type: Number β†’ Number

;; 2.
(defn first-char [s] (first s))
;; Type: String β†’ Char (or nil if empty!)

;; 3.
(defn filter-evens [numbers]
  (filter even? numbers))
;; Type: [Number] β†’ [Number]

;; 4.
(defn apply-twice [f x]
  (f (f x)))
;; Type: (a β†’ a) β†’ a β†’ a  (higher-order!)

Think in types: Helps reason about what functions can/can't do.

Exercise 2: Type-Driven Design

Start with the type signature, then implement:

-- Want: validate user
validateUser :: User -> Either Error User

-- Either Error User means:
-- - If valid: Right User
-- - If invalid: Left Error

validateUser user =
    if age user < 0
        then Left "Negative age"
        else if null (name user)
            then Left "Missing name"
            else Right user

Type guides implementation: Return type is Either, so must return Left or Right.

Compiler enforces: Can't forget error cases.

Exercise 3: Cardinality

Calculate how many possible values:

-- 1. Bool
|Bool| = 2  (true, false)

-- 2. (Bool, Bool)
|(Bool, Bool)| = 2 Γ— 2 = 4  ((T,T), (T,F), (F,T), (F,F))

-- 3. Either Bool Bool
|Either Bool Bool| = 2 + 2 = 4  (Left T, Left F, Right T, Right F)

-- 4. Maybe Bool
|Maybe Bool| = 1 + 2 = 3  (Nothing, Just True, Just False)

Cardinality helps understand types (how many test cases do you need?).

Type Systems in Practice

Weak vs Strong Typing

Weak typing (implicit conversions):

// JavaScript
"5" + 3  // => "53" (string concatenation)
"5" - 3  // => 2 (numeric subtraction)
true + 1 // => 2 (true = 1)

Surprises! The language coerces types.

Strong typing (no implicit conversions):

# Python
"5" + 3  # TypeError: can't concatenate str and int
"5" - 3  # TypeError: unsupported operand types

# Must be explicit:
int("5") + 3  # => 8
"5" + str(3)  # => "53"

Predictable: No surprises. Type errors are loud.

Clojure (strong, dynamic):

(+ "5" 3)  ; Error: String cannot be cast to Number
(+ 5 3)    ; => 8

Nominal vs Structural Typing

Nominal (Java, C++): Types have names, names matter.

class UserId { int value; }
class ProductId { int value; }

UserId u = new UserId(42);
ProductId p = u;  // Error! Different names, even though structure is identical

Structural (TypeScript, Go): Types defined by shape, names don't matter.

// TypeScript
type Point = { x: number; y: number };
type Vec2 = { x: number; y: number };

const p: Point = { x: 3, y: 5 };
const v: Vec2 = p;  // OK! Same structure

Trade-offs:

Type Safety

Type-safe languages guarantee: No type errors at runtime (if compiler accepts, program won't crash due to type mismatch).

Sound Type Systems

Sound: If compiler accepts, no type errors will occur.

Examples: Haskell, Rust, ML

Benefits: Trust the compiler. If it compiles, types are correct.

Unsound Type Systems

Unsound: Compiler accepts, but type errors might occur.

Examples: Java (null can inhabit any type), TypeScript (explicit any escape hatch)

String s = null;  // null is "subtype" of all types (unsound!)
s.length();  // NullPointerException at runtime

Trade-off: Pragmatism (Java's null) vs purity (Haskell's Maybe).

Why Types Matter

1. Documentation

Type signature documents behavior:

map :: (a -> b) -> [a] -> [b]

-- Reads: "Give me a function from any type a to any type b,
--         and a list of a's,
--         and I'll give you a list of b's."

You know what map does without reading implementation!

2. Catch Errors Early

fn divide(x: i32, y: i32) -> i32 {
    x / y
}

divide(10, 0)  // Compiles (but crashes at runtimeβ€”division by zero)

// Better: use Option to make failure explicit
fn divide_safe(x: i32, y: i32) -> Option<i32> {
    if y == 0 {
        None
    } else {
        Some(x / y)
    }
}

// Type forces caller to handle None case!

3. Enable Refactoring

Change a type β†’ compiler finds all places that need updating.

-- Change User type
data User = User String Int  -- name, age

-- Add email field
data User = User String Int String  -- Compiler error at every usage site!

-- Must update all pattern matches (compiler guides you)

Without types: Must manually search, might miss some usages.

4. Guide Design

Types constrain what you can build (in a good way).

-- Can't compile this:
reverse :: [a] -> [a]
reverse list = 42  -- Error! Returns Int, but signature says [a]

-- Must implement correctly:
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]

Types force correctness.

Practical Type Wisdom

When to Use Static Typing

Choose static types when:

Examples: Rust (systems programming), Haskell (finance, compilers), TypeScript (large JS projects)

When to Use Dynamic Typing

Choose dynamic types when:

Examples: Python (data science, scripting), Clojure (REPL-driven web apps), JavaScript (small projects)

The Valley's Position

We use both:

Principle: Choose the right tool. No dogma. Evaluate trade-offs.

Try This

Exercise 1: Type Signatures in Your Head

For functions you write, think about types:

# Python (dynamic, but think in types)
def process_orders(orders):
    return [o for o in orders if o['total'] > 100]

# Type (imaginary): [Order] -> [Order]
# Constraint: orders must have 'total' field (partial function!)

Better (make constraint explicit):

def process_orders(orders: List[Order]) -> List[Order]:
    return [o for o in orders if o.total > 100]

Type annotations help even in dynamic languages (documentation + IDE support).

Exercise 2: Design with Types

Problem: Represent a traffic light.

Bad (stringly-typed):

(def light "red")  ; What if someone writes "blue"?

Good (keyword enum):

(def light :red)  ; One of: :red, :yellow, :green

(defn next-light [light]
  (case light
    :red :green
    :yellow :red
    :green :yellow))

Even better (Rust with enums):

enum Light { Red, Yellow, Green }

fn next_light(light: Light) -> Light {
    match light {
        Light::Red => Light::Green,
        Light::Yellow => Light::Red,
        Light::Green => Light::Yellow,
    }
}

// Compiler ensures: all cases handled!

Exercise 3: Explore clojure.spec

(require '[clojure.spec.alpha :as s])

;; Define specs (types, but at runtime)
(s/def ::age (s/and int? #(>= % 0) #(<= % 150)))
(s/def ::email (s/and string? #(re-matches #".+@.+" %)))
(s/def ::user (s/keys :req-un [::age ::email]))

;; Validate
(s/valid? ::user {:age 30 :email "alice@example.com"})  ; => true
(s/valid? ::user {:age -5 :email "invalid"})  ; => false

;; Explain why invalid
(s/explain ::user {:age -5 :email "invalid"})
; -5 - failed: (>= % 0)
; "invalid" - failed: (re-matches #".+@.+" %)

Gradual typing: Add specs where you want validation, skip where you want flexibility.

Going Deeper

Related Essays

External Resources

For the Mathematically Curious

Reflection Questions

  1. Are types primarily for the compiler or for humans? (Both! But which matters more?)
  2. Is dynamic typing "simpler" than static typing? (Depends on definition of simpleβ€”fewer language features, but more runtime complexity)
  3. Should all programs be formally verified? (Ideal but impracticalβ€”what's the trade-off?)
  4. Can types replace tests? (Noβ€”but they eliminate whole classes of tests)
  5. Is TypeScript worth it for JavaScript projects? (Depends on size, team, longevity)

Summary

Types are:

Key Concepts:

Benefits:

Trade-offs:

In the Valley:

Next: We'll explore the command lineβ€”your primary interface to Unix systems, where you'll apply the text-oriented, compositional thinking we've been building!

Navigation:
← Previous: 9530 (rich hickey simple made easy) | Phase 1 Index | Next: 9550 (command line your primary interface)

Metadata:

Copyright Β© 2025 kae3g | Dual-licensed under Apache-2.0 / MIT
Competitive technology in service of clarity and beauty

← back to index