23 Jan 2023
Background This is a question I've been wrestling with for a little bit. My first experience with a type system was with Java, and I didn't like it. It just felt like an annoying constraint on the kinds of programs I could write. I was coming from Perl, which sports weak dynamic typing, so Java's rigidity came as a bit of a shock.
After Java I learned some C, which too has types.
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.