[JC] Efficient Parallel Programming in Poly/ML and Isabelle/ML

Authors: David C.J. Matthews and Makarius Wenzel
URL: http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf
Year: 2010

I had not heard of Poly/ML or Isabelle/ML prior to reading this paper. I tried to do a bit of background research to get an idea for it, but I may have gotten some details wrong. If I made any mistakes below I will be happy to correct them.

The Paper

Poly/ML is a full implementation of Standard ML originally developed by David Matthews. Larry Paulson was an early adopter and implemented the Isabelle theorem prover. Isabelle/ML is the implementation of Isabelle on Poly/ML. Poly/ML was originally implemented with a single threaded run time system (RTS). With the ubiquity of multicore machines the RTS was modified to support threading, the garbage collector was modified and threading APIs were introduced. Finally, the modifications were tested in Isabelle. This paper is relevant to the frequent debates that occur on the Ocaml mailing list. Ocaml currently has no support for parallelism and this deficiency is frequently brought up as a negative.

A little gotcha in overloading comparison methods in Python

Python supports chaining relational operators so you can express 2 < 3 < 4 and get true. It looks like this is implemented as a little compiler trick that actually creates the expression "2 < 3 and 3 < 4". This can be confusing if you try to do something insane like implement Haskell's (>>=) in Python using (>=). Something like:

Just(10) >= (lambda x : Just(x + 1)) >= (lambda x : Just(x / 2))

Will actually become:

Just(10) >= (lambda x : Just(x + 1)) and \
    (lambda x : Just(x + 1)) >= (lambda x : Just(x / 2))

This only seems to only apply to the relational operators, choosing to implement (>>=) with (>>) in Python seems to work fine. Here is a Gist showing the problem from @apgwoz: https://gist.github.com/916132.

Unicorn is Unix, What?

I'm late to this blog post but @apgwoz just sent it to me. I found it pretty silly. Apparently we should like Unicorn because it uses a lot of Unix system calls...

There’s another problem with Unix programming in Ruby that I’ll just touch on briefly: Java people and Windows people. They’re going to tell you that fork(2) is bad because they don’t have it on their platform, or it sucks on their platform, or whatever, but it’s cool, you know, because they have native threads, and threads are like, way better anyways.

Fuck that.

Don’t ever let anyone tell you that fork(2) is bad. Thirty years from now, there will still be a fork(2) and a pipe(2) and a exec(2) and smart people will still be using them to solve hard problems reliably and predictably, just like they were thirty years ago.

False dichotomies are the best form of logic.