Type Theory

/taɪp ˈθɪə.ri/ · Noun · Development · Origin: 1902

Definitions

  1. A formal system in which every expression has a type that constrains how it can be used. Modern type theory (Martin-Löf, HoTT) serves as both a foundation of mathematics and the basis for advanced type systems in languages like Haskell, Rust, and Idris.

    In plain English: A branch of math that classifies values into types. It's why your compiler can catch bugs before you run your code — types are guardrails for correctness.

    Example: "In dependent type theory you can encode the proof that your sort function actually sorts — the types won't let you ship a wrong implementation."

Related Terms