featured

Implementing Type Systems as Macros

14 Aug 2023
featured
computer-science, programming-languages, type-checking

There’s a neat paper Type Systems as Macros by Chang, Knauth, and Greenman [1] that describes how to implement a typed language using an untyped host language and macro expansion. The paper is neat, but I found the code hard to follow—the paper uses a compact notation that’s convenient for print, but not so much for reproducing on one’s own. This post is my attempt to implement and explain in more accessible terms what’s presented in the paper. ...

What is a type system, really?

23 Jan 2023
featured
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. ...

Continuations—what are they?

17 Nov 2022
tutorials, featured
programming, programming-languages

I had a friend ask me what continuations are, and why they're useful. There's a ton of literature about continuations; this is just a simple example meant to showcase something small and hopefully grokkable. You will need to understand a little bit of Racket, but if you know any Scheme, that should be good enough. If you just want a quick primer, check out Learn X in Y minutes for Racket. ...

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

27 Jul 2022
featured, tutorials
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. ...

microKanren Reading

4 Jul 2022
tutorials, featured
programming-languages, racket

μKanren (“micro-Kanren”) is a tiny, embeddable logic programming language. It’s easy to understand and implement in almost any language. It’s a great case study of an embedded language: unlike other common “embedded” languages like SQL or regex, which normally are represented as just plain-old strings, μKanren takes more advantage of the host language’s features. I recommend reading the original paper: it’s short, well-written, and easy to understand. I did a write-up which you can read on Sourcehut. ...

Foundations of High-Modernist Ideology in Metropolis

7 Dec 2021
featured
school, literature, literary-criticism

The following is from a essay from a class on German literature and film. Fritz Lang’s movie Metropolis is primarily about the struggle between the oppressed working class and the ruling elite. What drives this tension, however, is a particular view of technology and technological progress that exacerbates the problems the film focuses on. This mentality is called high modernist ideology by Scott in his book Seeing Like a State: ...

Models of Programming

24 Oct 2021
featured
programming, programming-languages

Last week I was studying outside of a lecture hall where someone was teaching an introductory course on computer programming. There was a lot that I overheard that I disagreed with; this essay is an attempt to help me crystallize what exactly I disagreed with.

...