Typing Rules, Notation and Variables

I’ve changed a few things since I started giving talks again, I’ve got at least one more change on the way, and I figured it was worth talking about them so other people could see why I’ve made them and to comment on the tensions behind the status quo.

First of all, I’m extremely glad I let Conor McBride nudge me towards larger fonts on slides! I’ve found myself in a situation where the original speaking room overflowed and I wound up with people watching from a worrying viewing angle that put them at twice the expected viewing distance. So these days my Beamer slides pretty much default to \Large everywhere and so far it’s doing right by me. I figure I need a really good reason to dip into \large for a slide, let alone \normalsize or smaller.

But there’s a related problem that’s all over mathematical papers - superscripts and subscripts. I don’t think it’s too bad if I ask Pandoc to give me, say, π² or τ^f in the middle of a post rather than some slides, but in most settings the font gets smaller and smaller - 2²²² is actively uncomfortable.

Superscripts also play into another, more controversial issue in our notation. I used τ^f as an example because I often use it for a function’s type. Or at least I did - these days I try to use τf instead to avoid the scaling problem. But nice as that is when we’re doing a bunch of pen and paper work? It’s still a pain to read, especially for anybody who doesn’t manage to guess that not only is τf a function type, but τp is the type of a parameter and τr is a return or result type! The notation might be strictly formal, but the more intuition we can provide the better.

So what I’m trying to do where I can is use names like τfunction or - when I get to name it - Γbody. The names are more informative and the greek letters now have a clear purpose that applied all long.

Surprise! It’s Charles Simonyi’s Hungarian Notation!¹ We use τ and Γ to indicate the syntactic categories - the meta-level types, if you will - that our schematic variables refer to. If I wanted to wind up a certain kind of E.W. Dijkstra fan I might even compare them to BASIC-style sigils.

So what’s stopping me from doing this everywhere? Well, for one: it’s a pain when we’re writing to fit a page limit on paper. Page limits force us to spatially compress what we’re saying. Even if the variable names fit fine in a column, they might mean it takes an extra line or two to write a typing rule down. When we want to publish papers, the paper gets right in our way.

And okay, my handwriting’s both slow and ugly so if I’m calculating by hand… but I’m not a maths lecturer and I don’t often do that for an audience of more than one or two people. If I need to reproduce my working elsewhere, I’ve got time to typeset it and pick better variable names.