The Calculus of Constructions (CoC) is one of the most common typed lambda calculi, forming the theoretical foundation for dependently typed programming languages like Coq. In this post, we'll implement a type checker for CoC in 200 lines of Python, breaking down the key components and explaining how they work. This is mostly a code-golf exercise, so the implementation is not super robust but it is fun that we can even implement this in Python.
Some background, the CoC was developed by Thierry Coquand in 1985, and is a higher-order typed lambda calculus that combines two key ideas:
Let's break down our implementation into its core components. We have the term representation, in which we approximate algebraic data types using Python classes. A key implementation detail is that we use Higher-Order Abstract Syntax (HOAS) - a technique that encodes object-language binders using metalanguage functions. This allows us to avoid the complexity of handling capture-avoiding substitution and variable renaming that would be needed with traditional named variables or de Bruijn indices.
Before diving into the implementation, let's understand De Bruijn indices, which we use for variable lookup. In De Bruijn notation, variables are represented by numbers that indicate how many binders you need to go up to find the variable's binding site. For example: