We got a paper submitted to PLDI—Programming Language Design and Implementation—if just. The acceptance rate of late has been around 20% it seems. I think the paper was good, but I have no idea of it was that good. Since PLDI has a double-blind refereeing system, I’ll try not to give too many specifics in this post: specific enough that I can talk about things, but vague enough that a referee won’t inadvertently stumble here from Google.

I’m fairly sure that this language marks the direction my research should be going in during my Ph.D. It has the possibility of being a very nice language. Of course I’ll wait to see what the referees say. It may be unlikely, but there’s always the chance of a “this research is a dead-end because of [reason you’ve never thought of]” which is why it’s nice to get feedback from fresh eyes.

There are issue for the front-end. I think this is the biggest fault of the language as it stands right now. Considering what the language is intended to do—give automatic guarantees on polynomial time complexity—a lot of the complexity is justifiable, but still it can be improved. The typing system is a bore to get around. After becoming familiar with the language for a few weeks or so one starts to get a bit of intuition about how to structure things to “beat” the typing system. Still, it would be nice to add a bit more in the way of inference so the typing system can help you out. The syntax is perhaps more cumbersome, in the sense that there are too many constructs, than is totally necessary.

Changes to the front-end wouldn’t be purely cosmetic, either. The way we have the language right now is nice since everything that’s in there serves a purpose and everything is proved to work correctly. In a language such as this, removing something or changing something is a very delicate matter and it’s easy to destroy the guarantee mentioned above of guaranteeing time complexity. But work and cleverness aside, I’m sure it can be done.

On the back end of things, there aren’t problems so much as there are opportunities. As it stands, the implementation—which needs a lot of work yet—is just a very naïve interpreter. Making a compiler for a language such as this brings up myriad issues which one wouldn’t find in any other language. Memory management is the big one. Garbage collection is likely not necessary at all, so it will be interesting to see exactly what nice—and efficient—memory management schemes it would offer.


I apologize for not posting more often to this blog. It is, of course, the usual excuse—I always find more important things to do. In fact I’m still terribly busy, but I thought I was overdue.

I got back from working with Robin Cockett and Brian Redmond in Calgary. They’re working on a new programming language which uses type theory to enforce that each well-typed program halts in polynomial time. It’s been done before, but nowhere near as nicely as this. The implementation is just a proof-of-concept, nowhere near fit for consumption of a general computer science audience. It was this fact that it’s built on a terribly recondite foundation mixed with discussions over the minutiæ of the syntax got me thinking more about the face of a programming language, the dreaded “front end.”

Syntax in the programming languages world has, to a large extent, been considered a solved problem for the past couple decades, and for good reason. The technology behind parsing has, so far as I’m concerned, been solved. There have been enough languages created, and segregated into successes and failures, that people have a general idea of what a decent programming language should look like. Yet the process is still not formalized. When creating a new language, people—or myself at least—look at existing successful languages, fudge them to fit whatever new characteristics their language will contain, and use common sense to reason it out.

I think I’ve stated on here before my fondness for literate programming. I think code should be primarily documentation and, further, that that documentation should look gorgeous and be easy to read. As I was mulling over programming language syntaxes, I hit an epiphany when I realized that the primary goal in the syntax of a language should be how readable it is when typeset. As we move towards higher-level languages and rely on smarter compilers to do what we want to do, the purpose of a language is no longer to describe exactly which bits gets pushed where, but rather to, in the most elegant way possible, describe the essence of the solution to the problem.

I like the off-side rule—the “significant whitespace” present in Python and Haskell—for exactly this reason. When displaying code that’s meant to be read, it’s imperative that the code be indented nicely anyway. Why not have the language enforce that the program’s structure be identical to how it’s presented?

This got me thinking about syntax highlighting. Highlighting is nearly as important to indentation when understanding the structure of code, in my view. Further, when typesetting literate code, that code should properly be highlighted in the typeset document. So why not make highlighting part of the language? One could distinguish between the highlighted keyword let and the variable name let. It poses some practical problems, namely that you potentially have to abandon straight ASCII as an input format in favour of annotated ASCII such as LaTeX or Rich Text.

The other thing I started thinking about is syntax in the context of information theory. This got in my head as we were discussing the role of keywords such as of in the new language. Should the syntax dictate that you write case x of … or should it leave out the entirely unnecessary keyword of there?

In the interest of maintainable code, there’s value in redundancy. As two extremes: one can write 50 characters of C++ code and, due to the noisiness of C++’s template syntax, relay only 50 bits of actual information; however, 50 characters of Lisp code might relay 200 bits of information. In this case I like Lisp’s syntax better than C++’s, but there’s a huge danger in having a syntax which is too concise: one parenthesis in the wrong spot and the semantics of your program can be completely different from what you intended. And that difference might not be obvious to the reader.

