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 to6. 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.