Three famous quotes

These three quotes are logically related to each other. Have you figured out their relationship? ;-)

UNIX is simple, it just takes a genius to understand its simplicity. —Dennis Ritchie

This suit of clothes is invisible to those unfit for their positions, stupid, or incompetent. —the emperor’s weavers

If you can’t explain it to a six year old, you don’t understand it yourself. —Albert Einstein

RubySonar: a static analyzer for Ruby

(This is a reposting of a blog post I wrote on Sourcegraph‘s website)

Since the last enhancement to our Python analysis, we have been working on improving the Ruby part of Sourcegraph by building a similar static analysis tool for Ruby. The result is a new open-source project RubySonar. With its help, now we are happy to see significantly improved results of Ruby repos which in general finds over ten times more symbols, provides more examples and more accurate jump-to-definition. It also provides local variable highlighting which was not available in our previous Ruby results. With the improved speed of analysis, we can now process the full Ruby standard library, Ruby on Rails, and Ruby apps such as Homebrew.

RubySonar’s analysis is interprocedural and is sensitive to both data-flow and control-flow, which makes it highly accurate. Although we currently don’t show the types, RubSonar internally uses the same type inference technique of PySonar, and thus can resolve some of the difficult cases that can challenge a good Ruby IDE.

Although Ruby and Python seem to be very similar languages, lots of work has been done to adapt PySonar’s code to Ruby. Still more work has to be done before RubySonar can achieve the same coverage of PySonar2, but so far the Ruby results are a lot more usable. We have been carefully keeping things simple and easy to extend, so we are optimistic about further improvements to the Ruby analysis.

Tests and static analysis

Ever since I made a static analysis tool for Python called PySonar, I have been asked about the question: “What is the difference between testing and static analysis?” When I worked at Coverity, my coworkers told me that they also spent quite some time explaining to people about their difference. My answer to this question evolves as my understanding of this area deepens. Recently I replied to a comment asking a similar question, so I think it’s a good time to write down some systematic answer for this question.

Static analysis is static, tests are dynamic

Static analysis and tests are similar in their purposes. They are both tools for improving code quality. But they are very different in nature: static analysis is static, but tests are dynamic. “Static” basically means “without running the program”.

Static analysis is similar to the compiler’s type checker but usually a lot more powerful. Static analysis finds more than type errors. It can find defects such as resource leaks, array index out of bounds, security risks etc. Advanced static analysis tools may contain some capabilities of an automatic theorem prover. In essence a type checker can be considered a static analysis with a coarse precision.

Static analysis is like predicting the future, but testing is like doing small experiments in real life. Static analysis has the “reasoning power” that tests hasn’t, so static analysis can find problems that tests may never detect. For example, a security static analysis may show you how your website can be hacked after a series of events that you may never thought of.

On the other hand, tests just run the programs with certain inputs. They are fully dynamic, so you can’t test all cases but just some of them. But because tests run dynamically, they may detect bugs that static analysis can’t find. For example, tests may find that your autopilot program produces wrong results at certain altitude and speed. Static analysis tools can’t check this kind of complex dynamic properties because they don’t have access to the actual running situation.

But notice that although tests can tell you that your algorithm is wrong, they can’t tell you that it is correct. To guarantee the correctness of programs is terribly harder than tests or static analysis. You need a mechanical proof of the program’s correctness, which means at the moment that you need a theorem prover (or proof assistant) such as Coq, Isabelle or ACL2, lots of knowledge of math and logic, lots of experience dealing with those tools’ quirks, lots of time, and even with all those you may not be able to prove it, because you program can easily encode something like the Collatz conjecture in it. So the program’s passing the tests doesn’t mean it is correct. It only means that you haven’t done terribly stupid things.

Difference in manual labor

Testing requires lots of manual work. Tests for “silly bugs” (such as null pointer dereference) are very boring and tedious to make. Because of the design flaws of lots of programming languages, those things can happen anywhere in the code, so you need a good coverage in order to prevent them.

You can’t just make sure that every line of the code is covered by the tests, you need good path coverage. But in the worst case, the number of execution paths of the program is exponential to its size, so it is almost impossible to get good path coverage however careful you are.

On the other hand, static analysis is fully automatic. It explores all paths in the program systematically, so you get very high path coverage for free. Because of the exponential algorithm complexity exploring the paths, static analysis tools may use some heuristics to cut down running time, so the coverage may not be 100%, but it’s still enormously higher than any human test writer can get.

Static analysis is symbolic

Even when you get good path coverage in tests, you may still miss lots of bugs. Because you can only pass specific values into the tests, the code can still crash at the values that you haven’t tested. In comparison, static analysis processes the code symbolically. It doesn’t assume specific values for variables. It reasons about all possible values for every variable. This is a bit like computer algebra systems (e.g. Mathematica) although it doesn’t do sophisticated math.

The most powerful static analysis tools can keep track of specific ranges of the numbers that the variables represent, so they may statically detect bugs such as “array index out of bound” etc. Tests may detect those bugs too, but only if you pass them specific values that hits the boundary conditions. Those tests are painful to make, because the indexes may come after a series of arithmetic operations. You will have a hard time finding the cases where the final result can hit the boundary.

Static analysis has false positives

Some static analysis tools may be designed to be conservative. That is, whenever it is unsure, it can assume that the worst things can happen and issue a warning: “You may have a problem here.” Thus in principle it can tell you whenever some code may cause trouble. But a lot of times the bugs may never happen, this is called a false positive. This is like your doctor misdiagnosed you to have some disease which you don’t have. Lots of the work in building static analysis tools is about how to reduce the false positive rate, so that the users don’t lose faith in the diagnosis reports.

Tests don’t have false positives, because when they fail your program will surely fail under those conditions.

The value of static analysis

Although static analysis tools don’t have the power to guarantee the correctness of programs, they are the most powerful bug-finding tools that don’t need lots of manual labor. They can prevent lots of the silly bugs that we spend a lot of time and energy writing tests for. Some of those bugs are stupid but very easy to make. Once they happen they may crash an airplane or launch a missile. So static analysis is a very useful and valuable tool. It takes over the mindless and tedious jobs from human testers so that they can focus on more intellectual and interesting tests.

What makes python static analysis interesting and hard

(The original version of this post appeared in my company’s blog. Here is just a personal copy of it.)

Python is a dynamic language in the authentic sense. It represents the world-view that types don’t really exist in reality, and this is probably right. Type systems are “thinking tools” that only exist in our head. They help us reason about programs, but the world doesn’t really work in their ways. Types help prevent basic programming errors, but if not designed properly, a type system can be a big impedance to the programmer’s productivity. Years of cutting-edge research still haven’t produced a type system that won’t get into the programmers’ way, but you can still write useful program without a static type system. This is why dynamic languages such Python, Ruby and JavaScript are attractive to people, especially those who want to express themselves more directly and don’t like to go out of their way to make type systems happy.

But this directness and ease of use have a cost. Making IDEs and refactoring tools is a hard problem for Python. Type errors are hard to catch. For a simple example, the current state-of-the-art in Python IDEs is like the following.

I loaded this tiny program into the most recent version of JetBrains PyCharm (3.0.2), a Python IDE, and pressed the “show declaration” key on the field accessor foo, and it gave me three irrelevant choices, without including the right one.

