Type Theory, A Very Rudimentary Introduction

In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. The lineage of type theory can be traced back to after the development of set theory in the late 19th century where it is born out of the need to avoid the Russell’s paradox.

In the context of computer science and programming, it is known that static program analysis, such as the type checking algorithms in the semantic analysis phase of compilers, can be used to detect type errors in compile time - and has deep connections to type theory.

In what follows, I will provide a very rudimentary introduction to type theory. The series of post serve more as a reflection and learning experience for me than an in-depth guide. We will walk through the basic concepts of type theory and its applications in computer science. Most examples will be in Python. It would be helpful if the readers skim through PEP 483 - The Theory of Type Hints, written by Guido van Rossum and Ivan Levkivskyi, before diving into the series.

Although the reference guide is written by the authors of the python language, the concepts of type theory, including subtype relationships and type safety, are applicable across many programming languages, not just Python. These principles have deep roots in computer science and are essential in understanding static type checking in languages like Java, C#, TypeScript, and many others.

Table of Contents

• Subtypes
• Type Safety
• Subsumption
• Generics and Type Variables
• Bound and Constraint in Generics and Type Variables
• Invariance, Covariance and Contravariance
• Function Overloading
• Sentinel Types

Citations

• [1] Z. Luo, S. Soloviev, and T. Xue, “Coercive subtyping: Theory and implementation”, Information and Computation, vol. 223, pp. 18–42, Feb. 2013. doi:10.1016/j.ic.2012.10.020

• [2] C. Muñoz, “Type Theory and Its Applications to Computer Science”, National Institute of Aerospace, Hampton, VA, Tech. Rep., Apr. 10, 2007.