Inside 245-5D

Existential Pontification and Generalized Abstract Digressions


An Eq instance for non de Bruijn terms

tl;dr A non-nameless term equipped with a map specifying a de Bruijn numbering can support an efficient equality without needing a helper function. More abstractly, quotients are not just for proofs: they can help efficiency of programs too. The cut. You're writing a small compiler, which defines expressions as follows: type Var = Int data […]

  • January 30, 2015

A Year of Notebooking (Part 1)

Over the year, I’ve accumulated three notebooks worth of miscellaneous notes and musings. Since these notebooks are falling apart, I’ve decided to transfer their contents here. Warning: they might be slightly incoherent! This is the first of three notebooks. I recommend skimming the section headers and seeing if any of them pop out. Tony Hoare: […]

  • June 20, 2011

Measurement, quantification and reduction

Today we continue the theme, “What can Philosophy of Science say for Software Engineering,” by looking at some topics taken from the Philosophy of Physical Sciences. Measurement and quantification Quantification is an activity that is embedded in modern society. We live by numbers, whether they are temperature readings, velocity, points of IQ, college rankings, safety […]

  • June 8, 2011

Greetings from Switzerland

“Roughing it,” so to speak. With no reservations and no place to go, the hope was to crash somewhere in the Jungfrau region above the “fogline” but these plans were thwarted by my discovery that Wengen had no hostels. Ah well. Still pretty. Of which I do not have a photo, one of the astonishing […]

  • December 29, 2010

To the right! Autocompletable names

In my younger days, the stylistic convention of MM/DD/YYYY confused me; why on earth would people opt for such an illogical system that placed months, days and years in non-hierarchical order? Surely something on order of YYYY-MM-DD would make far more sense: this format is sortable and, all-in-all, quite logical. Eventually, though, I grudgingly accepted […]

  • January 25, 2010