Use this tag for questions about type theories, which are formal systems to specify properties of objects.

Type theory is the study of formal systems that classify objects into categories. It was historically introduced in logic, to provide a foundational set theory, and is now widely used in programming language design. Use this tag if your question touches on theoretical aspects of types.

References:
Stanford Encyclopedia of Philosophy
nLab
Wikipedia

For a history on types see Functions and Types in Logic, Language and Computation∗ (pdf)