Advanced Type Features

An algebraic data type is a type built by combining other types using two fundamental operations: product ("and") and sum ("or"). The name comes from the fact that the number of possible values of a composite type follows algebraic rules — products multiply, sums add.

Product types ("and"): A value of a product type contains one value of each component type simultaneously. A Point = (Float, Float) is a product: every point has both an x-coordinate and a y-coordinate. In Haskell, data Pair a b = Pair a b — the type Pair Int Bool has |Int| × |Bool| = infinitely many values.

Sum types ("or"): A value of a sum type contains exactly one of several alternatives. data Shape = Circle Float | Rectangle Float Float — a shape is either a circle with a radius or a rectangle with width and height. The number of values is |Circle values| + |Rectangle values|, hence "sum".

ADTs are recursive: data List a = Nil | Cons a (List a) — a list is either empty (Nil) or a head element followed by a tail list. This simple definition gives you singly-linked lists, and pattern matching on it gives you virtually all list algorithms.

Why ADTs matter: they force you to enumerate the possible shapes of your data. In a language without sum types (like Java before sealed classes), you might represent a shape as an interface with many implementations — but the type system cannot tell you whether you've handled every case. ADTs move that check to compile time. You cannot forget to handle Nil because the compiler will warn about a non-exhaustive pattern match.

Real-world payoff: Rust's Option<T> (= Some(T) | None) and Result<T, E> (= Ok(T) | Err(E)) are sum types. They make null-pointer exceptions and unhandled errors impossible to express — you must explicitly handle both branches.

-- Haskell: A small expression language as an ADT
data Expr
  = Lit Int            -- literal number
  | Add Expr Expr      -- addition
  | Mul Expr Expr      -- multiplication
  | IfZero Expr Expr Expr  -- if e1==0 then e2 else e3

-- Evaluate: the type guarantees every case is handled
eval :: Expr -> Int
eval (Lit n)         = n
eval (Add e1 e2)     = eval e1 + eval e2
eval (Mul e1 e2)     = eval e1 * eval e2
eval (IfZero c t f)  = if eval c == 0 then eval t else eval f

-- Example: (2 + 3) * 4
example :: Expr
example = Mul (Add (Lit 2) (Lit 3)) (Lit 4)
-- eval example == 20

Pattern matching is the mechanism for destructuring algebraic data types — inspecting which variant a sum type holds and binding the contained values to names. It is to ADTs what field access is to structs, but it is exhaustive (the compiler checks you cover every case) and safe (no casting required).

A pattern is a structural description of a value. Cons x xs is a pattern that matches any non-empty list, binding the head to x and the tail to xs. [] (or Nil) matches the empty list. The compiler checks that the set of patterns is exhaustive (covers all cases) and warns about redundant patterns (unreachable cases).

Nested patterns let you match deeply into a structure in one step. Cons x (Cons y _) matches a list with at least two elements, binding the first two.

Guards add boolean conditions to patterns: | x > 0 = ... after a pattern fires only if the guard is satisfied.

Pattern matching in modern languages: Rust's match is essentially Haskell's case expression. Python 3.10+ added structural pattern matching (match/case). Scala has match. Even C++'s std::visit over std::variant is a workaround for the lack of first-class pattern matching.

The deep connection: pattern matching is the eliminator for a sum type. Every sum type A | B | C has a canonical eliminator that says "give me a function for each variant, and I'll give you a function from the sum type to any result". Pattern matching is syntactic sugar for this eliminator, and exhaustiveness checking ensures the eliminator is total — defined on every possible input.

Performance: compilers (especially ML/Haskell compilers) compile pattern matches to efficient decision trees, often outperforming hand-written chains of if-else.

-- Haskell: pattern matching on a recursive ADT
data Tree a = Leaf | Node (Tree a) a (Tree a)

-- depth: maximum depth of the tree
depth :: Tree a -> Int
depth Leaf           = 0
depth (Node l _ r)   = 1 + max (depth l) (depth r)

-- inorder traversal with nested patterns
inorder :: Tree a -> [a]
inorder Leaf           = []
inorder (Node l x r)   = inorder l ++ [x] ++ inorder r

-- Rust equivalent (for comparison):
-- enum Tree<T> { Leaf, Node(Box<Tree<T>>, T, Box<Tree<T>>) }
-- fn depth<T>(t: &Tree<T>) -> usize {
--   match t {
--     Tree::Leaf => 0,
--     Tree::Node(l, _, r) => 1 + depth(l).max(depth(r)),
--   }
-- }

Parametric polymorphism (called generics in most languages) lets you write a single function or type that works uniformly for any type, without knowing what that type is. The canonical example is identity :: a -> a in Haskell: for any type a, given a value of type a, return it unchanged. The function cannot do anything with the value — it doesn't know what type it is — so the only thing it can return is the value it was given. The type signature proves the implementation.

