" /> Ezra's Research: September 2008 Archives

« August 2008 | Main | October 2008 »

September 12, 2008

Formlets; Idioms, arrows and monads

[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

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.

September 9, 2008

motor sounds

Overheard on #haskell:

newsham: > let motor sounds = sounds "vroom! " in motor cycle

lambdabot: "vroom! vroom! vroom! vroom! vroom! vroom! vroom! vroom! vroom! vroom! vroo...

September 4, 2008

Der Hauptsatz

Had a good time today puzzling over Gerhard Gentzen's 1934 paper, "Untersuchungen über das logische Schließen. I." ("Investigations into logical reasoning"). I wanted to determine that this was really what I thought it was: the paper where he introduced cut-elimination and the subformula property, which I'm examining now in my research.

I was looking at the German version and I don't know anything about German. But Google Translate and the BeoLingus online DE-EN dictionary came to the rescue. (Phil tells me he has a translation, but where's the fun in that?)

The result was satisfying:

Eine nähere Untersuchung der besonderen Eigenschaften des natürlich Kalküls fürte mich schließlich zu einem sehr allgemeinen Satz, den ich im folgenden "Hauptsatz" nennen will. Der Hauptsatz besagt, dass sich jeder rein logische Beweis auf eine bestimmte, übrigens keineswegs eindeutige, Normalform bringen lässt.

which I render,

A closer examination of the special properties of the natural calculus led me to a general theorem that I have called the `fundamental theorem'. The fundamental theorem says that any purely logical proof can be brought to a certain (incidentally, non-obvious) normal form.

And much later, after introducing the natural deduction calculi for classical (NK) and intuitionistic logic (NJ), as well as the respective sequent calculi (LJ and LK), we get to this understated result:

Hauptsatz: Jede LJ- bzw. LK-Herleitung läßt sich in eine LJ- bzw. LK-Herleitung mit der gleichen Endsequenz umwandeln, in welcher die als Schnitt bezeichnete Schlußfigur nicht vorkommt.

Every LJ- (resp. LK-)derivation can convert to a LJ- (resp., LK-)derivation with the same end sequent, in which the rule called ``snip'' does not appear.

Instead of the usual name "cut," I've merrily translated the German "Schnitt" as "snip," because it pleases me--I like direct, etymological, native translations of this kind. (OED traces the English "snip" to Low German "schnipp," not terribly far off; "cut" has, of course, OE origin.)

(Sadly, I can't remember where I got the PDF of this original. The browsable online version linked above is from Gentzen's own alma mater, Göttingen University.)

(Miscellanea: Fans of typographic history will appreciate the printer's use of letter spacing for emphasis, a practice unknown in English but apparently traditional in German, according to Wikipedia. It could be used roughly wherever we use italics in English.)

September 1, 2008

Discovery! \qedhere

Just made an exciting discovery! The TeX command \qedhere can be used within an AMS proof environment; it forces the proof-tombstone to go on the present line, whereas it would normally go after the end of the \begin{proof}/\end{proof} block, which often puts it outside an itemize or enumerate environment, looking ugly on a line of its own. Of course, the command properly suppresses the tombstone at the end of the proof environment. Ah comfort, O infinite luxury of macros!