ezyang's blog

One of the most mind-bending features of the untyped lambda calculus is the fixed-point combinator, which is a function fix with the property that fix f == f (fix f).

(Last IMAP themed post for a while, I promise!)

I am going to share a dirty little secret with you, a secret that only someone who uses and hacks on OfflineIMAP could reasonably know: OfflineIMAP sucks.

As software engineers, we are trained to be a little distrustful of marketing copy like this: OfflineIMAP is SAFE; it uses an algorithm designed to prevent mail loss at all costs.

After a long delay and a lot of editing, Issue 20 of The Monad Reader is finally out.

On the importance of primary sources.

Robert Harper has (somewhat) recently released a pre-print of a book (PDF) that he has been working on, Practical Foundations for Programming Languages.

Steve Yegge has posted a fun article attempting to apply the liberal and conservative labels to software engineering.

A common simplification when discussing many divide and conquer algorithms is the assumption that the input list has a size which is a power of two.

This document explains how polymorphic variants in Ur/Web work.

The holy grail of web application development is a single language which runs on both the server side and the client side.

Abstract.

Correctness is overrated.

Earlier this year, Woodie Flowers wrote this criticism of MITx: We seem to have decided to offer “courses” rather than participate in the exciting new process of replacing textbooks with more effective training tools.

You can view it here: An Interactive Tutorial of the Sequent Calculus.

It is once again time for Ubuntu upgrades.

“…so that’s what we’re going to build!”

While working on my senior thesis, I had to write a prior work section, which ended up being a minisurvey for the particular subfield my topic was in.

Ur is a programming language, which among other things, has a rather interesting record system.

This is a very quick and easy fix that has made latency on Ubuntu servers I maintain go from three to four seconds to instantaneous.

If you haven’t noticed, these are coming in the order of the visit days.

Note: this is not a discussion of Hilbert’s formalism versus Brouwer’s intuitionism; I’m using formalism and intuition in a more loose sense, where formalism represents symbols and formal systems which we use to rigorously define arguments (though not log…

I’m hoping that this will be the beginning of a series of posts describing all of the visit days/open houses that I attended over the past month.

Suppose that you have k sorted arrays, each of size n.

Range trees are a data structure which lets you efficiently query a set of points and figure out what points are in some bounding box.

The You could have invented… article follows a particular scheme: Introduce an easy to understand problem, Attempt to solve the problem, but get stuck doing it the “obvious” way, Introduce an easy to understand insight, Methodically work out the rest of t…

Here is a full transcript to Github of Bret Victor’s “Inventing on Principle”.

For various reasons (mostly PhD-related) I will be traveling a bit over the next month.

Abstract.

Last night, I returned from my very first POPL, very exhausted, and very satisfied.

The MonadIO problem is, at the surface, a simple one: we would like to take some function signature that contains IO, and replace all instances of IO with some other IO-backed monad m.

Editor’s note.

It can be hard to understand the appeal of spending three days, without sleep, solving what some have called “the hardest recreational puzzles in the world,”; but over this weekend, hundreds of people converged on the MIT campus to do just that, as part of

Have you ever wondered how the codensity transformation, a surprisingly general trick for speeding up the execution of certain types of monads, worked, but never could understand the paper or Edward Kmett’s blog posts on the subject?

There are two primary reasons why the low-level implementations of iteratees, enumerators and enumeratees tend to be hard to understand: purely functional implementation and inversion of control.

Do you remember your first computer program?

An “easy”, two-step process: Apply this patch for i686.

For the final project in our theoretical computer science and philosophy class taught by Scott Aaronson, Karen Sittig and I decided to create an interactive demonstration of zero-knowledge proofs.

Someone recently asked on haskell-beginners how to access an lazy (and potentially infinite) data structure in C.

Things I should be working on: graduate school personal statements.

I upgraded from Ubuntu Natty Narwhal to Oneiric Ocelot (11.10) today.

tl;dr — Save this page for future reference.

In his classic essay Reflections on Trusting Trust, Ken Thompson describes a self-replicating compiler bug which is undetectable by source code inspection.

What do automatic memory management, static types and purity have in common?

Being back in town over MIT’s Infinite Activities Period is making me think about what kind of short lecture I want to try teaching.

The opinions presented in this post are not necessarily mine.

Ever wondered how Haskellers are magically able to figure out the implementation of functions just by looking at their type signature?

In 2007, Eric Kidd wrote a quite popular article named 8 ways to report errors in Haskell.

Consider the following data type in Haskell: data Box a = B a How many computable functions of type Box a -> Box a are there?