I’ve just updated my web page with links to some new papers that are now available:
- “Homotopical Patch Theory” by Carlo Angiuli, Ed Morehouse, Dan Licata, and Robert Harper. To appear, ICFP, Gothenburg, October 2014. We’ve also prepared a slightly expanded version with a new appendix containing material that didn’t make the cut for ICFP. (Why do we still have such ridiculously rigid and limited space limitations? And why do we have such restricted pre-publication deadlines as we go through the charade of there being a “printing” of the proceedings? One soon day CS will step into its own bright new future.). The point of the paper is to show how to apply basic methods of homotopy theory to various equational theories of patches for various sorts of data. One may see it as an application of functorial semantics in HoTT, in which theories are “implemented” by interpretation into a universe of sets. The patch laws are necessarily respected by any such interpretation, since they are just cells of higher dimension and functors must behave functorially at all dimensions.
- “Cache Efficient Functional Algorithms” by Guy E. Blelloch and Robert Harper. To appear, Comm. ACM Research Highlight this fall. Rewritten version of POPL 2013 paper for a broad CS audience. Part of a larger effort to promote integration of combinatorial theory with logical and semantic theory, two theory communities that, in the U.S. at least, ignore each other completely. (Well, to be plain about it, it seems to me that the ignoring goes more in one direction than the other.) Cost semantics is one bridge between the two schools of thought, abandoning the age-old “reason about the compiled code” model used in algorithm analysis. Here we show that one can reason about spatial locality at the abstract level, without having to drop-down to low-level of how data structures are represented and allocated in memory.
- “Refining Objects” by Robert Harper and Rowan Davies. To appear, Luca Cardelli 60th Birthday Celebration, Cambridge, October, 2014. A paper I’ve meant to write sometime over the last 15 years, and finally saw the right opportunity, with Luca’s symposium coming up and Rowan Davies visiting Carnegie Mellon this past spring. Plus it was a nice project to get me started working again after I was so rudely interrupted this past fall and winter. Provides a different take on typing for dynamic dispatch that avoids the ad hoc methods introduced for oop, and instead deploying standard structural and behavioral typing techniques to do more with less. This paper is a first cut to prove the concept, but it is clear that much more can be said here, all within the framework of standard proof-theoric and realizability-theoretic interpretations of types. It would help to have read the relevant parts of PFPL, particularly the under-development second edition, which provides a lot of the background that we necessarily elide in this paper.
- “Correctness of Compiling Polymorphism to Dynamic Typing” by Nick Benton, Kuen-Bang Hou (Favonia), and Robert Harper, draft (summer 2014). Classically polymorphic type assignment starts with untyped -terms and assigns types to them as descriptions of their behavior. Viewed as a compilation strategy for a polymorphic language, type assignment is rather crude in that every expression is compiled in uni-typed form, complete with the overhead of run-time classification and class checking. A more subtle strategy is to maintain as much structural typing as possible, resorting to the use of dynamic typing (recursive types, naturally) only for variable types. The catch is that polymorphic instantiation requires computation to resolve the incompatibility between, say, a bare natural number, which you want to compute with, and its encoding as a value of the one true dynamic type, which you never want but are stuck with in dynamic languages. In this paper we work out an efficient compilation scheme that maximizes statically available information, and makes use of dynamic typing only insofar as the program demands we do so. There are better ways to compile polymorphism, but the dynamic style is forced by badly designed virtual machines, such as the JVM, so it is worth studying the correctness properties of the translation. We do so by making use of a combination of structural and behavioral typing, that is using types and refinements.
I hope to comment here more fully on these papers in the near future, but I also have a number of other essays queued up to go out as soon as I can find the time to write them. Meanwhile, other deadlines loom large.
[Update: added fourth item neglected in first draft. Revise formatting. Add links to people. Brief summary of patch theory paper.]