Some fun reads about typed languages, functional programming, software and language design, and just general culture stuff. Happy October!
Why Is Everything Sold Out Right Now? A lot has been written on how the woeful American response to the COVID-19 pandemic, but one of the areas that almost consumers can relate to is that it seems as though we have a shortage of everything when it comes to shopping online. If you, like me, are curious as how how these shortages came to be, you’ll find this piece interesting.
The Conflict is the Point. This piece is an excellent summary of the relationship between virality and “earned audience” that comes with creating conflict online. My favorite quote: “Whether you’re an individual writer looking to boost your profile or a private-equity fueled global fast food conglomerate, everyone is being trained in the easiest of hacks. Stoke conflict. Be kind of a dick. Go at someone. If there’s no one to go at, build a strawman. Or just subtweet no one. Whatever you do, structure your communication in a conflict or the feeds won’t listen.”
Jenna Wortham. I’m really digging Om Malik’s writings lately; last week I posted a piece on Brunello Cucinelli, and this week I went into the archives for a great read on Jenna Wortham, who’s NYT podcast (Still Processing) I’ve been loving during the pandemic. Non-technically, totally fun read.
The Dark Secrets of Fast Compilation for Kotlin. Kotlin is a interesting language for a lot of reasons, but one of my favorite attributes about the language is that it was designed for industrial programming – meaning it’s optimized for large codebases with many users that grow over time. As a result, one of the things that it needed was an optimizing compiler so that compilation time didn’t become untenable as the codebase grew. This blog post from Jetbrains outlines many of the tradeoffs that they considered when designing Kotlin’s optimizing compiler, and is a good read for not only compiler nerds, but any engineer who has to think hard about tradeoffs.
My Least Favorite Rust Type. A fun counterpoint to my post last week on “My Favorite Rust function”, this piece explains why Rust’s std::ops::Range type is full of confusing features. As a language designer, it’s fascinating to think about how users will interact with programming languages and posts like this are a good reminder on the things that improve language ergonomics.
Void Is a Smell. This is a Haskell post, but the idea that functions that return nothing (i.e. perform side-effects) are a code smell is an important idea that I think is worth considering in any language.
Lambda Pi. This is a really nice (haskell) tutorial by Andres Loh, Conor McBride, and Wouter Swierstra that is demonstrates minimal implementation of Lambda PI (STLC + dependent types). It’s only 30 pages but really clean and easy to read. If you like Haskell, or even just formal verification, you’ll have fun with this. The progressions goes as follows;
introduce an implementation of STLC that uses Locally Nameless representation, bidirectional typechecking, and higher order abstract syntax
implement the syntax, evaluator, and type checker.
Describe the minimal edits to make it into Lambda PI
show the changes to the syntax, evaluator, typechecker.
add Nat base type, introducing motives and dependent type elimination
add Vec base type.
further discussions and comparison to Agda, Epigram, Coq, etc
On Browser Tabs. A quick read that talks about the “seeking circuit” that many of us manufacture when we open (and save) a bunch of browser tabs.