Ezra's Research

[UPDATE: The broken link to "The Essence of Form Abstraction" has been fixed. Sorry!]

For the first time in three years of research, I'm really proud of a paper that I worked on with my research group: The Essence of Form Abstraction, by Ezra Cooper, Sam Lindley, Philip Wadler and Jeremy Yallop, to be published in APLAS 2008. The paper shows how you can create compositional HTML forms which package up their data in any desired type. It shows an OCaml implementation but we also use the idea in our web-centric language, Links.

Though this is the first good group work that I've contributed to, the others have been doing some great work. In particular, Jeremy, Sam, and Phil did some nice work characterizing the expressive power of idioms, arrows, and monads. They first defined a metalanguage, like Moggi's monadic metalanguage, which can encompass all three notions, in The Arrow Calculus, by Sam Lindley, Philip Wadler and Jeremy Yallop (unarchived). Then they showed the hierarchy of the three, under which idioms are the loosest interface but therefore their language is the strictest to program with, and monads are the strictest interface, therefore their language is the most free, and arrows can be seen as lying in between. The work is described in Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous (ibid.), MSFP 2008.

To summarize this, you can see the arrow calculus as a syntax like the do notation of Haskell:

do y <- f x
   z <- g y x
   return (h x y z)

Now to put the result crudely, monads allow expressions like the above, where the value bound at each step can be used in all future steps (this makes them "promiscuous"). The use of arrows restricts this so that the value bound at each step can be used only at the next step, as in:

do y <- f x
   z <- g y x
   return (j x z)  -- y cannot be used here

You can still use arrow operations to manually pass data forward through each step, but this is a nuisance. Hence Lindley, Wadler and Yallop coined the term "meticulous" to describe arrows.

The idiom laws restrict this further so that each value can be used only in a final return clause (the return clause is "oblivious"):

do y <- f x
   z <- k x        -- y cannot be used here
   return (h x y z)

An astute reader will note that return is not required in do syntax. What happens if there is no return clause? Then you can add one:

do y <- f x
   z <- k x
   q

is equivalent to

do y <- f x
   z <- k y x
   result <- q
   return result

But either way the idiom laws require that q cannot depend on y or z.

This shows that the three notions progressively restrict (and fairly naturally) the ways that you can program with them. But, in a familiar appearance of contravariance, the notions are reverse-ordered in how restrictive they are to create. An idiom, being the most restrictive on its user, is least restrictive to its writer. Thus you can model some computational notions as idioms which you could not model as monads. This fact came in handy in our latest paper, where we used idioms to model form abstraction.

I encourage you all to read about idioms, arrows and monads, as it's turning out to be a very nice theory.