A deep dive into parametric polymorphism in Haskell, framed as 'Unconditional Election' in the Five-Point Haskell series. The post explains how the `forall` quantifier in Haskell's type system provides mathematically guaranteed invariants for free — without explicit annotations or runtime checks. Through examples like `forall a. a -> a` (which must be identity), `forall a. [a] -> [a]` (which must commute with map), and higher-kinded data patterns, the author shows how surrendering type information paradoxically gives stronger correctness guarantees. Practical applications include enforcing lexically-scoped resources (similar to the ST monad), preserving struct fields across transformations, and separating policy from mechanism in business logic. The core insight: making functions more polymorphic restricts what they can do, turning type signatures into machine-checked contracts derived from mathematical properties of universal quantification.