Despite this limitation, PyCharm is still a really nice tool. I like PyCharm and use it myself. But this problem of finding the correct declaration of foo is harder than you might have thought. Without knowing what x is, how would you find the declaration of foo? This requires an “interprocedural analysis” where you track all the places where function f can be called. This could be many levels deep into the call chain. And because you can use functions as values, you sometimes don’t even know which function a name represents. You have to keep track of the type information that flows around this intricate data and control flow. Doing interprocedural analysis is hard in general, and it is even harder in a dynamic language with features such as first-class functions.

Finding type errors in Python is also hard. PyCharm would not report any problems for the following piece of code, but when you run it, you get a type error because you are adding the string "hi" and the integer 1. The if statement sets x to different types in different branches (int and str), and this confuses PyCharm’s type checker.

This might not be a big problem for an IDE, but as a semantic code search and browsing engine, we at Sourcegraph must do better, because if we can’t resolve the names, we will not have any usage information about that piece of code. We want to get as much information about code as possible. For this purpose, we use PySonar, a static analysis tool for Python. PySonar can handle the above cases, and a lot more complicated ones.

PySonar is at its core an “abstract interpreter”. It basically works like a Python interpreter, only that it doesn’t really execute the program. It implements almost everything in Python: modules, classes, objects, functions (closures), etc. It transfers “abstract values” (types) instead of actual values. It explores all possible execution paths of the program, and it always terminates. This simple technique works surprisingly well.

Working on PySonar is interesting because you think about the world philosophically with a “multiple worlds” model. If you don’t know the answer to a decisive question in your life, what can you tell about the future no matter what the answer is? The trick is to use as much information you can get, put it into the possible “branches”, and try to deduce conclusions from what you have. This is basically what mathematical proofs are about—I don’t know what the natural number N is, but a natural number can only be 1) zero, 2) M+1 where M is some other natural number. So as long as I know that 1) P holds for zero, and 2) P holds for M+1 whenever M is another natural number, then I know that P holds for all natural numbers.

Similarly in the above example, PySonar knows that if we don’t know what z is, x could be either an integer or a string. A program is safe only if it is safe in all possible worlds, thus PySonar knows that things could go wrong when we try to execute x+1. This kind of reasoning is done pretty easily by building so-called “models”. Models abstractly represent things inside the program’s execution. Old models transform into new models when actions happen in the program, and the “world” of models split at branching statements.

The new PySonar2 is a lot better than its predecessor. Its interprocedural analysis finds more declarations and more precisely. It also generates type information which can be helpful for understanding programs. This type information is already available on Sourcegraph for many Python repositories.

The recent additions to PySonar2 are intersection types, a more principled way of handling union types, and lots of improvements to its performance and simplicity. I’m also working on porting the same techniques to Ruby.

psydiff: a structural comparison tool for Python

(click on the above picture for a demo)

Psydiff is a structural comparison tool for Python, written in Python itself. The main algorithm and UI of psydiff is almost the same as ydiff.

If interested, you can see a demo of it here (psydiff comparing itself):

http://www.yinwang.org/resources/pydiff1-pydiff2.html

All the source code can be downloaded from my GitHub repo:

http://github.com/yinwang0/psydiff

It’s still in early stage of development. I appreciate your bug reports, feature requests or contributions.

Special thanks to Ronny Pfannschmidt for code contribution and suggestions.

(Note: This project was named “pydiff”, but I found that the name has already been taken for another project. Thus it is now renamed to “psydiff“, meaning “PYthon Structural diff” or “PSYcho diff” :=)

Null reference may not be a mistake

null

The null pointer is considered to be a “billion-dollar mistake” by Tony Hoare, but was he really saying that null pointer should never be used? After years of using languages both with null pointers (e.g. Java) and without them (e.g. Haskell), I found that null pointers are much easier and more natural to use than its counterparts (e.g. Haskell’s Maybe type). I have been wondering why there is such a notion of “billion-dollar mistake” until I saw the original video where Tony Hoare claims it to be his mistake. In fact, he didn’t really say that null pointer should not be used, so I realized that I made a mistake by taking the words “billion-dollar mistake” literally.

From this video, you can see that introducing null reference is not really a mistake. On the contrary, null references are helpful and sometimes indispensable (consider how much trouble if you may or may not return a string in C++). The mistake really is not in the existence of the null pointers, but in how the type system handles them. Unfortunately most languages (C++, Java) don’t handle them correctly.

Every class type A of Java is in fact a union type {A, null}, because you can use null anywhere an object of class A is expected. This is equivalent to the Maybe type of Haskell (where null in Java corresponds to Nothing of Haskell). So the trouble really is that an annotation like {String, null} should be distinguished from String, so that it will be clear what can possibly end up in the value. Unfortunately most languages don’t provide a convenient union type that you can put String and null together (Typed Racket is an exception). If Java is to have union types, we can say something like:

{String, null} findName1() {
  if (...) {
    return "okay";
  } else {
    return null;
  }
}

This is saying: findName may return a name which is a String, or it may return nothing. In comparison, we can say something slightly different:

String findName2() {
    ...
    return "okay";
}

By distinguishing the return types of findName1() and fineName2(), the type system knows that you should check for null when you have called findName1(), but you don’t need to check for null if you call findName2(). So you have to write something like:

String s = findName1();  
if (s != null) {
  x = s.length();      // use s as a String only after null check
}

But you may write:

String s = findName2();
x = s.length();

For the latter, you don’t have to check whether s is null because we know definitely that findName2() will return a String which is not null.

In fact this approach is hinted by Tony Hoare in the above video at 00:24.00. He said that null should be a class. Indeed, the union type {String, null} certainly thinks of null to be at the same status of String – it is a class.

But we soon realize that it doesn’t really matter whether null is a class or not since the class Null will have only one value — null. So any language with null references should work equally well given a correct type system.

Advanced static analysis tools can already help alleviate this issue by essentially inferring the union types like {String, null} even when the programmers write String instead, although a type annotation system which allows the programmers to specify union types directly certainly makes type checking easier and also makes programs easier to read.

Back to the future of databases

Why do we need databases? What a stupid question. I already heard some people say. But it is a legitimate question, and here is an answer that not many people know.

First of all, why can’t we just write programs that operate on objects? The answer is, obviously, we don’t have enough memory to hold all the data. But why can’t we just swap out the objects to disk and load them back when needed? The answer is yes we can, but not in Unix, because Unix manages memory as pages, not as objects. There are systems who lived before Unix that manage memory as objects, and perform object-granularity persistence. That is a feature ahead of its time, and is until today far more advanced than the current state-of-the-art. Here are some pictures of such systems:

IBM System/38

system-38

Lisp Machine

lisp-machine

Oberon

Oberon

Those systems don’t really need databases (in its usual sense). Data integration was seamless and transparent to the programmer. You don’t need to know the existence of a “disk”, a “file system”, or a “database”. You can just pretend that you can allocate infinite number of objects and work on them in the most natural way. Unfortunately most of those systems were either terribly expensive or had problems in other aspects of their design. Finally, they seemed to have died out.

Good ideas never die. This is not to say that there is nothing we can learn from their design. On the contrary, their ways are far superior than the current state-of-the-art of Unix-based systems. Unix will never reach this level of elegance and power.

But any how, Unix rules the world. We can live with it, but it is just mediocre. Please don’t believe everything that the modern Operating Systems books tell you. Sometimes you have to look further into the past for the future. As Einstein said, “Nothing is more needed to overcome the modernist’s snobbishness.”

