the arc of software bends towards understanding
From cvs-ghc@haskell.org:
Hi all,
We now plan to do the git switchover this Thursday, 31 March.
Thanks
Ian
There are some things that I will miss from Darcs (darcs send and the cases where “everything is a patch” actually does work well), but all and all I’m quite pleased to see GHC moving to Git.
The release cycle gets longer and longer… probably to the delight of all those downstream, anyway.
HTML Purifier 4.3.0 is a major security release addressing various security vulnerabilities related to user-submitted code and legitimate client-side scripts. It also contains an accumulation of new features and bugfixes over half a year. New configuration options include %CSS.Trusted, %CSS.AllowedFonts and %Cache.SerializerPermissions. There is a backwards-incompatible API change for customized raw definitions, see the customization documentation for details.
HTML Purifier is a standards-compliant HTML filter library written in PHP (gasp!).
Non sequitur. While researching the security vulnerabilities that were fixed in this version of HTML Purifier, a thought occurred to me: how easy is it to do programming with higher-order functions in JavaScript? JavaScript is extremely fluent when it comes to passing functions around (one might say its OOP facilities are simply taking some base structure and placing functions on it), but the lack of a type system means that it might get kind of annoying documenting the fact that some particular function has some weird higher-order type like Direction -> DataflowLattice -> (Block -> Fact -> (DG, Fact)) -> [Block] -> (Fact -> DG, Fact) (simplified real example, I kid you not!). My experience with the matter in Python is that it just takes too long to explain this sort of thing to ones colleagues, and debugging them is a headache (it’s… hard to inspect functions to see what you got) so it’s better to leave it out.
Yesterday I cycled from Cambridge to Ely, and back again. The route is a glorious 38 miles (round trip) of British towns and countryside. The cycling around Cambridge is quite good, because there aren’t very many hills, and in the farmland areas you get to see the tractors rolling by. The longest I’d ever cycled before was the Springwater Corridor in Portland, the segment of which I did was only about 10 miles.
*Non sequitur.* ICFP submission deadline is today! Functional programmers around the world have reported a sharp increase in draft paper sightings.
Ghost in the state machine
A long time ago (circa 2007-2008), I wrote perhaps the single most complicated piece of code in HTML Purifier—one of those real monsters that you don’t think anyone else could ever understand and that you are really grateful you have a comprehensive test suite for. The idea was this: I had a state machine that modified a stream of tokens (since this was a stream of HTML tags and text, the state machine maintained information such as the current nesting stack), and I wanted to allow users to add extra functionality on top of this stream processor (the very first processor inserted paragraph tags when double-newlines were encountered) in a modular way.
The simplest thing I could have done was abstract out the basic state machine, created a separate processor for every transformation I wanted to make, and run them one pass after another. But for whatever reason, this idea never occurred to me, and I didn’t want to take the performance hit of having to iterate over the list of tokens multiple times (premature optimization, much?) Instead, I decided to add hooks for various points in the original state machine, which plugins could hook into to do their own stream transformations.
Even before I had more than one “injector”, as they are called, I had decided that I would have to do something sensible when one injector created a token that another injector could process. Suppose you ran injector A, and then injector B. Any tokens that injector A created would be picked up by injector B, but not vice versa. This seemed to me a completely arbitrary decision: could I make it so that order didn’t matter? The way I implemented this was have the managing state machine figure out what new tokens any given injector had created, and then pass them to all the other injectors (being careful not to pass the token back to the originating injector.) Getting this right was tricky; I originally stored the ranges of “already seen” tokens separately from the token stream itself, but as other injectors made changes it was extremely easy for these ranges to get out of sync, so I ended up storing the information in the token themselves. Another difficulty is preventing A from creating a token which B converts into another token which A converts to B etc; so this skip information would have to be preserved over tokens. (It seems possible that this excluded some possible beneficial interactions between two injectors, but I decided termination was more important.)
Extra features also increased complexity. One particular feature needed the ability to rewind back to an earlier part of the stream and reprocess all of those tokens; since most other injectors wouldn’t be expecting to go back in time, I decided that it would be simplest if other injectors were all suspended if a rewind occurred. I doubt there are any sort of formal semantics for what the system as a whole is supposed to do, but it seems to work in practice. After all, complexity isn’t created in one day: it evolves over time.
There are several endings to this story. One ending was that I was amused and delighted to see that the problem of clients making changes, which then are recursively propagated to other clients, which can make other changes, is a fairly common occurrence in distributed systems. If you compress this into algorithmic form, you get (gasp) research papers like Lerner, Grove and Chamber’s Composing Dataflow Analyses and Transformations, which I discovered when brushing against Hoopl (note: I am not belittling their work: dataflow analysis for programming languages is a lot more complicated than hierarchy analysis for HTML, and they allow for a change made by A to affect a change B makes that can affect A again: they cut the knot by ensuring that their analysis eventually terminates by bounding the information lattice—probably something to talk about in another post).
Another ending is that, fascinatingly enough, this complex system actually was the basis for the first external contribution to HTML Purifier. This contributor had the following to say about the system: “I have to say, I’m impressed with the design I see in HTML Purifier; this has been pretty easy to jump into and understand, once I got pointed to the right spot.” The evolution of systems with complex internal state is, apparently, quite well understood by practicing programmers, and I see experienced developers tackling this subsystem, usually with success. From an experience standpoint, I don’t find this too surprising—years after I originally wrote the code, it doesn’t take me too long to recall what was going on. But I do wonder if this is just the byproduct of many long hacking sessions on systems with lots of state.
The final ending is a what-if, the “What if the older Edward came back and decided to rewrite the system.” It seems strange, but I probably wouldn’t have the patience to do it over again. Or I might have recognized the impending complexity and avoided it. But probably the thing that has driven me the most crazy over the years, and which is a technical problem in its own right, is despite the stream-based representation, everything HTML Purifier processes is loaded up in memory, and we don’t take advantage of streams of token at all. Annoying!
I recently attended a talk which discussed extending proof assistants with diagrammatic reasoning support , helping to break the hegemony of symbolic systems that is predominant in this field. While the work is certainly novel in some respects, I can’t also but help think that we’ve come back full circle to the Ancient Greeks, who were big fans of geometry, and its correspondingly visual form of reasoning. The thought came up again while I was reading a mathematics text and marveling at the multiple methods of presenting a single concept. In this essay, I’d like to look at this return to older, more “intuitive” forms of reasoning: I’ve called it “Hellenistic reasoning” because geometry and the Socratic method nicely sum up visual and interactive reasoning that I’d like to discuss. I argue that this resurgence is a good thing, and that though these forms of reasoning may not be as powerful or general as symbolic reasoning, they will be critical to the application and communication of abstract mathematical results.
Symbolic reasoning involves syntactic manipulation of abstract symbols on a page; as Knuth puts it, it’s the sort of thing we do when we have a symbol that “appears in both the upper and the lower position, and we wish to have it appear in one place rather than two”. It’s a rather unnatural and mechanical mode of reasoning that most people have to be trained to do, but it is certainly one of the most popular and effective modes of reasoning. While I suspect that the deep insights that lead to new mathematical discoveries lie outside this realm, symbolic reasoning derives its power from being a common language which can be used as a communication channel to share these insights. Unlike natural language, it’s compact, precise and easy to write.
While symbols are an imperfect but serviceable basis for communication among the mathematically inclined, they strike fear and terror in the hearts of everyone else. A conference room of mathematicians will sigh in relief when the slide of axioms and equations shows up; a conference room of systems researchers will zone out when the same slide rolls around. Is this a sign to just give up and start using UML? My answer should be obvious: No! The benefits of a precise formalism are too great to give up. (What are those benefits? Unfortunately, that’s out of the scope of this particular essay.) Can we toss out the symbols but not the formalism? Maybe…
First on the list is visual reasoning. If you can find one for your problem, they can be quite elegant. Unfortunately, the key word is if: proofs with visual equivalents are the exception, not the rule. But there are some encouraging theorems and other efforts that can show a class of statements can be “drawn as pictures on paper.” Here are some examples:
We proceed on to interactive reasoning. These are methods that involve dialogues and games: they find their roots in game theory, but have since then popped up in a variety of contexts.
(It is that last sense that makes wonder if interactional reasoning is something that could become very widely used among software engineers: if you want to reason about the correctness of a system as a whole using a game, you still need to prove facts about strategies in general, but in an adversarial context (for example, compiler error) it could be very simple and useful. This is idle speculation: interactive error systems have been built before, e.g. LaTeX, and unfortunately, they’re not very good. One wonders why.)
I could end this essay with an admonition to “draw pictures and describe interactions”, but that would be very silly, since people do that already. What I would like to suggest is that there is rich theory that formalizes these two very informal activities, and this formalism is a good thing, because it makes our tools more precise, and thereby more effective.
Books are expensive, but by the power of higher-education (also expensive, but differently so), vast oceans of books are available to an enterprising compsci. Here’s my reading list for the spring break lending period (many of which were recommended on #haskell:
Wherein I make fun of functional programming advocates.
In this essay, I’d like to discuss the ideologies of “imperative programming” and “functional programming” in terms of the language features they lean on: in particular, the mechanisms by which they allow developers to express themselves in less code. I propose that the set of features that make up imperative programming constitute a dominant programming monoculture that is partially incompatible with functional programming’s favored features, requiring functional programming advocates to do funny things to gain the attention of the programmers.
To first give a flavor of expressiveness, here are some frequently seen language features that increase expressiveness:
A few of those entries might make you laugh, because you might not understand how you could program without them. You may recognize a few that your favorite language supports well, a few that your language supports less well, and a few your language has no support for. The culture around the language will also have its folklore about what kinds of features are acceptable for use and which ones are not (think Pythonic or JavaScript: The Good Parts). The language you choose determines which features you get to know well.
Being expressive has a cost, which most developers figure out with a little experience in the field. There is a sort of natural selection going on here: language features that are well supported by languages, that other programmers know how to use, and that allow the job to get done are favored—in particular the community effect reinforces the winner. As a result, we have developer monoculture that is mostly comfortable with mutation, input/output, indirection, exceptions, polymorphism, etc. But even the bread-and-butter of current programming practice doesn’t come without cost: think about the famed division between “those who get pointers and those who don’t”, or the runtime costs of using exceptions in C++, or the representation complications of polymorphism (e.g. autoboxing in Java and Go’s lack thereof).
When someone does functional programming advocacy, what they’re really doing is asking you to look more closely at some of the other mechanisms we have for increasing expressiveness. You might feel like these are the only voices you hear, because there’s not much point advocating something that everyone uses already. And you might feel like the enthusiasm is unjustified, because the feature seems bizarrely complicated (continuations, anyone?) or you’ve tried using it in your favorite language, and there’s nothing more painful than seeing someone try to do functional programming in Python. Fact of the matter is, it’s not easy to add these extra language features to the existing monoculture. The new features interact in very complex and subtle ways.
This is why a functional programming advocate will often ask you to give up some of your old tools of expression. They will ask you to give up shared-state mutation, because otherwise handling concurrency is really damn hard. They will ask you to give up dynamic typing, because otherwise higher-order functions become much harder to reason about. The rhetoric will edge on the side of “stop doing that!” because it’s the common practice—they don’t actually mean “stop it entirely” but to the poor functional programming advocate it seems like a little bit of hyperbole is necessary to get the point across—and you can do some pretty amazing things with these extra features.
I encourage programmers to learn about as many ways to express themselves as possible, even if their language or workplace won’t necessarily allow them to use the method. The reasons are manifold:
tl;dr Certain programming language features increase developer expressiveness, and the “imperative programming methodology” captures the dominant monoculture containing those language features in wide use. But there are other ways of expressing oneself, and programmers are encouraged to explore these methods even when practical use necessitates them to stop using some of their favorite expressive tools.
The perverse incentive structure of the Internet
Suppose you have a Random Question™ that you would like answered. For example, “Did Sir Francis Galton have any children?” It’s the type of thing you’d type into Google.
Answers.com is not a terribly good source, but it is something to at least see if you can scrounge up some extra information on. So suppose you dig a little deeper and discover that Francis Galton only married once and that this marriage was barren. So unless some historian’s account of Galton suffering from venereal disease (Kevles 12) indicates that he knocked up some ladies in Syria and managed to pop out four offspring, who happened to conveniently be named “Francis, Harriet, Matilda and Mark,” Answers.com is wrong.
Not really surprising. But that’s not what this essay is about.
What this essay is about is what you’re supposed to do when you encounter flagrant and unabashed misinformation on the Internet: that is, someone is wrong on the Internet. There are a few obvious answers:
Disseminating corrective information is really just a glorified term for “arguing”. And everyone knows that arguing on the Internet is perhaps one of the most undignified occupations one can assume. Nevertheless, it is an important mechanism for correcting incorrect information. As Djerassi once said (and I paraphrase), only a masochist would get into an argument with a fundamentalist about evolution, yet we would be much worse off if we had no such masochists willing to engage in this debate. For less contentious issues, the formula of the “dispelling myths” essay is a popular mechanism of presenting interesting, corrective information to a receptive audience.
I think the primary difficulties with this approach can be summed up in three words: cost, effectiveness and reach.
The notion that you might be able to directly fix it seems to be a relatively recent one, come with the advent of wikis and the social web. Perhaps the ability to unrestrictedly edit an incorrect information source is a new, but the ability to go to the source, to write a letter to the editor of a textbook, is one that has been around for a long time. There is something of a glorious tradition here, including things like Knuth’s reward checks that offer fame and minuscule amounts of money for those who find errors. Sure you might need to argue with one person, but that’s all you need, and afterwards, the original infelicity is corrected.
When you go to the source, you partially resolve the reach problem: new readers instantly have access to the corrected text (though this doesn’t do much for existing dead-tree copies). But cost and effectiveness are still present; perhaps even exacerbated. You have to convince a single person that you’re right; if you can’t manage that, you’ll have to fall back to a separate rebuttal. Sometimes content is abandoned, with the original author having no intention of updating it.
Unrestricted edit access has also given rise to edit warring. In this situation, you have to actively defend the modification you have made, and unfortunately, the winner is usually the one who has more time and resources. Edit warring is war by attrition,.
Aside. There are some parallels with the world of open-source software. Fixing it is analogous to submitting a bug report or a patch; the need to convince the maintainers you are right translates into the act of writing a good bug report. If a project is abandoned, you’re out of luck; even if it’s not abandoned, you need to make the maintainer care about your specific problem. To fork is to disseminate corrective information, although there is an element of unrestricted edits mixed in with social coding websites that make it easy to find related copies.
Or you can not bother, and just ignore it. Maybe vent a little about the problem to your friends, who have no particular stake in the matter, file it away in your brain, and let life go on. In fact, this is precisely the disposition I see adopted by most of my colleagues. They don’t write for the public. They are more than happy to share their vast warehouse of knowledge and insights with their friends, with whom the exchange is usually effective and the cost not very high (they prefer informal mediums like face-to-face conversations and instant-messaging).
In fact, I’d hazard that only a fraction of what you might call the literati and experts of the world prolifically utilize this sort of broad-net information dissemination, that sites like Wikipedia, StackOverflow and Quora attempt to exploit. The incentive structure is simply not there! For the academic, communication with the general public is secondary to communication with your peers and your funders. For the entrepreneur, communication with your customers, and not the sort of communication we see here, is what is valued. For the software engineer, communication with upstream is beneficial insofar as it lets you stop maintaining your bug fixes. The mind boggles at how much untapped expertise there is out there (perhaps that’s what sites like Quora are going for.)
It would be folly to try to tell them all to not do that. After all, from their point of view, this is what is the most rational use of their time. We can try to trick individuals into pouring this information out, in the form of social incentives and addictive triggers, but by in large I think these individuals will not bite. They’re too clever for that.
Better hope you catch them in a fit of irrationality.
I was flipping through An Introduction to Non-Classical Logic by Graham Priest and the section on many-valued logics caught my eye. Many-valued logics are logics with more than the usual two truth values true and false. The (strong) Kleene 3-valued logic, sets up the following truth table with 0, 1 and x (which is thought to be some value that is neither true nor false):
NOT
1 0
x x
0 1
AND
1 x 0
1 1 x 0
x x x 0
0 0 0 0
OR
1 x 0
1 1 1 1
x 1 x x
0 1 x 0
IMPLICATION
1 x 0
1 1 x 0
x 1 x x
0 1 1 1
I’ve always thought many-valued logics were a bit of a “hack” to deal with the self-referentiality paradoxes, but in fact, Kleene invented his logic by thinking about what happened with partial functions where applied with values that they were not defined for: a sort of denotation failure. So it’s not surprising that these truth tables correspond to the parallel-or and and operators predicted by denotational semantics.
The reader is invited to consider whether or not one could use this logic for a Curry-Howard style correspondence; in particular, the law of the excluded middle is not valid in K3.
This is a collection of WTFs due to misuse of mutable state.
We’ll start off with some Java. What do you expect this snippet of code to do? :
Sensor Accel = sm.getDefaultSensor(Sensor.TYPE_ACCELEROMETER);
Sensor Orient = sm.getDefaultSensor(Sensor.TYPE_ORIENTATION);
sm.registerListener((SensorEventListener) this, Accel, sm.SENSOR_DELAY_FASTEST);
Ostensibly, it registers the current object to receive just accelerometer updates. But what if I told you getDefaultSensor was implemented like this:
public Sensor getDefaultSensor (int type){
if(sensors == null) {
sensors = new Sensor(mContext, type);
return sensors;
}else if(sensors.checkList(type)){
sensors.addSensor(type);
return sensors;
}else{
sensors.removeSensor(type);
return sensors;
}
}
This code completely fails to manage the expected semantics: there is a single sm wide Sensor object (stored in sensors) that accumulates sensor values as getDefaultSensor is called. So in fact, this will receive events from both the accelerometer and the magnetometer. The only saving grace is that when we register event listeners, we usually do want them to receive all events, so we might not notice if we weren’t looking too closely. This is real code from OpenIntents SensorSimulator.
Lest you think I only make fun of other people’s code, here is a diff from a project of my own:
@@ -197,13 +197,7 @@ def upload_all(tree, ftp, base):
ftp.cwd(base)
for blob in tree.blobs:
- logging.info('Uploading ' + '/'.join((base, blob.name)))
- try:
- ftp.delete(blob.name)
- except ftplib.error_perm:
- pass
- ftp.storbinary('STOR ' + blob.name, blob.data_stream)
- ftp.voidcmd('SITE CHMOD ' + format_mode(blob.mode) + ' ' + blob.name)
+ upload_blob(blob, ftp, base)
@@ -260,11 +254,25 @@ def upload_diff(diff, tree, ftp, base):
node = subtree/components[-1]
assert isinstance(node, Blob)
- logging.info('Uploading ' + full_path)
- ftp.storbinary('STOR ' + file, node.data_stream)
- ftp.voidcmd('SITE CHMOD ' + format_mode(node.mode) + ' ' + file)
- # Don't do anything if there isn't any item; maybe it
- # was deleted.
+ upload_blob(node, ftp, base)
It looks fairly plausible: I’ve factored out some common storebinary logic. Can you tell what the bug is? Here’s a hint.
The problem is that the upload_all changes the current working directory on the FTP connection (mutable state!), while upload_diff does not (working entirely from the base working directory). The upload function assumed upload_all style working directory changes, and so all upload_diff uploads were dumped in the base directory. Mutability hurts modularity! The fix was to get rid of this mutation and manually calculate the full path; this also removed some delicate invariant preservation in the original upload_all implementation.
Paradoxically enough, though Haskell encourages you not to use mutation, when you do use it, Haskell expressive static type system gives you the unusual ability to statically encode complicated invariants about your mutation—invariants that would not have been necessary if you hadn’t used mutation. A small example of this is ST monad, which uses rank-2 types to ensure that references to mutable memory cannot escape runST, the isolated “mutation thread.”
To the limit, you may find yourself knee deep in advanced type system features if you try to statically rule out incorrect usages of a mutable API. I found this out when I worked with abcBridge, and tried very hard to use types to prevent improper use of underlying C library. Here is one relevant code quote:
-- | When you duplicate a network, node indexes may change, so if you
-- would like to use old references, they need to be translated first.
-- You can read this type as @Node n -> NT n2 (Node n2)@ or @Node n ->
-- NQ n2 (Node n2)@, with the condition that the @n2@ index was one
-- generated by 'branch' or 'speculate'.
translate :: (G.NetworkMonad m AIG (Dup n n2)) => Node n -> m AIG (Dup n n2) (Node (Dup n n2))
This truly is some WTF, rank-2-phantom-types code, but it grew out of a very specific bug I stumbled onto and was unconvinced that I’d remember to avoid in the future (can you guess what it was?) A curious reader may ask, why do I need to duplicate networks in the first place? Because some operations that the underlying library provides are destructive, and the only way I can provide the illusion of persistent networks is duplicating before destruction.
In summary:
Avoid it when you can!