I had this conversation years ago with someone about the operator—used both in programming and English—”not.” Note that whenever someone feels they must get across the point that they are not something, they will emphasize—using italics or boldface or uppercase letters or anything at their disposal—the word “not” and often only the word “not.” Programmers typically don’t have such luxury, and an errant ! symbol can sometimes get lost in the mix. Yet it is one of the most powerful constructs in computer science: that you want to do exactly the opposite of what you’re going to describe next. From the point-of-view of information theory, A and not A are syntactically almost identical.

So that is a clear example of where it would be nice for the language to enforce some redundancy. Don’t just throw a ! in there, but redundantly make other changes to the code that make it clear that something’s going on.

The obvious question is: so how would a language do that? An even better question is: how can a language require redundant information without being complete torture to write in? I’ve no idea, but it would be nice if someone would look at it formally, ha!

I’m so pleased with my progress on the Ca compiler, I’ve decided to provide an ad hoc link to it in its current state. I’m not confident enough to give proper instructions for it though, as it is for hardcore haxx0rz only.

I’ve made the switch from make to ant for the build system. There are a number of things which are bizarre about ant. For instance, failonerror should default to true in every case. Perhaps there are some cases where silent failure can be acceptable, which can be made explicit in those cases with a failonerror="false", but in a build system, I have a hard time believing that an error should, by default, be considered a success. Also there is no convenient built-in way to copy a file while retaining permissions.

Aside from that, I like the ant model of things. Java is not such a horrible way to describe how to build something.

As for the compiler itself, there are a number of bug fixes still in the queue, such that it still can’t be used for useful work. For useless work, however, it is quite fabulous, if I say so myself.

Even more exciting is I’ve run into a theoretical problem which is proving very difficult to prove. Research is one of the few vocations where your very metric of “success” is the number of problems you create. I’m off for a camping trip over the next few days which will give me some time to mull it over.

Next month I’ll be taking a trip back to my alma mater. I’ve been invited by my undergraduate supervisor to help him and his post-doctoral student on a new project he’s starting up. It’s a programming language based on co-inductive types where each program is guaranteed to halt in polynomial time. My job is to come up with, ideally, some clever ways of implementing it efficiently. I don’t know many more details than that, but it sounds like a dream project for me.

I apologize for the long delays between posts. Rest assured no news is good news, and it’s just business as usual.

One bit of exciting news, though, is that I’ve received an email from my old supervisor, Robin Cockett, at the University of Calgary. He has a project for a pretty cool sounding programming language based on Martin Hofmann’s work—where programs are restricted to polynomial time—and needs someone to worry about the implementation details. I’m pretty excited about the prospects.

Also I’ve decided to turn my idle attention to my Zipit, borrowed from my friend Albert. It’s kind of a fun little thing, if annoying to type on, but sports a 60MHz ARMv4 chip in it. I’m toying with the idea of having my compiler target not just C, but also ARM. I’ve got an ARM cross-assembler installed, so it’s just a matter of working out the networking details.

ARM is a surprisingly beautiful ISA. Everyone knows it for its pervasive use of conditional instructions, of course, but its addressing modes are quite nice as well. My only other exposure to pre- and post-index addressing was with the PDP-11, but ARM does it in a much cleaner way.

Last week, my co-supervisor gave me the Steam Boiler Problem. It’s a classical problem for specifications languages. You have a computer monitoring a steam boiler: a giant tank of water with a heat source and a steam pipe at the top. There are water pumps to control—to add more water into the tank—and a series of sensors. Essentially, given complex specifications, you have to get the steam boiler into a functioning state and keep it that way. Sensors can start malfunctioning, too, to make it more difficult.

It’s a good problem because it forced me to look at how Ca is to work with in the flesh, in a complex example. Even though I’m not done, the conclusion is that it needs a lot of syntactic sugar built on top of it.

Some of them are rather superficial, if time-consuming. For example, currently patterns cannot overlap at all in Ca, so something like:

