Coming back to this after having taken graduate algebra makes me realize: programming type semantics is all magic