What is a type system, really?

23 Jan 2023
computer-science, programming-languages, type-checking

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. ...

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

27 Jul 2022
tutorials, featured
programming-languages, type-checking, computer-science

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. ...

Complete and Liveness, Safe and Sound

2 Mar 2022
programming-languages, computer-science

I have a hard time keeping these terms straight: liveness vs. safety soundness vs. completeness This is intended as a short guide for myself; maybe someone else will find it useful too! Note that this is all to the best of my knowledge and understanding at the present time; if there be faults, they be the faults of myself. I welcome correction and clarification if I am wrong. Liveness vs. Safety # Liveness and safety deal with properties of a system. ...

Control-Flow Analysis

27 Jul 2021
programming, computer-science, research, cfa

Control-Flow Analysis is a popular technique for performing static analysis of many different kinds of programming languages. It’s most often needed in cases where you have some kind of dynamic dispatch: either where you have first-class functions or when you have objects and you call one of their methods.