Type Theory, A Very Rudimentary Introduction

Type Theory, A Very Rudimentary Introduction#

Twitter Handle LinkedIn Profile GitHub Profile Tag

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. Muñoz[1] gives a gentle survey of this history and of type theory’s applications in computer science.

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 at static-analysis time - and has deep connections to type theory.

In what follows, I will provide a very rudimentary introduction to type theory. The series of posts 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, but the concepts — subtype relationships, type safety, variance — apply across statically checked languages like Java, C#, and TypeScript.

How to read this series#

The canonical reference for Python’s type system today is the maintained typing specification. The foundational PEPs — PEP 483, The Theory of Type Hints and PEP 484, Type Hints by Guido van Rossum and Ivan Levkivskyi — remain worth reading as historical design records, but where they and the specification disagree, the specification wins.

Conventions used throughout the series:

  • Code examples target Python 3.14 and use modern syntax (PEP 695 type parameters, builtin generics, X | Y unions). Legacy forms (TypeVar(...), Generic[T], capitalized typing aliases) appear only in sidebars explicitly labeled as legacy.

  • Every static-analysis claim is verified against pyright and mypy; where the two checkers disagree, both outputs are shown.

  • Runtime-demonstrable behavior runs in executed code cells; checker-rejected code lives in static blocks with the checker’s actual output.

Roadmap#

  1. Subtypes — types as sets of values; nominal versus structural subtyping; where structural subtyping meets the Liskov substitution principle.

  2. Type Safety — safe substitution; why int is promoted to, not a subtype of, float; static, dynamic, and gradual typing.

  3. Subsumption — the formal three-part criterion for subtypehood; reflexivity and transitivity; narrowing values and widening functions.

  4. Generics — motivation for parameterized types; type variables, parameters, and arguments; generic classes, functions, and methods.

  5. PEP 695: The Type Parameter Syntax (upcoming) — declaration sites, scoping rules, the type alias statement, lazy evaluation, and when legacy TypeVar survives.

  6. Bounds and Constraints — restricting type variables by upper bounds and constraint sets (and, soon, defaults per PEP 696).

  7. Invariance, Covariance, Contravariance — variance of type constructors; mutability’s role; contravariance of Callable arguments.

  8. Type Narrowing: TypeIs and TypeGuard (upcoming) — user-defined predicates, and why TypeIs soundness is a subtyping condition.

  9. Function Overloading — @overload variants, runtime behavior, single dispatch, and unsafe overlapping overloads.

  10. TypedDict and ReadOnly (upcoming) — structural typing of dict-shaped data; read-only keys as the payoff of the variance chapter.

  11. Sentinel Values — NotGiven/Missing singletons, why hand-rolled sentinels defeat narrowing, and the modern idioms.

  12. Annotations at Runtime (upcoming) — PEP 649/749 deferred evaluation, annotationlib, and the end of from __future__ import annotations.

Table of Contents#

Further Reading#