Untyped programs are often prone to errors, runtime exceptions, and can make debugging much harder. That’s why many production languages implement a static typechecker — an extra module, which is aimed to increase programs safety and make development simpler.
Type checking or type inference? What is Type theory and Type judgements? Is my language weakly or strongly typed? And how am I actually going to implement a typechecker?
There are so many questions when it comes to implementing this module. If you’ve been asking those questions in implementing your programming language, or just want to understand how typeckechers work under the hood, on a hands-on practical implementation, this course is for you.
Often related books on Type theory and type judgements go to theoretical aspects viewing types as mathematical sets, not explaining how actually to build a practical typechecker. I believe we should be able to build and understand a typechecker for a full programming language, end-to-end, in 2-4 hours — with a content going straight to the point, showed in live coding sessions as pair-programming and described in a comprehensible way.
In the Building a Typechecker from scratch class we focus specifically on a static typechecker, and build a similar to TypeScript, Java, etc. We slightly touch Type theory and already since the first lecture go into the practical implementation.
Implementing a typechecker would also increase your engineering level, as it touches several aspects of data structures and algorithms.
You can watch preview lectures, and also enroll to the full course, covering implementation of a static typechecker from scratch, in animated and live-annotated format. See details below what is in the course.
An optional prerequisite for this class is the Building an Interpreter from scratch (aka Essentials of Interpretation) course, where we build an AST-interpreter for a full programming language. Unless you already have understanding of how programming languages work at this level, i.e. what
eval, a closure, a scope chain, environments, and other constructs are — it is recommended to take the interpreters class as a prerequisite.
Watch the introduction video for the details.
Who this class is for?
This class is for any curious engineer, who would like to gain skills of building complex systems (and building a typechecker for a programming language is an advanced engineering task!), and obtain a transferable knowledge for building such systems.
If you are interested specifically in compilers, PL and Type theory, and want to build a typechecker module for your programming language, this class is also for you.
What is used for implementation?
Note: we want our students to actually follow, understand and implement every detail of the Typechecker themselves, instead of just copy-pasting from final solution. Even though the full source code for the typechecker is presented in the video lectures, the code repository for the project contains
/* Implement here */ assignments, which students have to solve.
What’s specific in this class?
The main features of these lectures are:
- Concise and straight to the point. Each lecture is self-sufficient, concise, and describes information directly related to the topic, not distracting on unrelated materials or talks.
- Animated presentation combined with live-editing notes. This makes understanding of the topics easier, and shows how the object structures are connected. Static slides simply don’t work for a complex content.
- Live coding session end-to-end with assignments. The full source code, starting from scratch, and up to the very end is presented in the video lectures
What is in the course?
The course is divided into four parts, in total of 20 lectures, and many sub-topics in each lecture. Below is the table of contents and curriculum.
Part 1: Type theory and Basic types
In this part we start talking about Type theory, type checking and type inference, and also build the foundation of our typecker. We establish the basic types, implement variables, talk about Typing Environment, and build a parser.
- Lecture 1: Introduction to Type theory and checking
- Introduction to Type theory
- Parsing pipeline
- Abstract Syntax Tree (AST)
- Static vs. Dynamic type checker
- Strong vs. Weak typing
- Sound vs. Unsound type system
- Type safety and Memory safety
- Type judgements
- Type Environment, Г
- Type checking vs. Type inference
- Hindley-Milner (HM) | Type constraints
- Eva programming language
- Union types
- Generic types
- Implementation of Number type
- Lecture 2: Typing Numbers and Strings. Testing
- Type class
- Number type
- String type
- Tests structure
- Test utils
- Lecture 3: Math binary operations | String concat
- Math operations
- Binary operations
- Operand types
- String concatenation
- Supported operations
- Lecture 4: Variables and Typing Environment, Г
- Variable declaration
- Variable access
- Type Environment, Г
- Identifier resolution
- Scope chain
- Type annotations
- Lecture 5: Blocks and Local scope
- Blocks: sequences of expressions
- Local variables
- Scope chains
- Identifier resolution
- Variable update
- Lecture 6: Parsing: S-expression to AST
- BNF grammars
- Syntax tool
- Generated parsers
- Global TC
- Lecture 7: Control flow: If and While expressions
- Control flow
- Boolean type
- Comparison operators
- If expressions
- While loops
- Parser regeneration
- Static vs. Runtime semantics
Part 2: Functional programming
In this part we focus on different types of functions — user-defined, built-in functions, inner function and closure, recursive function and anonymous lambda expressions.
- Lecture 8: User-defined functions | Local environments
- Function declaration
- User-defined functions
- Parameter types
- Return type
- Function scope
- Lecture 9: Function calls | Built-in functions
- Call expression
- Arguments check
- Native functions
- Lecture 10: Closures | Recursive calls
- Inner functions
- Closure calls
- Recursive functions
- Lecture 11: Lambda functions and IILE | Syntactic sugar
- Lambda functions
- Anonymous function expressions
- IILE calls
- Syntactic sugar
Part 3: Type declarations and Classes
In this part we implement constructs aimed to define new types. Topics of type alises and OOP classes are considered.
- Lecture 12: Declaring new types | Type aliases
- Type declarations
- Alias type
- Alias chains
- Lecture 13: OOP | Classes
- Class declaration
- Classes as Types
- Classes as Environments
- Lecture 14: OOP | Instances
- Class instances
- New operator
- Property access
- Lecture 15: Super calls | Inheritance
- Child classes
- Super calls
- Class inheritance
Part 4: Generic programming
In this part we continue with type declarations, and talk about Union types, and also implement generic functions.
- Lecture 16: Union type
- Type variants
- Operations intersection
- Generic code
- Lecture 17: Union | Type narrowing
- Union type
- Type narrowing
- Any type
- Lecture 18: Generics | Function declarations
- Type parameters
- Template functions
- Declaration time vs. Call time checks
- Environment capturing
- Lecture 19: Generics | Function calls
- Type bindings
- Template functions
- Actual functions
- Lecture 20: Final executable
- Typecheck CLI
- Checking expressions
- Checking files
- Next steps
I hope you’ll enjoy the class and will be glad to discuss any questions and suggestion in comments.