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.


Last modified 14d ago
Copy link