August

I'm serving on the program committee of POPL 2014, and I've just been given 24 submissions to review.  Most are 12 pages long, a few are shorter, but that's still over 273 pages of (highly polished in some cases, highly technical in other cases) reading over the next six weeks.  I'm not complaining, mind you, but this is going to displace all of my "recreational" technical reading.

Accordingly, I'm taking a vacation from blog for the next few weeks; I may post the odd link or trite observation from time to time, though.

XQuery on SQL Hosts

XQuery on SQL Hosts
Torsten Grust, Sherif Sakr, and Jens Teubner
VLDB 2004

I've been interested in XML and XQuery for a long time, and this spring taught a course on Querying and Storing XML, which primarily addresses research topics over the last 10-15 years aimed at supporting database-style querying over XML data.  Although the wave of hype/industry enthusiasm for XML seems to have crested, many of the basic ideas live on in the various NoSQL, MapReduce or RDF-based (graph querying) systems that are now attracting more attention.

One of the most interesting (to me) lines of work on XML query processing has been based on "compiling" operations over XML down to relational operations for which efficient implementations are well-understood.  Previous work by DeHaan et al. (SIGMOD 2003), Grust et al. (TODS 2004), and others investigated an interval encoding approach to storing XML in a database, which has the nice feature that you can translate XPath expressions (even involving recursive steps) to SQL range queries, which existing relational databases can optimize well.

Read more »

Edit Lenses

Edit Lenses
M. Hofmann, B. Pierce, and D. Wagner
Proceedings of POPL 2012, p. 495-508.


I previously wrote about Diskin et al.'s delta lenses.  That paper explores one approach to bidirectional transformations that takes into account information about the update process changing one state to another.

In this paper, Pierce et al. explore what they call edit lenses.  A delta lens considers a state space as a category, with the arrows of the category being updates describing how to get from one state to another.  An edit lens, by contrast, considers a state space acted upon by a monoid (this idea appears in previous work on algebraic foundations of bidirectional transformations by Stevens, and was mentioned in Pierce et al.'s Symmetric Lenses paper as a natural next step). 

Read more »

Exploring the compiler forest in Haskell

The combinators from the Compiler Forest paper can be implemented in Haskell as follows.  (Note: This requires recent GHC with options -XKindSignatures -XGADTs -XTypeFamilies.)
First, we define a type for partial compilers:

data PC :: * -> * -> * where
  PC :: (s -> (s', t' -> t)) -> PC (s,t) (s', t')

In Haskell terms, this is a "generalized algebraic data type", but this is solely so that we can think of PC as a two-argument type constructor instead of four.
Read more »

The Compiler Forest

The Compiler Forest
M.Budiu, J. Galenson and G. D. Plotkin
ESOP 2013

This paper explores a notion of partial compilers, motivated by the problem of compiling high-level code (e.g. LINQ-style collection-based programs) on different architectures, such as multicore, GPU, or database backends.  If we think of a compiler as a simple function $C : source \to target$, then a partial compiler is a function $PC : source \to source' * (target' \to target)$.  Moreover, we can think of a "compilation problem" $C(source,target)$ as a pair of the source language and target language types.  Then a partial compiler $PC : C(source,target) \mathrel{-\!\!\circ} C(source',target')$ translates one "compilation problem" to another, hopefully simpler one: it takes a $source$ and produces a $source'$ together with a function $target' \to target$ that says how to finish compiling to $target$ once the $source'$ has been compiled to $target'$.

An ordinary compiler is then just a partial compiler that reduces the problem of compiling $source$ to $target$ to the "empty" problem $C(unit,unit)$, since $source \to unit * (unit \to target)$ is isomorphic to $source \to target$.
Read more »