Monday, January 3, 2011

Papers, Proofs, PrimOps, Allocation and Strengthening

General status update: I got the reviews back for the paper I submitted to JFP on the DDC core language. The reviews were very helpful, and a huge thank you to the reviewers if you're reading this. I will endeavour to make all my own reviews as helpful.

The bottom line was the paper looked promising, but needs more motivation for the language design, and more meta-theory. The motivation is easy enough to 'port across from my thesis, so this part shouldn't take too long. For background, the JFP paper is an extension of the APLAS 2009 paper I wrote just after I finished my thesis. The original version of that paper had more motivational material, but I ended up cutting it to fit the page limit. For the JFP paper I tried to stick to the details of the core language, but I suppose not discussing the source language and wider context makes it hard to see the point of it all. There were also suggestions and questions as to the details of the language and typing rules, which I'll either fold in or explain why.

For the meta-theory, the paper needs proofs of observational equivalence for the example optimisations, showing how the witnesses are used during optimisation. I had a proof of soundness for the type system in the appendix, and worked examples of the optimisations, but not formal proofs that the optimisations are ok. Said optimisations are just standard ones like let floating and full-laziness, but I agree that if the point of having witnesses of purity and constancy in the core language is to perform optimisations in the presence of side-effects, then we want some formal link between the witnesses and those optimisations.

Anyway, I started on the proofs over the christmas break, and have the structure of one showing that let-floating is sound (changing the order of let-bindings with non-interferring effects), though I still need to fill in some details. I'm estimating about two or three weeks work (full time equivalent) to finish the proofs and update the paper.

I went to a hackathon hosted by Erik last week where we worked on LLVM support for DDC. Erik's written all the code for the backend, though to push it all the way through I needed to change how primops are handled in the rest of the compiler (which is explained in Erik's blog post). I just finished that this afternoon, so we're gunning for full LLVM support in the near future. The primop handling is pretty clean now, so if we wanted to, say, add support for vector operations like MMX and SSE then this should be reasonably straightforward.

Allocation Effects
The paper reviews have also convinced me that we want explicit allocation effects in the source and core languages. One of my thesis reviewers also suggested this, though so far I've left them out because they weren't absolutely needed. Allocation effects have a slightly different flavour to world effects (like writing to the Console) and to read/writing mutable data. When two expressions have world or read/write effects then this means they can interfere in such a way that you cannot change the order of these two expressions. In contrast, you can always change the order of expressions that just allocate new objects.

However, if an expression allocates new mutable objects, then you cannot hoist it out of a lambda (apply the full-laziness transform). Hoisting an expression means it is potentially executed less often, so we're not just changing the order of two actions in time. If you want to do hoisting without information about allocation, then it's sufficient to check that the binding to be hoisted performs no world or read/write effects, and does not return mutable data. However, using allocation effects will make this reasoning clearer, and can enable more optimisations later, so I'll add them in. I started on a branch that has them, but now I've convinced myself they're easy enough to add I'm going to leave the hacking to later and focus on getting the paper finished first.

In the type inferencer, it turns out that strengthening more-than constraints to equality constraints during inference breaks programs that use interesting higher order functions (like with parser combinators). This isn't a problem with standard 2nd order functions like map, fold, filter etc, but only appears with 3rd order functions and higher, or with data containing functions, which is why I hadn't noticed it before. By "break" I mean the inferencer returns a bad type, so we get a panic when we try to type check the corresponding core program. We still want to do the strengthening because it removes the need for a pile of redundant effect applications in the core programs, but it should be done while converting the desugared language to core, instead of during inference, which is fairly obvious in hindsight. I've started fixing this as well, but need to adjust the type utils (like type simplification and effect masking) so they'll handle the non-strengthened forms. Another job to be left until after the paper is finished...