How to write a type checker/type inferrer with good error messages

27 Jul 2022

All the source for this may be found on my SourceHut repository. Synopsis Experimental type checker/inferer for a simple lambda calculus Description This is a type inference system for a little language. (Described below.) It uses a fusion of type inference algorithms from PLAI, ESP, and μKanren. (See Resources) Broadly speaking, our type inference engine works by: generating typing constraints from the program solving those constraints We'll describe each of those in more detail. ...