Hi! I’m Michael Arntzenius, or “rntz” online. I study programming languages, in theory and practice. My PhD thesis project was Datafun, a functional query language. I currently work at RelationalAI.

You can email me (qnrxunery@tznvy.pbz, encoded rot13) or find me on Twitter as @arntzenius and Mastodon as @rntz@recurse.social. I’m rntz on GitHub, Goodreads, and Keybase. I have a Twitch but never use it.

Simple, generic, type-safe substitution in Agda

How to avoid needing a new case for every typing rule.

Representing binding in Agda using functions as contexts

A simple technique for implementing type-safe substitution.

Could an archaeologist grok an iPhone?
Parsing list comprehensions is hard

... because it's hard to tell patterns & expressions apart.

Why I am not a fan of Cabal or Stack

Their UI sucks, their docs suck, and they can't uninstall.

Against software development

A techno-pessimist “manifesto”, god help me.

Ursula Le Guin is dead

She's survived by many great women writers; here are a few.

Semilattices and their tensor products

On distributed computing, databases and dictionaries.

Aphorisms on programming language design

Every decision that matters is a tradeoff.

Not everything is an expression

Lisp macros add new expression forms. What about patterns?

Option and null in dynamic languages

To use nil well, always distinguish success from failure.

Monoids, scope, and extensibility

Can monoids be a basis for scoped syntactic extensibility?

On dynamic and static types

Type theory is useful even in dynamic languages.

Belief is indexed by proof system

“Belief” in intuitionistic or classical logic need not be exclusive.

Intuitive hygienic macros

Hygiene is lexical scoping for macros; to implement it, I use syntactic closures.

An odd type inference problem

Recursion + polymorphism + type inference = complicated.

Languages as models of computation

... and monads as tool for model-changing.

OO and pattern-matching

Classes are types are predicates are patterns. Dynamic dispatch is pattern-matching, ordered by specificity.