This is John Reynolds's parametricity theorem (1983): a parametrically polymorphic function must act uniformly across all types. This gives you "theorems for free" — you can prove properties of a function from its type alone, before seeing its code. For example, any function f :: [a] -> [a] can only rearrange, drop, or duplicate elements — it cannot create new ones because it doesn't know what type a is.

In Haskell: data Maybe a = Nothing | Just a — the type parameter a is a placeholder. fmap :: (a -> b) -> Maybe a -> Maybe b works for any a and b.

In Rust: fn largest<T: PartialOrd>(list: &[T]) -> &T — the type parameter T is constrained by the trait PartialOrd. Rust (and Haskell's typeclasses) uses bounded parametric polymorphism: you can require the type to implement certain interfaces.

In Java/C#: generics were added later and are implemented via erasure — the type parameter is erased at compile time. This means List<Integer> and List<String> share the same runtime representation, which enables some compatibility but prevents runtime type inspection.

In C++: templates are a form of generics but with duck typing — the constraints are not checked until instantiation. C++20 Concepts bring explicit constraints.

The key insight: parametric polymorphism is the mechanism for code reuse at the type level. Instead of writing sortInts, sortStrings, and sortShapes separately, you write sort :: Ord a => [a] -> [a] once.

-- Haskell: parametric polymorphism + typeclasses
-- fmap works for any Functor, any type a -> b
fmap :: Functor f => (a -> b) -> f a -> f b

-- "Free theorem": any function reverse-like :: [a] -> [a]
-- satisfies: map f . reverse == reverse . map f
-- Proof comes from the TYPE alone, not the implementation.

-- Rust bounded generics:
use std::fmt::Display;

fn print_twice<T: Display>(x: T) {
    println!("{} {}", x, x);
}
// Works for i32, f64, String, any type implementing Display
// The bound T: Display is checked at the call site

Subtyping is a relation between types: S is a subtype of T (written S <: T) if any value of type S can be safely used wherever a T is expected. This is not the same as inheritance, though they often coincide in OOP languages.

The correct formal definition is Liskov's Substitution Principle (LSP, 1987): if S <: T, then for every program context C[-] that expects a T, substituting an S must not break the program's observable behaviour. This is stronger than "S has all the methods of T" — it requires those methods to honour the contracts (pre/postconditions) of T's methods.

Structural vs. nominal subtyping: In Java and C#, S <: T only if S explicitly declares implements T or extends T — this is nominal subtyping. In TypeScript and Go, S <: T if S has at least the same fields/methods as T, regardless of declarations — this is structural subtyping (also called "duck typing with types").

Function subtyping: This is where intuition breaks down. When is (A -> B) <: (C -> D)? Answer: when C <: A (input is contravariant) and B <: D (output is covariant). To accept a function where a wider input is expected, the function must handle at least as many inputs. To produce something where a wider output is needed, the output must be a subtype. This leads us to variance.

Record/object subtyping: A record with more fields is a subtype of one with fewer fields (width subtyping). {x: Int, y: Int} is a subtype of {x: Int} because it can be used anywhere an {x: Int} is needed. This is why TypeScript allows passing {name: string, age: number} where {name: string} is expected.

Common pitfall — LSP violations: Java arrays are covariant (String[] <: Object[]), but this breaks LSP. If you put a Dog into an Animal[] that is actually a Cat[], you get an ArrayStoreException at runtime. A properly designed type system (like Scala's or Rust's) prevents this at compile time via correct variance annotations.

// TypeScript: structural subtyping
type Animal = { name: string };
type Dog    = { name: string; breed: string };

// Dog <: Animal (Dog has all fields of Animal, plus more)
function greet(a: Animal): string {
  return "Hello, " + a.name;
}

const d: Dog = { name: "Rex", breed: "Labrador" };
console.log(greet(d)); // OK — Dog is structurally a subtype of Animal

// Function subtyping: (Animal -> void) <: (Dog -> void)
// because Dog <: Animal (contravariant in input)
type DogHandler   = (d: Dog) => void;
type AnimalHandler = (a: Animal) => void;

const handleAnimal: AnimalHandler = (a) => console.log(a.name);
// Safe: handleAnimal can handle Dogs (contravariance)
const h: DogHandler = handleAnimal; // TypeScript allows this

Variance describes how subtyping relationships between type arguments relate to subtyping relationships between generic types. If Dog <: Animal, what is the relationship between List<Dog> and List<Animal>?

There are three possibilities:

• Covariant: List<Dog> <: List<Animal>. The subtyping goes in the same direction as the type argument. Read-only containers are safely covariant: if you can only read from a List<Dog>, you can safely treat it as a List<Animal>.
• Contravariant: List<Animal> <: List<Dog>. The subtyping goes in the opposite direction. Write-only containers are safely contravariant: a function that can consume any Animal can certainly consume a Dog.
• Invariant: neither is a subtype of the other. Mutable containers must be invariant: if List<Dog> <: List<Animal>, you could insert a Cat into what is actually a List<Dog>, corrupting it.

The rule of thumb: type parameters in output position (return types, readable fields) should be covariant; type parameters in input position (function arguments, writable fields) should be contravariant; type parameters in both positions (mutable containers) must be invariant.

In Scala: you declare variance explicitly. class Producer[+A] is covariant (only produces A), class Consumer[-A] is contravariant (only consumes A). The compiler checks that you use A only in the declared positions.

In Java: generics are invariant by default, but you can use wildcards: List<? extends Animal> is a covariant read-only view; List<? super Dog> is a contravariant write-only view. This is the "PECS" rule (Producer Extends, Consumer Super).

In Rust: variance is inferred automatically from how the type parameter is used. Vec<T> is covariant in T because you can only read values out (not write arbitrary values back through a shared reference).

In Haskell: the Functor typeclass requires fmap :: (a -> b) -> f a -> f b, which means f is covariant in its argument. Contravariant (for (b -> a) -> f a -> f b) and Profunctor (covariant in one arg, contravariant in another) formalize this.

Variance is one of the most practically important type-theory concepts — it explains a whole class of surprising type errors and is the key to understanding generics in any language.

-- Scala: explicit variance annotations
class Producer[+A](val value: A)   -- covariant: only produces A
class Consumer[-A] {               -- contravariant: only consumes A
  def consume(a: A): Unit = println(a)
}
class Container[A](var value: A)   -- invariant: both reads and writes

-- Subtyping consequences:
-- Producer[Dog] <: Producer[Animal]  (covariant, same direction)
-- Consumer[Animal] <: Consumer[Dog]  (contravariant, flipped)
-- Container[Dog] is NOT related to Container[Animal]

-- Java wildcards (PECS):
-- void readAll(List<? extends Animal> list) { ... }  // covariant
-- void addDog(List<? super Dog> list) { list.add(new Dog()); } // contravariant

Ad-hoc polymorphism (also called overloading) allows the same function name to have different implementations depending on the type it is called with. show 42 and show True both call show, but with completely different implementations. This is distinct from parametric polymorphism, where the same code runs for all types.

Typeclasses (Haskell) are the principled, type-safe way to achieve ad-hoc polymorphism. A typeclass is a contract — a set of function signatures that a type must implement. An instance is the evidence that a particular type satisfies that contract.

class Eq a where
  (==) :: a -> a -> Bool

instance Eq Int where
  x == y = ... -- primitive comparison

instance Eq a => Eq [a] where
  []     == []     = True
  (x:xs) == (y:ys) = x == y && xs == ys
  _      == _      = False

The instance Eq a => Eq [a] says: "if you can compare elements of type a, I can compare lists of a". This is instance resolution — the compiler automatically constructs the right implementation from the available instances.

Superclasses: Ord requires Eq as a superclass — you cannot order things you cannot compare. This creates a typeclass hierarchy.

Rust traits are essentially typeclasses. impl Display for MyType { ... } is an instance declaration. Rust's orphan rules prevent you from implementing a foreign trait for a foreign type, avoiding ambiguity.

Theoretical foundation: typeclasses are dictionary-passing under the hood. Eq a => becomes an extra function argument — a dictionary — containing the implementations of == for type a. The compiler inserts these dictionary arguments automatically. This is why typeclasses compose so cleanly.

Typeclass laws: good typeclasses come with laws that instances must satisfy. Eq must be an equivalence relation (reflexive, symmetric, transitive). Functor must satisfy fmap id = id and fmap (f . g) = fmap f . fmap g. These laws enable equational reasoning about programs.

-- Haskell: defining and using a typeclass
class Container f where
  empty  :: f a
  insert :: a -> f a -> f a
  toList :: f a -> [a]

data Stack a = Stack [a]

instance Container Stack where
  empty            = Stack []
  insert x (Stack xs) = Stack (x:xs)
  toList (Stack xs)   = xs

-- Generic function works for ANY Container
fillWith :: Container f => [a] -> f a
fillWith = foldr insert empty

-- The compiler picks the right 'insert'/'empty' at each call site
example :: Stack Int
example = fillWith [1,2,3]  -- Stack [3,2,1]

In a simply-typed language, types and values live in separate universes — types classify values, but values cannot appear in types. Dependent types break this wall: types can depend on values. This lets you express invariants that ordinary type systems cannot capture.

The canonical example is Vec n a — a vector of exactly n elements of type a. The type carries the length as a value. The type of append :: Vec m a -> Vec n a -> Vec (m+n) a tells you the exact length of the result. A bounds-checked get :: Vec n a -> Fin n -> a uses Fin n (a type with exactly n values: 0, 1, ..., n-1) to make out-of-bounds access unrepresentable.

Dependent products (Σ-types): (x : A, B x) — a pair where the type of the second component depends on the value of the first. Example: (n : Nat, Vec n Int) — a vector together with its length. The type guarantees they are consistent.

Dependent functions (Π-types): (x : A) -> B x — a function whose return type depends on the argument value. Example: replicate :: (n : Nat) -> a -> Vec n a — given n, produces a vector of exactly that length.

Total functions: in a dependently-typed language like Agda or Idris, all functions must be total (defined on all inputs and provably terminating). This is necessary for consistency — a non-terminating function could "prove" False.

Practical dependent types: Full dependent types (Agda, Coq, Lean, Idris) are used for formal verification of software and mathematics. Lighter forms appear in TypeScript (literal types, template literal types), Rust (const generics: [T; N]), and Liquid Haskell (refinement types). These give you much of the safety benefit without the full complexity of dependent type theory.

The cost: dependent types make type checking undecidable in general (since it requires checking program equivalence). Agda and Coq restrict the language (no general recursion) to regain decidability.

-- Agda-style pseudocode (illustrative)
data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Vec (A : Set) : Nat -> Set where
  []  : Vec A zero
  _::_ : A -> Vec A n -> Vec A (suc n)

-- Type of 'head' guarantees non-empty input
head : Vec A (suc n) -> A
head (x :: _) = x
-- The case '[]' is IMPOSSIBLE to write -- the type forbids it!

-- append: type tracks exact lengths
append : Vec A m -> Vec A n -> Vec A (m + n)
append []       ys = ys
append (x :: xs) ys = x :: append xs ys

-- Rust const generics (a practical approximation):
fn zip<T, U, const N: usize>(a: [T; N], b: [U; N]) -> [(T, U); N] {
    // N is a VALUE in the TYPE -- this is limited dependent typing!
    std::array::from_fn(|i| (a[i].clone(), b[i].clone()))
}

The Curry-Howard correspondence (also called the Curry-Howard isomorphism, or the propositions-as-types principle) is one of the deepest ideas in computer science: types correspond to logical propositions, and programs correspond to proofs.

The correspondence is not a metaphor — it is a precise, formal bijection:

Concrete example: The proposition "if P and Q, then P" has the proof λ(p,q). p. As a type, (P, Q) -> P. As a program, fst :: (a, b) -> a. The same object is simultaneously a tautology, a type signature, and a function.

The proof of a function: when you write fmap :: (a -> b) -> Maybe a -> Maybe b and implement it correctly, you have proved the logical statement: "for all propositions a and b, if a implies b, then (Maybe a implies Maybe b)" — i.e., Maybe is a covariant functor.

Proof assistants: Coq, Lean, Agda, and Isabelle are programming languages where programs are proofs. The Four Colour Theorem was formally verified in Coq. The CompCert C compiler is proved correct in Coq — its assembly output is proved equivalent to the C source.

The gotcha — consistency: the correspondence only works if the type system is consistent as a logic — i.e., there is no proof of Void. This requires the language to be total (no infinite loops). Haskell's undefined :: a is a value of every type, making Haskell's logic inconsistent (but still useful for programming). Agda enforces totality.

Curry-Howard is the philosophical foundation explaining why type-driven development — writing the type first and letting the type guide the implementation — actually works. The type is the theorem; the implementation is the proof.

-- Haskell: propositions as types, proofs as programs

-- Tautology: P -> Q -> P  ("if P and Q, then P")
const_proof :: p -> q -> p
const_proof x _ = x
-- This IS the proof of the tautology, not just a program that "encodes" it.

-- Conjunction elimination: (P, Q) -> P
and_elim_left :: (p, q) -> p
and_elim_left (x, _) = x

-- Modus ponens: (P -> Q, P) -> Q
modus_ponens :: (p -> q, p) -> q
modus_ponens (f, x) = f x

-- Disjunction introduction: P -> Either P Q
or_intro_left :: p -> Either p q
or_intro_left = Left

-- Ex falso quodlibet: Void -> a  (false implies anything)
ex_falso :: Void -> a
ex_falso v = absurd v   -- absurd :: Void -> a  (no cases to match!)

-- Note: in Agda/Lean/Coq these proofs are checked for TOTALITY,
-- making the logic consistent. In Haskell, 'undefined' breaks consistency.