Hi! I'm Michael Arntzenius, “rntz” for short. I study programming languages, in theory and practice. My current project is Datafun, a functional query language.

You can email me, or find me on Twitter as @arntzenius. I'm rntz on GitHub, Pinboard, Keybase, and Freenode.


Simple, generic, type-safe substitution in Agda

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

Representing binding in Agda using contexts as functions

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.

Anarki updated to arc3
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.