Real-world type theory I: untyped normalisation by evaluation for λ-calculus

Normalisation corresponds to a sensible notion of /computation/ in most type systems; most theories with a natural number type, for example, will have terms like 1 + 5, (1 + 1) * (1 + 1 + 1), and so on all reduce to 6. In Abel’s wonderful analogy, normalisation increases /entropy/, understood by analogy to thermodynamic entropy. In physics, entropy is a measure of /disorder/ in a system. A pile of firewood contains a lot of complex organic molecules; lighting it on fire reduces it to much simpler molecules, reducing the total amount of “order” in the system, and converts some of the energy stored in chemical bonds to heat energy in the process. Energy is conserved, but the entropy of the (wood + oxygen + smoke + ashes) system increases in the process. In our PL-theoretic world, too, normalisation collapses — not chemical, but rather syntactic — structure.

Haskell doesn’t have macros

Quasiquotes in GHC optimise a different use-case to macros: they let you deal with /foreign/ languages. Macros let you add slight enhancements to your /existing/ language.

Tales From a Core File - Lessons from the Unix stdio ABI: 40 Years Later

Topology Explains Why Automobile Sunshades Fold Oddly

We use braids and linking number to explain why automobile shades fold into an odd number of loops.

Hacker News discussion of Structure and Interpretation of Classical Mechanics

Good recommendations and references.

The medical test paradox: Can redesigning Bayes rule help? (3Blue1Brown video)

Surprisingly, given all the time I’ve spent on Lesswrong, I hadn’t heard of likelihood ratios / Bayes factors before.

Berkson’s Paradox

Why are handsome men jerks? Why does Hollywood ruin books? Why do restaurants serve good burgers or good fries but not both? Spurious negative correlations everywhere.