Unix used to be free, but you get what you pay for. Although there is a thing called “virtual memory”, your programs can’t just allocate objects and then operate on them without any knowledge about the “file system”. Nothing works out-of-the-box in Unix. In fact it is far from that. Unix and its “philosophy” is a constant source of trouble. It is more like a “non-operating system” than an “operating system”. It leaves too much work for you to do, and leaves more than enough rope to hang yourself.

Unix builds its reputation and authority by blaming the users. If you don’t know how to use me, you are an idiot! This is the same trick that the weavers played on the emperor: If you can’t see the clothes, you are either stupid or incompetent. What a powerful way to cover the ass of any crap!

Unix’s incapability is why people “invented” databases. The combination “Unix + databases” is supposed to be a cheap replacement for those advanced systems where programs don’t need to know the existence of such a second-level data storage layer. But because of some irreparable design issues, Unix still can’t achieve that even with the help of databases. The databases, until today, still relies on Unix’s low-tech mechanisms such as memory mapped files to store data, which causes complications and performance issues.

However, databases were somehow considered a big thing, and people who made it became the richest men in the world. Consequently, you have to take database classes if you want a computer science degree. So here is an ultimate cheat sheet for those who really want to know what a database is. You will not need to sit through a semester’s course if you remember the few things that I put below. Trust me, many students got A+’s because I told them this ;-)

Every “row” in a database “table” is a data structure, much like a “struct” in C, or a “class” in Java. A table is then an array (or list) of such data structures. The “keys” of a database table are in essence “persistent memory addresses”. When serializing an object, we can’t just put the memory address of an object onto disk, because the address may not be the same when the object is reloaded into memory. This is why we need “keys”. In a sense, “keys” are a more general notion than “addresses” — addresses are just keys that are integers.

There is a white lie in the above paragraph – I didn’t mention that there is some redundancy in a database table in comparison to a serialized data structure. Some data is duplicated across multiple rows because a RDBMS table row has fixed width, so it can’t store variable length data such as arrays. What can you do then? By recognizing that the table is the only thing that can “grow” in a relational database, an obvious solution is to turn the array 90 degrees clockwise, and make each element a row in another table! But how do you connect from where the array is originated from? You add the key of the object to each row of this new “array table”. See how the key is duplicated? This is why people “invented” column-based databases (such as Vertica, HBase etc) for “compressing” these keys. But what they achieved was essentially making the tables slightly closer to the format of serialized data structures.

You create the problem, and then you solve it. And you call this two inventions.

Keys are persistent pointers. Whenever you need to dereference a pointer, you do a “join” in the database, so “join” is equivalent to “following pointers”.

A database “schema” is in essence a “structure type”, like the struct definition in C. For example, the schema created by the following SQL statement

CREATE TABLE Students ( sid CHAR(20),
                        name CHAR(20),
                        login CHAR(20),
                        age INTEGER,
                        gpa REAL )

is equivalent to the C struct

struct student {
  char* sid;
  char* name;
  char* login;
  int age;
  double gpa;
}

(Note that I use a SQL declaration here just because I don’t want to draw a picture of the schema. This equivalence of a relational schema with a structure type has nothing to do with SQL.)

That’s almost the whole story. You have addresses, pointers, dereference operation, structure types, arrays/lists of structures, so now you can implement things like linked lists, graphs etc. With them, you can implement some complicated algorithms such as A* search in a database. You just need to take a data structure class, and then translate what you learned there into a database language like SQL.

But SQL is a crappy language. It wasn’t designed for programmers. It was designed for manual input by human operators (usually non-technical people like accountants). You type in a “query”, and the computer prints out a “response”. That is why it is called a “query language”. This language does its job for human operators, but it was then abused beyond its capabilities. It was interfaced with computer programs to write serious programs. I doubt if those people knew what they were doing, but it just happened, like many other silly things. There are just so many things you can’t express in that language. The result is a dumb and fragile system held together by band-aids. You have to be very careful otherwise you lose blood.

If you really want to learn SQL, here is the cheat sheet for it:

The query

SELECT Book.title
 FROM Book
 WHERE price > 100

is equivalent to the Lisp expression

