2014 ICFP Contest Writeup, Part 2
Part 1 is here. My mostly-contemporaneous writeup left off abruptly after talking about general ideas and before getting into specifics about what I actually did (and didn’t do). So this part is based on months-old memories and some cryptic notes-to-self that I’m sure made sense to me while I was writing them.
Level 3b
Continuations: we like them. The CPS transform is a simple matter of programming, but doing it without introducing lots of unnecessary continuations (or reducing them away afterwards) requires more thinking. (In hindsight, I wonder if I could have taken more of a Lambda: the Ultimate Label approach with them, but I don’t think I thought of that — which is kind of strange, because that used to be one of my favorite “secret weapons” of CS theory.) But the larger theme was, given complete control of the language, trying to see whether qualities normally extracted by analysis/inference could be made explicit.
So, if returning from a function should mirror calling a function, then it should bind some names. This led to the idea of a function body being a sequence of binders — either let/letrec or a call, or maybe eventually some kind of task yield — plus conditional branching, and terminating in a return or tail call. Meanwhile, the trees of primitive operator applications could remain as they were.
And thus from the seeds of CPS, that ultimate flower of the functional world, arose an expression/statement distinction, the original sin of procedurality, considered harmful since Landin’s ISWIM. (Or something like that.) Oops.
In fact, it turned out to be kind of a pain to actually use — especially compared to the earlier Scheme-like language, where I could just write expression trees and not have to think about whether they were statement-ish. And it got worse: I had a preprocessing pass to expand some derived forms into a simpler core language, which is a useful tool in general, but I was still thinking in Scheme terms and (not entirely consciously) trying to force this statement language into that mold, and that didn’t go so well.
Level 3a
Types: I want them, but I’m scared of them. More specifically, scared of trying to implement something like type inference so I don’t have code that’s more annotations than actual code, but also scared of what might happen without some way of statically ensuring that the code won’t break.
Hindsights
Hindsight the first: ML-style inference would have been less work than what I wound up with, and could probably have expressed everything I actually needed to. (Unfortunately, I didn’t realize how much work I was getting into until too late; see below re alligators.)
Hindsight the second: the Forth leitmotif of factoring a program into pieces small enough to be obviously correct would probably have worked okay here. (Beta-reduction and concatenation aren’t that different, really.)
Hindsight the third: I probably didn’t have enough time to try to implement the entire game mechanics… but I could have implemented the core SECD machine for unit testing.
From JavaScript to Java (sort of)
But I was also trying to answer more questions about the program than whether it confuses an integer with a cons cell or whatever; specifically, I wanted to do some kind of time-usage analysis. Also, I was going to have mutable state encapsulated in closures, which is how object-oriented programming is typically [encoded in lambda calculus][sicp-oop]… so why not cut out the intermediate layer?
Which would also give me a nice answer to the analysis question: instead of dealing with function invocations that could go anywhere and would need some extravagant analysis like [kCFA][], I’d have calls to specific methods in specific classes (even though the constancy of the control transfer target would be lost in translation to the SECD machine). Meanwhile there was another train of thought, about “tagged lambdas” and matching tags on funcalls, which collided with the OO ideas.
The essential difference between a named class and an unnamed lambda, it seemed to me, was basically the same as between an ML tuple and a C struct: [structural vs. nominal][structnom]. Thus: nominal function types. Which probably need their own post, but the basic idea is that each lambda expression is annotated with the name of the type it inhabits. Multiple functions can inhabit the same type; this is basically subclassing (or sum types / variants / enums, in other languages). The type system must ensure that each call site for a type is passing values acceptable to all inhabitants of the callee type. An analysis thus gets information about which functions a call site can reach, and the programmer has a relatively straightforward way to adjust the granularity of this information.
Concretely: the type checker maintained a map from names to [lower and upper bounds][subtyping] on the argument and return type lists, narrowing them from the appropriate side when encountering functions and call sites, and raising an error if the bounds crossed (i.e., if the lower bound was no longer a subtype of the upper bound). In principle it seemed very elegant, with pleasing symmetries among the dimensions of subtyping and argument/return and definition/call.
PROTIP: Subtyping is a swamp full of alligators. And the alligators do not like you. I spent the better part of a day getting confused about which way was up in the type lattice and mixing up meet/join and so on; this was not helped by my messing up extending the subtype relation to lists of types (to make variable arity and ignoring excess values work), and probably other embarrassing mistakes I can’t bring myself to look at the commit history for. And the worst part is: I’m pretty sure I didn’t actually need subtyping, and that everything I was doing could’ve been done (and possibly done better!) with type variables and unification. I’ll call this one a “learning experience”.
Timing
I made an attempt at using the nominal function types to do a worst-case running time analysis; even though there wasn’t runtime support to do anything interesting with it in the actual program, it could still be useful as a programming aid, to guarantee that I wouldn’t run over bounds.
Unfortunately, I didn’t have any code really worth timing like that (say, an incremental breadth-first search). I also got bogged down in a detail I could maybe have just avoided instead: trying to handle loops/recursion by declaring (or in concrete syntax declareing; cf. Common Lisp) a maximum depth and having the time checker use it instead of just bailing out. I then went off into the weeds of handling this generally, for arbitrary mutual recursion (there’s some subtlety in defining “maximum recursion depth”) and trying not to combinatorially explode into exploring every possible interleaving of stack frames, by making the checker return essentially a system of linear inequalities that was sort of approximately solved. This eventually more or less worked, but it wasn’t really useful enough or even elegant enough to justify the work.
And it all could have been avoided if I’d just gone ahead and implemented a generator/yield construct and made everything incremental. No loops means no caring how many times the loop runs, as previously discussed. Possible answers to the problem of dynamic cycle-counting overhead:
-
If the cycle counter can replace a loop counter or depth limit or similar, then it can basically pay for itself.
-
Iterating over
conslists of known maximum length can be special-cased, or just statically unrolled. -
Just deal with it; there’s already an extra cycle per call from using CPS, to allocate the continuation closure, so an extra few per loop iteration isn’t that bad. And I could even quantify the proportion of time lost to this overhead, because I’d know how much time the actual code takes — if I’d had code to measure. (Yes, that would need best-case instead of worst-case for branching. This is not a hard problem.)
This also makes me wonder what could be done with the language design, given a constraint that recursion has to go through some special construct — see also Forth and early binding — but this didn’t actually occur to me during the contest.
Conclusions?
I guess there should be a section here with some kind of closing thoughts. I’ll grudgingly admit that it would have been nice to have had a better actual submission, and/or to have a better ratio of ideas to implemented ideas. I don’t know how much of my PL ideation fun-time I’d have wanted to give up for that, though. I did tend to wind up trying to avoid getting bogged down in tedious implementation of something well-understood and then, as a result, getting bogged down in tedious implementation of something not so well-understood — and I’m not sure that’s actually a win.
And it seems to me that, beyond a certain point, the cause of improving a language design is best served by climbing down from the land of meta-abstraction and trying to actually use it — even for “toy” languages like these — and that certain point tended to go flying past without my noticing it.
Even so, it was nice to have an excuse to take a break from thinking about my day job and wander off into the land of programming language design for a bit.