l {
  Cons 5 xs -> ...;
  Cons x xs -> ...;
  _ -> ...;

Is not allowed, though it really should be. I had no idea before now how irritating it is not having that feature. There are other minor syntax features like that that need to be addressed.

The more interesting case is what to do with the catamorphisms. Theoretically they work fine, almost. In practice, they’re a bit cumbersome. When I said “almost” before, I meant they worked fine up to Loïc Colson’s famous inférieur (“minimum”) problem. It pertains to primitive recursive schemes like the one I’m working with, were writing the “minimum function”—finding the minimum of two values—has greater time complexity than in an unrestricted computational model.

What this boils down to in my mind is the inability to perform a catamorphism over two objects simultaneously. Or stated in a more Haskell-ish way, there’s no efficient way to write the zip function.

One solution floating in my mind is to make the catamorphism construct explicitly allow zipping. It’s not too bad adding it in. The syntax would be something like so:

(l, n) {
  (Cons x xs, p+1) -> ...;
  (Nil, 0) -> ...;

Where l is a list and n is a natural number.

Another possible solution, which I quite like, is the idea of making catamorphisms parametric. So you could do something like so:

{ i ->
  Cons x xs -> i * x + @xs x;
  Nil -> i - 2;
} l 0;

The variable i is a parameter over the catamorphism, initially 0. I like this is as it makes a lot of things more natural and doesn’t add any computational power. The syntax for the catamorphism has to change, but I think this is for the best anyway.

I’ve been thinking about the compiler again and how best to implement higher-order functions, once time comes to do that. Currently the compiler uses a lambda lifter. I.e., there are no closures. Every function is lifted out of any scope to the top-level, collecting extra parameters along the way. This is fine for first-order programs, since you can change every call to a nested function into a call with extra arguments. However, in first order programs, this causes problems because the arities have to match. For instance:

f x = let g y = x + y; in
  g (x + 4);

Gets transformed into:

f_g x y = x + y;
f x = f_g x (x + 4);

Every function is now at the global level and g has all the variables it needs. This causes problems with higher-order functions though:

f x zs = let addX y = x + y; in
  map addX zs;

Naïvely this is:

f_addX x y = x + y;
f x zs = map (f_addX x) zs;

Ahh, but the first argument to map is a closure, not a function! We should properly implement closures as lambda lifted functions, so we can’t very well implement lambda lifted functions are closures! There are myriad other problems with this approach, but suffice it to say it won’t work.

Anyway, I was contemplating abandoning lambda lifting entirely and just leaving closures implemented as closures in C. The GNU C Compiler has a little-known and little-used, sadly, feature usually called nested functions. They’re half-closures in a way. They’re closures up until their lexical scope disappears. Well, such is the C way. But they would do what I needed.

I was reading the original 1988 Usenix paper which describes the technique, usually called “trampolining,” to implement nested functions quite smartly in C. As I was reading, I discovered that the author had originally intended to implement unnamed functions in C!

He gives two suggestions for syntax. I like the first one he suggests, which looks something like (int (*)(int x) { return x + 2; }). For instance, you could do something like (int (*)(int x) { return x + 2; })(3), which would evaluate to 5. Perhaps not the most useful example, but you get the idea.

These unnamed functions are really no more of a bother to implement than named functions, once you allow nested functions, but it appears this feature was never implemented in GCC! I suppose to get good use out of them you’d need a less bulky syntax. Type inference could help there.

Anyway, the point of this post was to register my dismay at GCC never implementing unnamed functions, despite there being no technical reason for not doing so. They can be quite handy, those unnamed functions.

For what it’s worth, I think I’ve decided against relying on GCC’s trampolining to do higher-order functions and lambda abstractions in Ca. It is very clever and very efficient, but the semantics are a bit hairy for the 21st century. For example, I just looked at some SPARC assembler that GCC produced for it, and it involves a system call to make to the stack executable. In today’s security conscious kernels, executing the stack, as trampolining necessarily requires, is less practical than it once was. Maybe one day we can get rid of these blunt MMUs, but that’s a rant for another time. In any case, MMU concerns aside, executing the stack mucks with the instruction cache on architectures with separate caches. As I said, hairy semantics.

In Breuel’s paper, he sets up other simpler solutions for implementing closures as being impractical due to their changing calling conventions. Well, I’m making my own language and I can make my own calling conventions. I expect that higher-order functions will simply be passed as two pointers instead of one. It saves everyone a lot of headaches.

The functional programming language community seems to be moderately abuzz over the recent release of the Disciplined Disciple Compiler. The first announcement I saw for it I ignored almost completely. Dialect of Haskell, allows destructive updates, allows mixing lazy and strict, etc. None of that really grabbed me.

Then this afternoon I saw another blog mentioned it on the Planet Haskell feed. This time it was mentioned with the phrase “region, effect, and closure inference” and immediately I had to read more about it.

The compiler seems to be a Google summer of code project by an Australian Ph.D. student. There is no paper yet! This means trying to figure out what’s going on involves combing through all the wiki pages and reading some tea leaves. Regions—à la Tofte—are not used for memory allocation. Darn! They seem to be used as part of the effect system, e.g., to mark certain regions of memory as being pure/constant/read-only or allowing destructive updates.

All of the magic is in the type system. It looks very well thought-out and very rich and is all orthogonal to the usual Haskell type system.

It looks like an interesting language to follow. I shall be keeping track of its developments.

From a syntactic stand-point, it seems to further my belief that you need to choose a “side” on the strict versus lazy issue. Disciple should in theory nicely and transparently mix strictly evaluated expressions with lazily evaluated ones. In practice this means things are strict by default but can be made lazy with annotations.

In my mind, what defines a language as being “strict” or “lazy” is the standard library. A language which truly is agnostic on the issue should allow, for example, map to be used in either a strict or lazy manner rather than having both a strict map and a lazy map. I don’t see an easy way to get this, so for the time being it seems languages have to pick sides.

In a similar vein, one of the nice features of Disciple is that its effect system ends the duality in Haskell between pure and impure functions. For instance, in Haskell you have a map which works on pure functions and a mapM which works on monadic functions. No such division exists in Disciple.