ezyang's blog

the arc of software bends towards understanding

Posts

A classical logic fairy tale

(Selinger) Here is a fairy tale: The evil king calls the poor shepherd and gives him these orders. “You must bring me the philosophers stone, or you have to find a way to turn the philosopher’s stone to gold. If you don’t, your head will be taken off tomorrow!” What can the poor shepherd do to save his life?

Hat tip to Chris for originally telling me a different variant of this story. Unfortunately, this quote from Lectures on the Curry-Howard Isomorphism was the only reference I could find. What should the shepherd do? Is there something a little odd about this story?

Read more...

Resource limits for Haskell

Last week, I made my very first submission to ICFP! The topic? An old flame of mine: how to bound space usage of Haskell programs.

We describe the first iteration of a resource limits system for Haskell, taking advantage of the key observation that resource limits share semantics and implementation strategy with profiling. We pay special attention to the problem of limiting resident memory usage: we describe a simple implementation technique for carrying out incremental heap censuses and describe a novel information-flow control solution for handling forcible resource reclamation. This system is implemented as a set of patches to GHC.

Read more...

The single export pattern

From the files of the ECMAScript TC39 proceedings

Single export refers to a design pattern where a module identifier is overloaded to also represent a function or type inside the module. As far as I can tell, the term “single export” is not particularly widely used outside the ECMAScript TC39 committee; however, the idea shows up in other contexts, so I’m hoping to popularize this particular name (since names are powerful).

Read more...

The duality of weak maps and private symbols

From the files of the ECMAScript TC39 proceedings

I want to talk about an interesting duality pointed out by Mark Miller between two otherwise different language features: weak maps and private symbols. Modulo implementation differences, they are the same thing!

A weak map is an ordinary associative map, with the twist that if the key for any entry becomes unreachable, then the value becomes unreachable too (though you must remember to ignore references to the key from the value itself!) Weak maps have a variety of use-cases, including memoization, where we’d like to remember results of a computation, but only if it will ever get asked for again! A weak map supports get(key) and set(key, value) operations.

Read more...

What is a membrane?

If you hang out long enough with a certain crowd (in my case, it was the ECMAScript TC39 committee), you will probably hear the term membrane tossed around. And eventually, you will start to wonder, “Well, what is a membrane, anyway?”

As is the case with many clever but simple ideas, membranes were first introduced as a footnote [1] in a PhD thesis. Suppose that you are building distributed system, in which you pass references to objects between two separate nodes. If I want to pass a reference to foo in process A to process B, I can hardly just hand over an address—the memory spaces are not the same! So instead, I need to create a wrapper object wrappedFoo representing foo in B, which knows how to access the original object in A. So far so good.

Read more...

Kindle Paperwhite notes

Along with a Nexus 7, I also acquired a Kindle Paperwhite over winter break. (Wi-Fi only) I have been quite pleased by this purchase, though in an unexpected way: while I have not increased the number of books I read, the Kindle has materially changed how I read articles on the Internet. Not via their web browser, which is essentially unusable except for the simplest tasks, but via tools which take articles on the Internet and convert them into ebook form.

Read more...

The GHC scheduler

I’d like to talk about some nitty-gritty details of GHC’s thread scheduling, discovered over the course of working on stride scheduling for GHC. Most of these choices are merely implementation details and are not part of any specification. While these choices shouldn’t be relied upon, they are worth knowing, since many of these details were accreted over the course of many performance bugs, benchmark tests and other battles. In this post, I’ll attempt to give some historical insight into why many choices were made. These insights should generalize to any system that would like to implement green threads, lightweight threads that use less memory than traditional operating system threads. For space reasons, I’m not going to talk about STM or sparks (though they are also quite interesting).

Read more...

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 otherwise not have the resources to deal with.

But there is one tool which is conspicuously absent: the natural language processing library.

Read more...

Google Nexus 7 setup notes

I acquired a Google Nexus 7 (Wi-Fi only) over winter break. I don’t really like getting new devices: they invariably require a lot of work to setup to my liking. Here are some notes:

  • Jailbreaking the device from Linux is still fiddly. Ultimately, it’s probably easiest to just find a Windows box and use the Nexus Root Toolkit. The tool is somewhat racy; try the detection code again if it fails the first time.
  • Transferring files to/from Linux is a pain in the ass. I have SCP over SSHDroid working; I also tried both DropBear SSH Servers but they did not come with scp binaries and were thus fairly useless for the purpose of file transfer. SSHDroid didn’t work out of the box: I needed to apply comment 14 to make the real scp binaries get picked up in the path. By default, these apps are configured to accept password-authentication (not even keyboard-interactive!) with extremely weak default passwords: make sure you disable that. Still looking for a good rsync implementation. On the USB side, Ubuntu/Gnome/Nautilus natively recognised Nexus in PTP mode but when I tried copying files it hung. MTP is fairly unsupported by Ubuntu 12.10, but go-mtpfs works decently well given a sufficiently modern libmtp. Adam Glasgall has packaged libmtp for Quantal, so go add his PPA, and then follow the installation instructions of go-mtpfs. Update: Transferring files directly to removable media has also worked reasonably well.
  • The tablet really does feel like a phone, courtesy of both being on the Android platform. But no 3G means offline is a lot more important, and the larger screen makes certain types of applications a lot more pleasant to use (Update: I’ve settled on MX Player as my video player of choice, since it supports Advanced SubStation Alpha subtitling and MKV files. Unfortunately, it doesn’t support deep color (e.g. 10-bit).)
  • Micro USB to USB OTG cable is really handy, esp. for hooking up keyboards or external media. I’d dare say, it’s a more essential accessory than a cover. Note that the micro-USB port isn’t able to power USB devices with high power requirements (e.g. spinning platter external disks), so you’ll need a powered USB hub to connect them. (One symptom of this is if you try to mount an under-powered hard drive, the directory listing will persistently come up empty. It may also may make clicking noises: probably not good for the drive.) I use USB-OTG to perform mounting.
  • I tried to get my paper database on Mendeley mirrored onto my tablet, but it’s been pretty tough. I’ve been trying to use Referey, which is a Mendeley-client for Android, but it requires me to somehow propagate my Mendeley SQLite database and all of my PDFs. Dropbox seems like a good match here, except that the official Dropbox client doesn’t support keeping entire folders synced (only favorite files). If you’re like me, and you don’t know exactly what papers you are going to be reading, you have to use something different, e.g. Dropsync. (BTW, if you, like me, have the clever idea of putting the SQLite database with your PDFs, so they all get synced in one folder, don’t ever “Tidy Up”: Mendeley will happily delete your SQLite database as a “foreign object”.) Mendeley and Dropbox seem to interact poorly with each other in various ways (case-sensitivity; also, Mendeley likes to make filenames that are too long, and Dropbox will stupidly and happily accept them).
  • The “open windows” button doesn’t appear to properly respect when an application is closed through its own volition (i.e. through an exit button natively supported by the aplication.) This is a bit annoying.

Oh yeah, and Happy New Year. :)

Read more...