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.

results matching ""

    No results matching ""