2.0  Prologue

In declarative languages the type system is not just a bug-finder - it is an expressive tool for encoding domain invariants. Algebraic data types let you define exactly the set of valid values. Type inference removes annotation noise while preserving full static safety. Phantom types and refinement types push correctness guarantees deeper into the type layer.

2.1  Algebraic Data Types

An algebraic data type (ADT) is built from two operations:

• Product types (records, tuples) - a value contains both a field of type A and a field of type B. The set of values is the Cartesian product A × B.
• Sum types (tagged unions, enums) - a value is either a variant of type A or a variant of type B. The set of values is the disjoint union A + B.

-- Haskell: product type (record) data Point = Point { x :: Double, y :: Double } -- Haskell: sum type (tagged union) data Shape = Circle { center :: Point, radius :: Double } | Rect { topLeft :: Point, width :: Double, height :: Double } | Triangle Point Point Point -- F#: discriminated union (same concept) type Shape = | Circle of center: Point * radius: float | Rect of topLeft: Point * width: float * height: float -- Rust: enum (sum type with data per variant) enum Shape { Circle { center: Point, radius: f64 }, Rect { top_left: Point, width: f64, height: f64 }, } ADTs make invalid states unrepresentable. A Shape is always one of the known variants - there is no way to construct a half-initialized shape or one that is simultaneously a circle and a rectangle.

2.2  Type Inference

Hindley-Milner (HM) inference deduces the most general type of every expression from its usage, without requiring annotations. The algorithm is complete: if a type exists, HM finds it. If the expression is ambiguous or ill-typed, it reports an error. -- Haskell: no annotations needed; inferred types shown in comments add x y = x + y -- inferred: Num a => a -> a -> a double = map (*2) -- inferred: Num a => [a] -> [a] first = head -- inferred: [a] -> a -- F#: full HM inference let add x y = x + y // int -> int -> int (defaults to int) let double = List.map ((*) 2) -- Rust: local inference (not full HM; annotations required at fn boundaries) let v: Vec<_> = (0..10).filter(|x| x % 2 == 0).collect(); // ^ element type inferred from context HM inference supports let-polymorphism: a let-bound function is generalized to work at any type that satisfies the constraints found during inference. This is how Haskell achieves full parametric polymorphism without a single type annotation in typical code.

2.3  Phantom Types

A phantom type is a type parameter that appears in a type definition but not in any of its runtime fields. It carries no data; it exists only to let the compiler distinguish values that would otherwise have the same representation. -- Haskell: phantom type for unit safety newtype Quantity unit = Quantity Double type Meters = Quantity "meters" type Seconds = Quantity "seconds" addLengths :: Quantity u -> Quantity u -> Quantity u addLengths (Quantity a) (Quantity b) = Quantity (a + b) -- These compile: addLengths (Quantity 3.0 :: Meters) (Quantity 4.0 :: Meters) -- This does NOT compile (unit mismatch caught at compile time): -- addLengths (Quantity 3.0 :: Meters) (Quantity 2.0 :: Seconds) -- Rust: zero-cost phantom type via PhantomData use std::marker::PhantomData; struct Quantity<Unit> { value: f64, _unit: PhantomData<Unit> } struct Meters; struct Seconds; Phantom types are zero-cost: the compiler erases the phantom parameter entirely at runtime. The safety guarantee is purely compile-time.

2.4  Dependent and Refinement Types

Dependent types are types parameterized by values, not just other types. They allow the type of a function’s output to depend on the value of its input - for example, a vector whose type records its length. -- Idris (dependently typed language): length-indexed vector data Vect : Nat -> Type -> Type where Nil : Vect 0 a (::) : a -> Vect n a -> Vect (n+1) a -- zip can only be called on vectors of equal length (enforced by type) zip : Vect n a -> Vect n b -> Vect n (a, b) Refinement types attach a predicate to an existing type. A value of type { x : Int | x > 0 } is an integer known at compile time to be positive. Tools like Liquid Haskell, F*^*, and Dafny check these predicates statically using SMT solvers, eliminating entire classes of runtime invariant violations. -- Liquid Haskell: refinement type annotation {-@ head :: {v:[a] | len v > 0} -> a @-} head (x:_) = x -- Liquid Haskell proves statically that head is never called on an empty list Dependent and refinement types represent the frontier of type-driven development. They are not yet mainstream but are increasingly influential in security-critical and formally verified software.

2.5  Epilogue

Algebraic data types, inference, phantom types, and refinement types push correctness from runtime checks into compile-time proofs. The richer the type language, the more the compiler can verify on your behalf. The next chapter shows how pattern matching unlocks the full power of ADTs at the use site.

2.6  References

Algebraic Data Types - Wikipedia
Hindley-Milner Type System - Wikipedia
Liquid Haskell
Idris - Dependently Typed Language