Skip to main content

Type Theory

Here is a nice thread on what a type is. Mélitte is nice toy implementation of Martin-Löf Type Theory.

Notes​

  • 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.
  • Types are specifications of behavior.
  • Roughly speaking, a type is a specification of its possible values.
  • Generics should not force you to mention irrelevant information.