Type Theory


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