12 articles
← Back to all tagsAlgebraic type theory offers us an elegant correspondence between data structures and elementary arithmetic.
Algebraic data types (ADTs) form the foundation of modeling in typed functional languages, and their influence now extends far beyond.
A total function is one that terminates and produces a valid value for every input in its declared domain.
This phrase, popularized by Yaron Minsky in the context of OCaml, captures the very essence of a defensive approach to modeling: rather than verifying after the fact that a state is valid, we structur...
Alexis King's article, published in 2019, crystallized an intuition that many functional programmers carried without necessarily knowing how to articulate it.
An isomorphism between two types A and B is a pair of functions to : A → B and from : B → A such that from(to(a)) = a and to(from(b)) = b for any value.
Property-based testing (PBT), popularized by QuickCheck in Haskell in the late 1990s, reverses the traditional approach to unit testing.
The scenario is classic: a legacy function f, tangled, difficult to maintain, but whose behavior is correct (or at least accepted as such by system users).
The Curry-Howard correspondence, sometimes called the Curry-Howard isomorphism, establishes a deep equivalence between two apparently distinct domains: formal logic and type theory. The term isomorphi...
Philip Wadler, in his talk and paper "Propositions as Types," offers a historical and philosophical meditation on the Curry-Howard correspondence.
Beyond classical typing, certain systems allow encoding finer properties. The compiler then becomes a proof assistant, enabling enforcement of even more precise business invariants.
The fundamental Lean principle that a defect costs exponentially more as it progresses through the value chain applies with particular acuity to software development.