ezyang’s blog

the arc of software bends towards understanding

Computer Science

A short note about functional linear maps

Some notes collected from a close read of Conal Elliot's Compiling to Categories and The Simple Essence of Automatic Differentiation. A colleague of mine was trying to define a "tree structure" of tensors, with the hope of thereby generalizing the concept to also work with tensors that have "ragged dimensions." Let's take a look: Suppose […]

  • May 15, 2019

Tomatoes are a subtype of vegetables

Subtyping is one of those concepts that seems to makes sense when you first learn it (“Sure, convertibles are a subtype of vehicles, because all convertibles are vehicles but not all vehicles are convertibles”) but can quickly become confusing when function types are thrown into the mix. For example, if a is a subtype of […]

  • November 14, 2014

Calculating Shanten in Mahjong

Move aside, poker! While the probabilities of various poker hands are well understood and tabulated, the Chinese game of chance Mahjong [1] enjoys a far more intricate structure of expected values and probabilities. [2] This is largely due in part to the much larger variety of tiles available (136 tiles, as opposed to the standard […]

  • April 1, 2014

HotOS “Unconference” report:
Verifying Systems

Ariel Rabkin has some code he'd like to verify, and at this year’s HotOS he appealed to participants of one “unconference” (informal breakout sessions to discuss various topics) to help him figure out what was really going on as far as formal verification went. He had three questions: "What can we verify? What is impossible […]

  • May 14, 2013

NLP: the missing framework

So you want to make a web app. In today’s world, there is a panoply of software to assist you: you can use an all-in-one framework, or you can grab libraries to deal with the common needs of templating, database access, interactivity, etc. These libraries unify common functionality and take care of edge-cases you might […]

  • January 2, 2013

Functional Encryption

Joe Zimmerman recently shared with me a cool new way of thinking about various encryption schemes called functional encryption. It’s expounded upon in more depth in a very accessible recent paper by Dan Boneh et al.. I’ve reproduced the first paragraph of the abstract below: We initiate the formal study of functional encryption by giving […]

  • November 25, 2012

Extremist Programming

Functions are awesome. What if we made a PL that only had functions? Objects are awesome. What if we made a PL where everything was an object? Lazy evaluation is awesome. What if we made a PL where every data type was lazy? Extremist programming (no relation to extreme programming) is the act of taking […]

  • November 20, 2012

ACM XRDS: Jeff Dean profile

I was wandering through the Gates building when the latest issue of the ACM XRDS, a student written magazine, caught my eye. “Oh, didn’t I write an article for this issue?” Yes, I had! The online version is here, though I hear it’s behind a paywall, so I’ve copypasted a draft version of the article […]

  • October 22, 2012

Visualizing satisfiability, validity & entailment

So you’re half bored to death working on your propositional logic problem set (after all, you know what AND and OR are, being a computer scientist), and suddenly the problem set gives you a real stinker of a question: Is it true that Γ ⊢ A implies that Γ ⊢ ¬A is false? and you […]

  • October 15, 2012

GET /browser.exe

Jon Howell dreams of a new Internet. In this new Internet, cross-browser compatibility checking is a distant memory and new features can be unilaterally be added to browsers without having to convince the world to upgrade first. The idea which makes this Internet possible is so crazy, it just might work. What if a web […]

  • October 12, 2012