Type Theory

6 articles

• Type Algebra: Products and Sums3 min read

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

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

• Initial and Final Encodings: Two Embedding Philosophies3 min read

  Embedded domain-specific languages (embedded DSLs) allow building mini-languages within a host language, inheriting its syntax, type system, and tooling.

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

• Propositions as Types: Wadler's Unification3 min read

  Philip Wadler, in his talk and paper "Propositions as Types," offers a historical and philosophical meditation on the Curry-Howard correspondence.

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