Type Safety

9 articles

• Type Algebra: Products and Sums3 min read

  Algebraic type theory offers us an elegant correspondence between data structures and elementary arithmetic.

• Algebraic Data Types: Precision and Expressiveness3 min read

  Algebraic data types (ADTs) form the foundation of modeling in typed functional languages, and their influence now extends far beyond.

• Total and Partial Functions: The Type's Promise4 min read

  A total function is one that terminates and produces a valid value for every input in its declared domain.

• Make Illegal States Unrepresentable3 min read

  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...

• Parse, Don't Validate3 min read

  Alexis King's article, published in 2019, crystallized an intuition that many functional programmers carried without necessarily knowing how to articulate it.

• Isomorphisms at Boundaries: Lossless Translation3 min read

  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.

• The Curry-Howard Correspondence: Linking Programs and Proofs4 min read

  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...

• Refinement and Dependent Types: Towards Types That Prove3 min read

  Beyond classical typing, certain systems allow encoding finer properties. The compiler then becomes a proof assistant, enabling enforcement of even more precise business invariants.

• Detect Errors Early: From Lean to Shift Left3 min read

  The fundamental Lean principle that a defect costs exponentially more as it progresses through the value chain applies with particular acuity to software development.