(map (lambda (b) b.title)
     (filter (lambda (p) (> p 100)) Book)

<

p>This program is then sent to the “database engine” for execution. That is, we move the program to the data, instead of loading the data to the program. And that’s also the principle behind MapReduce. Have you noticed how easy this can be done with Lisp? You just send the code to the interpreters running on remote machines!

The problem with SQL is that you need yet another layer of language before programs can operate the database. SQL is a weak and quirky language. It is not Turing-complete and at some places it doesn’t even “compose”. You need to combine it with a decent language before you can write serious programs. Your programs send SQL commands to the database to store and load data, just like a human operator would do. This is a very low-tech way of data integration. It is error-prone, inefficient and subject to security risks such as “SQL injection”.

Indeed, there is a “good component” in SQL, because it has some “relational programming” features. However, the other word for “relational programming” is “logic programming”, where languages like Prolog and Datalog excel. They are both more expressive and more elegant than SQL. Considering that Prolog and Datalog appeared much earlier than SQL (1972, 1977 v.s. 1986), I would say that SQL is a step backwards.

Maybe you have seen, for some weird reasons we are still in the Dark Ages of computer programming. We are not supposed to be here since better designed systems already existed. It would be foolish to dismiss them as failures. They are just ahead of their times. By looking to the past, we see a way back to the future.

Why is indexing faster than binary search

We all know that indexing into an array takes only O(1) time, while searching for a number in a sorted array takes O(n) time with linear search, and O(log n) time with binary search. But why is indexing so fast? What is the secret sauce?

The reason is really about the nature of indexing — how it is implemented in a circuit. In order to illustrate this, let me show you an “addressing circuit”.

addressing cuicuit

Here, A and B are the two-bit address lines, they represent the indices: 00, 01, 10, 11. The output Z, Y, X and W are the selectors of the items in the array. Notice that an output selector is enabled only when both of the input lines of the corresponding AND gate is “1″.

Now, ignore the input B and just look at A. See how its signal flows through the direct wires and the inverters. We can make the following observations:

  • When A is “1″, then the AND gate of X and W will receive a “1″ on one of their input ports, while the AND gate of Z and Y will receive a “0″ on one of their input puts.
  • On the other hand, if A is “0″, then the AND gate of X and W will receive a “0″ on one of their input ports, while the AND gate of Z and Y will receive a “1″ on one of their input puts.

From the above, I hope you have seen that the value of A partially selects half of the AND gates — it is either the set {X, W} or {Z, Y}. By “partially select”, I mean they are not fully selected, because we haven’t taken B into account. At this point, I hope you have noticed that A is in fact doing one step of a “binary search”.

Now we do a similar thing, but this time focus on B and ignore A. You should see a similar thing: depending on the value of B, either we partially select {Y, W}, or we partially select {Z, X}. So we can also think of B as doing one step of a “binary search”.

Now, we see that A and B are each a step of a binary search, and it is interesting to see that B’s selection will cut A’s selection evenly, whether A is 0 or 1. We can say the same thing vice versa: A’s selection will cut B’s selection evenly, whether A is 0 or 1.

Also notice that the selection of A and B can happen at the same time. That means, when they work simultaneously, it takes just O(1) for a binary search through an array of length 4. If we generalize this circuit to N bits of input, then within O(1) time, we can do a binary search through an array of length 2N.

This explains why indexing an array is faster than binary search, because it is a parallel binary search where (log n) steps happen at the same time.

On pureness

It is usually a pleasure to use a functional programming language, but it is doubtful whether we should care about the “pureness” of the language. To write programs in a completely pure functional programming language (e.g. Haskell) is much like living in a wired world.

There are no electromagnetic waves nor sound waves in such a world, so you don’t have wifi, cell phones, satellite televisions, radios, etc. You don’t even have light or sound. In other words, everything is blind and deaf.

All information must pass through wires or pipes, connected by switch boxes which we call “monads”. You must carefully route all the wires and pipes and connect them correctly before any information processing device, including your eyes and ears, can properly work.

So I think a language will need parts of it not to be pure, in order to naturally represent the effects such as electromagnetic waves. Normally those effects are called “benign effects“.

Undecidability proof of the halting problem without diagonalization

As a TA for a graduate level Theory of Computation course, I don’t understand why we have to teach the diagonalization proof of the undecidability of the halting problem. It is much easier if we just use a normal argument about functions in a programming language. Basically, functions correspond to Turing machines in a theory of computation context. In order to improve the situation, I came up with a simpler formulation based on the view of “Turing machines as functions”.

Suppose that we have this function Accept(M,w) which takes two arguments, a function M and its input w, and can tell you whether or not M(w) will output True. Basically, suppose that Accept is the hypothetical solver for the halting problem. To connect to usual theory of computing terminology, the fuction M corresponds to a Turing machine, True corresponds to reaching an accept state, and False corresponds to reject state. Note that although the argument M may go into infinite loops, never will Accept.  Accept always returns True or False in a finite amount of time.  Accept determines this without actually running M because M may go into an infinite loop and never return. This way of finding properties of programs without running them is usually called static analysis. It has the same essence as fortune-telling and all other sciences.

Now we come to our simple contradiction: does the following expression (call it F) return True or False?

Accept(λm.not(Accept(m,m)), λm.not(Accept(m,m)))

It turns out that this question cannot be answered at all! If F returns True, then when we actually apply the function λm.not(Accept(m,m)) to the argument λm.not(Accept(m,m)), it should return True, right? But when we apply it, we get

not(Accept(λm.not(Accept(m,m)), λm.not(Accept(m,m))))

Notice that it is exactly the negation of the original expression F. This means that F should return False (because the “actual run” returns False). On the other hand, if F returns False, then when we actually apply the function on its argument, it will return True. Thus the contradiction. QED.

Some may argue that I’m implicitly using “diagonalization” here. Well, you can say that they are equivalent in effect, but the equivalence doesn’t mean that “diagonalization” is a good word for describing what I’m doing. Actually I’m just making a loop in a “circuit”. I don’t see the diagonal, then why call it that way? The diagonal argument and the “loop argument” may have the same essence, but they are very different in their comprehensibility. I feel that the loop way is a much easier to understand than diagonalization.

An interesting final question may be, what is the connection between the above expressions with the Y combinator?

λf.(λx.f(x x)) (λx.f(x x))

A mind map guide for TeXmacs

TeXmacs was my best kept secret for homework assignments and papers with lots of mathematical formulas. It is a state-of-the-art typesetting system with unparalleled beauty. Many people think that it is just a “frontend” of TeX/LaTeX (like LyX) but they are very wrong, because TeXmacs is fundamentally superior than TeX. TeXmacs is a fully independent software, with the same or even better typographical quality than TeX but with much more intuitive and beautifully designed interface.

The editor environment is just amazing. It is 100% WYSIWYG. Yep, 100%. That means, the screen shows exactly what you would print out on paper. I don’t know of any word processor (including MS Word) that can do this today. If you haven’t used TeXmacs before, it would refresh your mind about what the word WYSIWYG really mean.

I know exactly what you would argue now, TeXers, but listen—with all the beauty, you don’t lose detailed control of document structure. You will be surprised to find out that it is also WYTIWYG (What You Think Is What You Get), and it has exploited this notion to the extreme. You will sense a “human centered” design in it.

So, ready for a try? Just download it (free) and dive in. Over the years, I have accumulated lots of useful knowledge regarding its use and have collected them into a mind map. Click on the following image and you can see all my best tricks with this software. Have fun!

Understanding the yin-yang puzzle

I have a friend who is a very fast learner. I introduced him to the Scheme programming language a few days ago and he soon digged into this yin-yang puzzle:

(let* ((yin
        ((lambda (cc) (display #\@) cc) (call/cc (lambda (c) c))))
       (yang
        ((lambda (cc) (display #\*) cc) (call/cc (lambda (c) c)))))
  (yin yang))

This program prints out the infinite string @@@@****@*****@****** …

Why does this happen? This took me almost a full afternoon to figure out. It is always good to have friends who feed you with questions and challenges. I’m going to document my finding here. I may want to make some animated slides (as is always a good idea) later, but for now a short note may suffice.

The Plan

You will probably never understand the program if you examine the contents of the stack. You need their high level semantic meaning to think clearly. The higher level meaning of the stack is the continuation. So instead of frightening you with the details of the stack, I’m going to use functions to show the continuations explicitly.

Also I will use a little bit of compiler optimizations along the way. The optimizations will simplify the program and show its deeper meanings.

Here is an overall plan of this article:

  1. Find the functional representations of the two continuations. Name them c1 and c1.
  2. Plug in c1 and c2 into the places of the two call/cc’s.
  3. Simplify the program using compiler optimizations.
  4. Perform behavioral analysis on the simplified program.

Transform and Remove Call/cc

So here we go. Let’s repeat the original program here:

(let* ((yin
        ((lambda (cc) (display #\@) cc) (call/cc (lambda (c) c))))   ; B1
       (yang
        ((lambda (cc) (display #\*) cc) (call/cc (lambda (c) c)))))  ; B2
  (yin yang))

Note that there are two binding clauses, B1 and B2, each prints a char and binds a continuation to a variable.

B1 binds yin to the “current continuation” of the first call/cc. Let’s call this continuation c1. Its function representation is:

(lambda (k)
  (let* ((yin
          ((lambda (cc) (display #\@) cc) k))           
         (yang
          ((lambda (cc) (display #\*) cc) (call/cc (lambda (c) c)))))          
    (yin yang)))

We can simplify it using some compiler optimization tricks. I will go very slowly here just in case you are not familiar with compiler optimizations.

First, since Scheme is a strict language, k will be a pure value (with no side-effects), so we can lift the side-effect (display #\@) out:

(lambda (k)
  (display #\@)
  (let* ((yin
          ((lambda (cc) cc) k))           
         (yang
          ((lambda (cc) (display #\*) cc) (call/cc (lambda (c) c)))))          
    (yin yang)))

Now we can “partial evaluate” ((lambda (cc) cc) k) to k:

(lambda (k)
  (display #\@)
  (let* ((yin k)           
         (yang
          ((lambda (cc) (display #\*) cc) (call/cc (lambda (c) c)))))          
    (yin yang)))

Then we can copy propagate the value of yin, k, to the body of let*, (yin yang). And now we have only one binding left:

(lambda (k)
  (display #\@)
  (let ((yang
         ((lambda (cc) (display #\*) cc) (call/cc (lambda (c) c)))))
                                         ^^^^^^^^^^^^^^^^^^^^^^^^
    (k yang)))

Now we try to figure out the underlined continuation. It should be:

(lambda (j)
  (let ((yang
         ((lambda (cc) (display #\*) cc) j)))
    (k yang)))

You see why? Since the “current continuation” means “what is going to happen with this value”, it doesn’t include the computation before it, namely (display #\@). Now we do a similar optimization on this continuation: lifting out the side-effect (display #*), do some partial evaluation and copy propagation:

The result of this inner continuation is:

(lambda (j)
  (display #\*)
  (k j))

Now we can plug it back:

(lambda (k)
  (display #\@)
  (let ((yang
         ((lambda (cc) (display #\*) cc) 
          (lambda (j)
            (display #\*)
            (k j)))))
    (k yang)))

Do a similar sequence of optimizations: lifting out the first (display #*), partial evaluation, copy propagation. And we have the final result for the value of yin. Let’s name it c1 with a definition:

(define c1
 (lambda (k)
   (display #\@)
   (display #\*)
   (k (lambda (j)
        (display #\*)
        (k j)))))

Now, the original program would look like the following. The program would have by now printed a @ before binding yin to c1, so we make a sequence and include the display term in the front of it.

(begin
  (display #\@)
  (let* ((yin c1)
         (yang
          ((lambda (cc) (display #\*) cc) (call/cc (lambda (c) c)))))
    (yin yang)))

Try it. It will behave the same as the original program. Now we do another copy propagation to get rid of the first binding:

(begin
  (display #\@)
  (let ((yang
         ((lambda (cc) (display #\*) cc) (call/cc (lambda (c) c)))))
    (c1 yang)))

Since the call/cc here will not cause any side-effects (why?), we can lift (display #*) out:

(begin
  (display #\@)
  (display #\*)
  (let ((yang
         ((lambda (cc) cc) (call/cc (lambda (c) c)))))
                           ^^^^^^^^^^^^^^^^^^^^^^^^
    (c1 yang)))

Now we just have to find what this underlined continuation is, and it will become the value of yang. It is:

(lambda (k)
  (let ((yang
         ((lambda (cc) cc) k)))
    (c1 yang)))

After our routine sequence of optimizations we have the value of yang. Let’s define it as c2:

(define c2
  (lambda (k)
    (display #\*)
    (c1 k)))

Plug c1 and c2 back into the original program:

(begin
  (display #\@)
  (display #\*)
  (let* ((yin c1)
         (yang c2))
    (yin yang)))

And do a copy propagation:

(begin
  (display #\@)
  (display #\*)
  (c1 c2))

Transformed Program

Now we have our final transformed and optimized program. Let’s put the definitions of c1 and c2 here for an overview:

(define c1
 (lambda (k)
   (display #\@)
   (display #\*)
   (k (lambda (j)
        (display #\*)
        (k j)))))

(define c2
  (lambda (k)
    (display #\*)
    (c1 k)))

(begin
  (display #\@)
  (display #\*)
  (c1 c2))

For simplicity, let’s inline c2 into the main program. Now c2 disappears.

(define c1
 (lambda (k)
   (display #\@)
   (display #\*)
   (k (lambda (j)
        (display #\*)
        (k j)))))

(begin
  (display #\@)
  (display #\*)
  (c1 (lambda (k)
        (display #\*)
        (c1 k))))

Try it. It will still work the same as the original program.

Behavioral Analysis

Now the program doesn’t contain any call/cc’s and is much easier to understand. Let’s try to figure out how it executes:

  1. First, @* will be printed, and we will invoke:
(c1 (lambda (k)
      (display #\*)
      (c1 k)))
  1. Inside the invocation, @* will be printed by the body of c1, and k is now bound to (lambda (k) (display #*) (c1 k)). So the program proceed to:
((lambda (k)
   (display #\*)
   (c1 k))
 (lambda (j)
   (display #\*)
   ((lambda (k)
      (display #\*)
      (c1 k)) 
    j)))

It will print a *, and becomes:

(c1
 (lambda (j)
   (display #\*)
   ((lambda (k)
      (display #\*)
      (c1 k)) 
    j)))

Now we have seen @*@**

  1. Notice that we are back to a call to c1! This is a good sign of recursion. But this time the argument is different. If we simplify it a little, we get:
(c1
 (lambda (j)
   (display #\*)
   (display #\*)
   (c1 j)))
  1. I think you see what’s going on here. This time, c1 is called with
(lambda (j)
   (display #\*)
   (display #\*)
   (c1 j))

which means “When called, display TWO *’s, and then behave like c1 on the argument”. If we go on, the argument to c1 will be longer and longer, and each time with an additional (display #*). It will print @***, and then @****, and then @*****, and so on.

  1. Let’s introspect a bit. Which part of the program is responsible for creating the ever-longer displays, and why? It is this piece from the definition of c1:
(k (lambda (j)
     (display #\*)
     (k j)))

Here k is c1′s argument. Notice that k is always of the form:

(lambda (j)
   (display #\*)
   (display #\*)
   ...
   (c1 j))

When k is applied, it will print the corresonding number of *’s inside it, and then behave like c1. The argument to k is:

(lambda (j)
  (display #\*)
  (k j))

What does this mean? It says: “When called, print a * and then behave like k on the argument.” This is how you get a “new k”, with one more display of *.

This will go on indifinitely. This is why you see the infinite string: @@@@****@*****@****** …

On software design patterns

In this post I try to answer the contraversial question

Are software design patterns good or bad?

This used to be a long post, but I have since condensed it into a very short one, thanks to the pictures. One picture is worth ten thousand words. Hopefully you will have understood most of Richard Gabriel’s 239-page book after looking at the following two pictures.

  1. Here are some nice design patterns. You can use them to decorate the floors in your house.

  2. Here is a masterpiece. Can you construct it using the above patterns, or any patterns at all?

I think the answer is already obvious. One cannot produce a masterpiece by just putting patterns together. Artists know that techniques are never as important as vision. That is why they spend their lives studying the nature of things such as the human body. Once they get hold of the essence, they use whatever techniques at hand to express what they want. They can also change the techniques or invent new ones as needed.

The same holds for computer programming. We need to keep in mind that design patterns are means and not ends. True programmers are never constrained by existing patterns. They observe and grasp the essence of things, inventing new techniques and patterns as needed.

Concurrent stack does not exist

Some weeks ago I read this thought-provoking article by Nir Shavit Data Structures in the Multicore Age. The topic is about efficiency of concurrent data structures. There have been many thinkings going on after the reading, but the most interesting point to me is that the author started trying to use a “concurrent stack”, but ended up happily using a pool.

“In the end, we gave up the stack’s LIFO ordering in the name of performance.”

Now there can be several interesting questions to ask. Can we give up some property of a data structure if it is crucial to the correctness of the program? If we can give up the LIFO ordering, then why did we think we need a stack? But the most interesting question is probably:

Does a “concurrent stack” really exist?

I think the answer is No — a “concurrent stack” hasn’t really existed and will never exist. Here is why:

  1. If the threads are allowed to push and pop concurrently, then the “stack” can’t really maintain a LIFO order, because the order of the “ins” and “outs” is then indeterminate and contingent on the relative execution speeds of the threads.
  2. If the execution of two threads strictly interleave. Each time a “pusher” pushes an element, a “popper” immediately pops it out, then this is a FIFO order, a queue.
  3. If a pusher pushes all the elements before a popper starts to pop all of them out, then this is indeed a LIFO order, a stack. But notice that there is no concurrency in this case — the executions of the threads must be completely sequential, one after another.
  4. If two threads interleave randomly, or there are more than two threads accessing the “stack” at the same time, then nothing can be said about the access order.

From the above, we can see that there is a fundamental conflict between the two notions, “concurrency” and a “stack”.

If a “stack” can be accessed concurrently, then there is no way we can maintain a LIFO order. On the other hand, if we enforce a LIFO order, then the stack cannot be accessed concurrently.

If we have realized that the essence of a stack is a continuation, and a continuation (by itself) is sequential, then it is no surprise we arrive at this conclusion.

Since a LIFO order is essential to a stack, we can’t call the data structure a “stack” if we can’t maintain a LIFO order.

We can’t call a data structure a “stack” just because it has the methods named “push” and “pop” — we have to look at what the methods actually do.

Even if we continue to think that we are using a stack, the threads are in effect just distributing messages, with the operations “push = send” and “pop = receive”. So in essence this data structure is a pool. This exactly justifies the author’s relaxation to a pool, although no actual relaxation happens — the data structure has been a pool from the beginning. It was just disguised as a stack and less efficient.

So we see that the concept of a “concurrent stack” does not really exist. We also see that some data structures we have in the sequential world may not have concurrent counterparts.

How to reinvent the Y combinator

I always believed that one can never learn the essence of anything without reinventing it. Once you reinvent things, you will never forget them — because otherwise you can just re-reinvent them.

Today I found that I forgot how to derive the defintion of the Y combinator. I learned it several years ago from an online article, but now the search “Y combinator” only brings me news about start-ups (sigh). I tried for two hours, but still couldn’t make the leap from the “poor man’s Y” to “Y”. Finally, I opened my good old friend The Little Schemer. Alas. Chapter 9 tells me exactly how to reinvent Y. Thank you Dan Friedman and Matthias Felleisen!

To prevent myself from forgetting how to derive Y again, I made a slide to record my understanding of it. I hope it can be of help to people (including the future me). So here it is.

Exercise: The Y combinator derived from this tutorial only works for direct recursion, try to derive the Y combinator for mutual recursive functions, for example the following two functions even and odd.

(define even
  (lambda (x)
    (cond
     [(zero? x) #t]
     [(= 1 x) #f]
     [else (odd (sub1 x))])))

(define odd
  (lambda (x)
    (cond
     [(zero? x) #f]
     [(= 1 x) #t]
     [else (even (sub1 x))])))

A reformulation of reducibility

I found the theory of computation books very imprecise about their descriptions of Turing machines and reductions. They usually start with something precise and mathematical, for example they would define a Turing machine as a 7-tuple, but after that, everything about decidability and reduction is described with impenetrable paragraphs in natural languages.

I believe that the use of natural languages leads to most of the confusion in theory of computation because natural languages are inherently imprecise and ambiguous. There are too many ways to say the same thing. For example, you can find these sentences which mean exactly the same in the books:

  • “Run M on w”
  • “Run M on input w”
  • “Simulate M on w”

The pronouns and references are even more confusing. For example:

“Use the description of M and w to construct the TM M1 just described.”

What is “just described”, and do M and w here mean the same things as in the earlier paragraph?

Another serious problem is that natural languages are very weak at representing the notion of “interpretation”, which underlies much of theory of computation. For example, a Turing machine simulates another Turing machine, which again contains and simulates yet another one.

After some thought, I found that we could use something precise such as mathematical notations combined with programming languages to describe the concepts. As an example, I’ll show here how the notion of reduction can be defined precisely as a homomorphism which can be instantiated for reducing one problem to another.

Definition 1 (reduction): A reduction (as in theory of computation) is a homomorphism (as in universal algebra):

Reduce(TM, I) = (TM', I')

satisfying the property

TM @ I = TM' @ I'

where

  • TM = Turing machine which we reduce from
  • TM' = Turing machine which we reduce to
  • I = input string of TM
  • I' = input string of TM’
  • @ = simulation, similar to the Scheme code ((eval TM) I)
  • TM @ I = result from simulating TM on I (accept or reject)
  • TM' @ I' = result from simulating TM’ on I’ (accept or reject)

End of Definition 1.

Notice that the simulation (TM @ I) may go into an infinite loop and never produce any result. Now I show how to use this homomorphism to describe the reduction from ATM ==> HALT, where

  • ATM = the “acceptance problem” (deciding whether a Turing machine M accepts string w)
  • HALT = the “halting problem” (deciding whether a Turing machine M halts on string w)

For convenience, we let

  • DATM = “the decider of ATM”
  • DHALT = “the decider of HALT”

Now the reduction can be fully described by the following homomorphism:

Reduce(DATM, (M,w)) = (DHALT, (M',w))
where
  M' = <if (M @ w) then accept else loop>
satisfying
  DATM @ (M,w) = DHALT @ (M',w)

Yes, that’s an all-inclusive formal proof that HALT is undecidable. It even includes the notion of “reduction” itself.

Let me explain it a bit. The first line says that there exists a function (named Reduce) from the pair (DATM, (M,w)) to another pair (DHALT, (M',w)), where M' = <if (M @ w) then accept else loop> is a description of a Turing machine.

Now let’s look at the last line:

DATM @ (M,w) = DHALT @ (M',w)

It says: if we have a decider for HALT (DHALT), then we can use it to define DATM, thus deciding ATM.

Why this is a valid defintion for DATM? This is because from the definition of M'

<if (M @ w) then accept else loop>

we know that:

  • If (M @ w) accepts, M' accepts, thus DHALT @ (M',w) accepts
  • If (M @ w) rejects, M' loops, thus DHALT @ (M',w) rejects
  • If (M @ w) loops, M' loops, thus DHALT @ (M',w) rejects

Notice from the colored words that DHALT @ (M',w) will accept if and only if M accepts w. Thus this defines a decider for ATM.

So if DHALT exists, then we can have DATM. But this contradicts the fact that DATM cannot exist, so DHALT must not exist.

If you wonder how this proof corresponds to Definition 1, here is some details how it is instantiated:

  • TM = DATM (nonexistent)
  • TM' = DHALT (hypothetical)
  • I = (M,w) where M is the description of a Turing machine which we want to know whether it accepts input w.
  • I' = (M',w) where M' is <if (M @ w) then accept else loop>
  • TM @ I = DATM @ (M,w) (running decider of DATM on input (M,w))
  • TM @ I' = DHALT @ (M',w) (running decider of DHALT on (M',w))

This is a lot more concise, accurate and easier to understand than a paragraph:

F = "On input <M,w>:
  1. Construct the following machine M'
     M' = "On input x:
        1. Run M on x.
        2. If M accepts, accept.
        3. If M rejects, enter a loop."
  2. Output <M',w>."

A bug in GHC’s type system

Several days ago, I implemented an experimental type inference system with first-class polymorphism. When comparing it with other systems, I found a possible bug in GHC’s type system regarding universal quantification. The phenomemon was confirmed and reproduced by people at #haskell IRC channel for GHC versions above 7.01. The code that causes trouble is:

gen :: [forall a. a -> a]
gen = [id]
test1 = head gen 1

Obviously this program should typecheck, since:

  • id has the type forall a. a -> a.
  • A list gen containing id should have type [forall a. a -> a](as in the annotation).
  • head has the type forall a. [a] -> a.
  • head gen should have the type forall a. a -> a.
  • head gen should be able to be applied to 1.

But GHC rejected this program for a strange reason.

Couldn't match expected type `t1 -> t0'
with actual type `forall a. a -> a'
Expected type: [t1 -> t0]
Actual type: [forall a. a -> a]
In the first argument of `head', namely `gen'
In the expression: head gen 1

On the other hand, it works if (head gen) is bound at let:

test2 = let hg = head gen in hg 1

It doesn’t break the soundness of the type system since it only rejects some correct programs, but this kind of pecularities of type systems can be painful when they add up. I guess this may be caused by the interaction between GHC’s internal type system with the legacy let-polymorphism.

On point-free programming

Concatenative programming, or point-free style, is useful sometimes, but has some serious drawbacks similar to the SKI combinators. Applicative programs can be compiled into point-free style easily, but writing and reading them directly in large scale is usually a mental burden.

It only works well with functions with one or two arguments. Concatenation of functions with more than two arguments will not be so convenient. If the receiver has an argument order that is different from the sender’s output order, you will need a non-trivial permutation of argument order.

For example, if the function is defined as:

f :: Int -> String -> Bool
f x y = ...

If you want to use it as the predicate for filtering a list of strings, that’s fine. You just write something like filter (f 2) .... But what if you want to filter a list of integers? Then you will need to swap the order of the first two arguments before you can do the partial application. So you write filter (flip f 2) .... Fine. But what if the function looks like:

g :: Int -> A -> String -> Bool
g x y z = ...

And you want to filter a list of A’s? Which function do you use to switch the argument order, and you expect the reader of the program to learn it?

What about functions with four arguments. Notice that there are 4! = 24 different argument orders. How many order switchers do we need?

In order to prevent this kind of plumbing, we have to take unnecessary care when we decide the order of the parameters. This often makes the function look ugly.

Names are more convenient. Notice that even mathematics uses names for permutations (as in algebra):

(a b c d)
(b a d c)

Concatenative programming is like connecting the components of a circuit. But even electronic engineers don’t do it this way. They use net-lists with names and labels.

Names are essential and useful in most cases. Concatenative programming, although nice when used sparsingly, may not be good to serve as a major way of composition.

At this point, I found this sentence from Tao Te Ching (Chapter 1) especially relevant:

“The nameless is the origin of Heaven and Earth
The named is the mother of myriad things”

On literate programming

A friend and I had a discussion about the current trends of programming methodologies. At some point, the topic turned to Literate Programming (LP). I personally have written a non-trivial literate program (in CWEB) a few years back, but like many other people, I did not persevere. As a hindsight, there are some good reasons why people do not adopt LP.

Missing the big picture

Although we love books, they may not be the best medium for documenting programs. Programs are much like circuits or cars. They are very complex systems with interconnected parts. The interactions and constraints among the parts can’t really be understood when they are taken apart.

LP systems usually segments the program into small pieces and rearrange them into a book-like order. This is like taking a car apart when teaching car-making. There is a huge loss of structural information in this rearrangement. It may be useful to take some parts out for explanations and experiments, but they should be placed back immediately after examination. The student must have a clear view of the overall structure of the car.

If we take all the parts out and lay them along the road, the student would have trouble figuring out how they would fit and work together. In short, the student see trees and not the forest when reading a book generated by Literate Programs.

Programs are not text

LP systems usually allow programmers to fragment a program into small pieces, reorder the pieces into an order that is “convenient to the human mind”. Later on, a program (weave) generates printable documentation for the program; another program (tangle) assembles the fragments into machine-executable code.

However, these systems have a big problem — treating programs as text. LP systems usually don’t parse the programs. They just segment the code textually. This often messes up the variable scopes and causes subtle bugs. This is much like macros in early Lisps and C, extremely dangerous and error-prone.

There are other kinds of LP systems such as Literate Haskell, CoffeeScript etc. They don’t break up the procedures and don’t have the above “hygiene problem”. But because we already have the freedom to rearrange the order of procedures in any programming language, those systems are nothing more than a fancy comment facility like JavaDoc. In views of authentic literate programmers, those systems miss the essence of LP.

Human supremacy, human languages and human cognition

LP systems rely their arguments on a false belief in human supremacy, an overemphasis in human languages, and a misunderstanding of human cognition. Practice has shown that the human brain is incapable of competing with computers in anything that requires rigorous reasoning and perseverance. Natural languages are woefully inaccrurate and confusing for programming. Any programming language that tries to mimic natural languages is doomed to suffer the same “design flaws” of natural languages (for example SQL).

It is also doubtful whether the order set by literate programming is suitable for human cognition at all. Programs should be constructed in an order that matches the nature of the concept it models, and not in the order of a particular person’s way of thinking, nor in the arbitrary order set by a compiler. Once the program structure matches nature, it will immediately appeal to human understanding.

So instead of investing in LP, a probably better direction is to investigate better ways of representing programs that enable them to match the concepts more naturally. Functional Programming and Logic Programming are gradually moving toward this direction.

Painful code navigation

Once the code is weaved into a book, it will be very hard to navigate through. Several years ago, I spent some time reading Knuth’s MMIXware, a book generated from a CWEB program. I noticed how much time I spent on finding definitions and cross-references of variables. Although Knuth painstakingly constructed an index for the book, obviously I still had to turn hundreds of pages back and forth, while in IDEs I can jump to the definition of a variable with just one keystroke. One should wonder why we bother publishing code as books at all.

From these observations, it is really unclear how literature and books can serve as a good medium for programs. The world has changed and technology advanced, instead of pursuing something static and classic, we may just need to open our minds to new kinds of media.

Indentation-based syntax considered harmful

Although the idea of layout syntax—using whitespace characters to delimit blocks—has been promoted by several languages (notably Python and Haskell), I feel that this kind of syntax brings more trouble than benefits.

It takes just one keystroke to produce a serious bug

In most languages a program’s format is determined by its meaning, but in a language with layout syntax, its meaning is determined by the format. This makes programs in layout syntax fragile because a tiny change in format could result in a serious error. For example, consider these two Python programs:

# correct definition
def member(x, ls):
    for y in ls:
        if x == y:
            return True
    return False         # correct indentation
# incorrect definition
def member(x, ls):
    for y in ls:
        if x == y:
            return True
        return False     # incorrect indentation

The second definition has been “derived” from the first by an inadvertent TAB key, which indented the return statement one more level to the right. While the two definitions differ only in one indentation, they produce totally different results. The first definition is correct, while the second has serious bugs:

  1. If ls is non-empty, it will always return False whether x is an element of ls or not.
  2. If ls is empty, it will return None (instead of False) because there is no return statement after the for-loop, a “missing return statement” bug.

Although this is just a minimal example, the bug may take quite some time to show up and be fixed. In order to prevent this kind of bugs from happening, I often find myself moving the cursor up-and-down in a straight line to check the alignment of the statements.

Let’s see why this bug cannot happen in a language which does not use layout syntax. We now invent an alternative syntax for Python, so that the pervious program looks like:

def member(x, ls) {
    for y in ls {
        if x == y {
            return True
        }
    }
    return False
}

Given the correct definition, can you imagine how you could reproduce the bug with just one keystroke? It is almost impossible. To see why:

  1. The return statement can never get into the loop with a change in indentation.
  2. It takes at least two edits and one movement in the editor to move the return statement into the loop. There are two alternatives to choose from:
    • Cut return False. Move the cursor into the closing curly brace of the for-loop. Paste.
    • Delete the closing curly brace of the for-loop. Move the cursor beyond return False. Insert an closing curly brace.

Either way, you must be deliberate and precise in order to reproduce the bug. Otherwise the parser would have complained (for example, if you just delete a closing curly brace).

However, the situation is very different with layout syntax, where one TAB key press produces the same amount of change as the above three operations. The change happens quickly and the program remains grammatically correct, obscuring the presence of a bug.

The situation is a little better for Haskell, because incorrect indentations often cause type errors and the programmer will be alerted, but in either languages, it takes quite some time to fix this kind of bugs.

Unconvincing advantages

It is often claimed that layout syntax has the following advantages over curly braces:

  • Your programs become a lot shorter because less curly braces are used.
  • You write less clutter such as curly braces and semicolons, and that beautifies your code.

I found that neither of the two advantages convincing. For the first part, Python and Haskell programs are indeed several times shorter than equivalent Java or C programs, but this cannot really be creditted to layout syntax.

We need to have some blank lines even in a Python or Haskell program, between definitions and sometimes in the middle of a block. The blank lines naturally denote groups of statements. So if we count the number of additional lines introduced by curly braces, we will find that there aren’t many. Curly braces also naturally denote statement groups, so not only they don’t look bad, they are helpful.

In Python and Haskell, it is the semantic features (pattern matching, first-class functions etc.) that make the programs short, not layout syntax. If we had an alternative syntax of Java which uses layout, then Java programs would still be several times longer than equivalent Scala programs. Java programs are longer not because they use curly braces, but because they don’t have things such as first-class functions, so they have to use some tedious design patterns.

Second, layout syntax does not really save “clutter”. Even in a language with layout syntax, we may still need to write almost the same amount of (if not more) clutter. The following is a random piece of code taken from the current release of GHC. We can still see lots of curly braces and semicolons in it. I guess layout syntax actually caused trouble, so the authors of GHC decided that they will just write curly braces.

tcInstanceMethodBody skol_info tyvars dfun_ev_vars
                     meth_id local_meth_id
             meth_sig_fn specs
                     (L loc bind)
  = do  {       -- Typecheck the binding, first extending the envt
        -- so that when tcInstSig looks up the local_meth_id to find
        -- its signature, we'll find it in the environment
          let lm_bind = L loc (bind { fun_id = L loc (idName local_meth_id) })
                             -- Substitute the local_meth_name for the binder
                 -- NB: the binding is always a FunBind

    ; (ev_binds, (tc_bind, _))
               <- checkConstraints skol_info tyvars dfun_ev_vars $
          tcExtendIdEnv [local_meth_id] $
              tcPolyBinds TopLevel meth_sig_fn no_prag_fn
                 NonRecursive NonRecursive
                 [lm_bind]

        ; let full_bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
                                   , abs_exports = [(tyvars, meth_id, local_meth_id, specs)]
                                   , abs_ev_binds = ev_binds
                                   , abs_binds = tc_bind }

        ; return (L loc full_bind) }
  where
    no_prag_fn  _ = []      -- No pragmas for local_meth_id;
                        -- they are all for meth_id

Better ways to save clutter

Even if we do hate curly braces, there are better ways to reduce or even completely eliminate them. For a trivial “solution”, we could just use a dim color for curly braces and semicolons in the editor, so that they are less noticeable. For example the above Python program in that curly bracy syntax could look like this in your editor:

def member(x, ls) {
    for y in ls {
        if x == y {
            return True
        }
    }
    return False
}

Better still, we could use a structural editor that lets us manipulate the AST (abstract syntax tree) directly. Those editors could provide several options of denoting blocks. You can switch between colored blocks, curly braces, or nothing at all. You can switch the look of your code at any time, instantly. People have implemented such editors, for example this editor designed by Kirill Osenkov.


Re-indentation hassle

In a language that doesn’t use layout syntax (Java, C, Scheme, …), no re-indentation is really needed when the code changes. The programmer can move a block of code by a simple copy-and-paste and continue solving the real problem. Re-indentation can always be done later and can be done automatically.

But in a language that uses layout syntax, re-indentation is mandatory, and worse, it can only be done manually. Layout syntax completely disables any editor’s auto-indent function. One may think that we might be able to invent a smarter editor that can auto-indent code for those languages. This is simply impossible. This is evident in the analysis of the above example. The two programs differ only in indentation, but they have completely different meanings. Both are grammatically correct programs and the editor has no way to tell which is the one you want unless it can read your mind.

Some people say that because those languages have advanced semantics, programs are so short that we don’t need to re-indent code very often. But experiences prove to me that the need for changing and rewriting code can never be eliminated. Writing code is like writing a book, you can always find pieces that need change or even complete rewrite. Usually changes in the following category will cause re-indentation:

  • Scope changes. There are lots of examples in this category: lifting an internal function to top level or push a top-level function into an internal function, surrounding a block with let-bindings, loops, conditional statements, try-except or lifting a block out of them, factoring out duplicated patterns, lifting “invariant code” out of recursion, … to name a few. These will necessarily change the indentation of a block of code, and each line needs to be re-indented.
  • Align code. For example in Haskell, when we align the arrows (->) of a case expression or the equal signs (=) of a function definition, we will notice that we have to re-indent most of the right-hand-sides, because they often contain multi-line expressions but the editors (for example, Emacs’ align-regexp function) only move the lines that contains the arrows or equal signs.
  • Renaming. We seldom choose the best names on the first shot, and good names make programs self-explanatory, so renaming is a very important and commonplace action. But in the following simple Haskell program, if we change the name from “helloworld” to “hello” and don’t re-indent the rest of the lines, we will get a parse error.
    helloworld z = let x = 1
                       y = 2 in
                     x+y+z

    Because the code becomes the following after the renaming, and the second line will no longer be aligned to “x = …”, and that confuses the parser.

    hello z = let x = 1
                       y = 2 in
                     x+y+z

    A similar thing happens when we lengthen the name to something like “helloworldcup”. Try it yourself. From this example, I hope you see how simple things are made frustratingly complicated by layout syntax. If you haven’t been convinced, try adding more lines to the above let expression.

The interruption from re-indenting code is usually not just one or two seconds, but often tens of seconds, even minutes. The programmer has to put down real problems at hand and turn to the mind-dead re-indenting job. This disrupts the “flow”, which is essential for producing creative and elegant code.

Syntax considered harmful

I believe that syntax, although an important aspect of natural languages, should not play a significant role in programming languages. It has already brought us too much trouble and frustration and wasted too much of our energy. You can read my other blog post detailing the harm of syntax in general and why we should remove the concept of “syntax” as a whole from programming languages.

Syntax has prevented lots of new design possibilities in programming languages. You may have heard language designers say: “Hey this is a nice feature, but the syntax of my language hasn’t any room left for it.” Layout syntax pushes to this direction even more. It forces us to consciously and constantly think about syntax, drawing our attention away from semantics design. It poses certain constraints on how code must be formatted, and makes a language even less extensible. Thus I think layout syntax is the most troublesome type of syntax.