Type Theory

Roughly speaking, a type is a specification of its possible values.


  • A value is some concrete thing, and a type is a collection of concrete things (but is itself not a concrete thing. For example any individual integer is a value, but the collection of all integers is a type. Much like elements and sets in set theory.
  • A type is a collection of values which inhabit that type. A type is a value which is a member of the type of types.
  • Type theory goes much much further than just tagging data.
  • The type determines which data structure you use.
  • Dependent types is basically about being able to express arbitrary things in your type system, meaning that you can construct arbitrary proofs. That's how Coq, Agda and Idris work.
  • Types are types and propositions are propositions; types come from programming languages, and propositions from logic, and they seem to have no relation to each other.

results matching ""

    No results matching ""