Wadler's Blog

Blame for All, Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Symposium on Principles of Programming Languages (POPL), Austin, January 2011. (See also: STOP version).

Several programming languages are beginning to integrate static and dynamic typing, including Racket (formerly PLT Scheme), Perl 6, and C# 4.0, and the research languages Sage (Gronski, Knowles, Tomb, Freund, and Flanagan, 2006) and Thorn (Wrigstad, Eugster, Field, Nystrom, and Vitek, 2009). However, an important open question remains, which is how to add parametric polymorphism to languages that combine static and dynamic typing. We present a system that permits a value of dynamic type to be cast to a polymorphic type and vice versa, with relational parametricity enforced by a kind of dynamic selaing along the line proposed by Matthews and Ahmed (2008) and Neis, Dreyer, and Rossberg (2009). Our system includes a notion of blame, which allows us to show that when casting between a more-precise type and a less-precise type, any failure are due to the less-precisely-typed portion of the program. We also show that a cast from a subtype to its supertype cannot fail.

The arrow calculus, Sam Lindley, Philip Wadler, and Jeremy Yallop, Journal of Functional Programming 20(1):51-69, 2010.

We introduce the arrow calculus, a metalanguage for manipulating Hughes’s arrows with close relations both to Moggi’s metalanguage for monads and to Paterson’s arrow notation. Arrows are classically defined by extending lambda calculus with three constructs satisfying nine (somewhat idiosyncratic) laws; in contrast, the arrow calculus adds four constructs satisfying five laws (which fit two well-known patterns). The five laws were previously known to be sound; we show that they are also complete, and hence that the five laws may replace the nine.

And a fifth entry in the stakes to illustrate a list, or at least recursion. Thanks to Mitchell Wand, who found the original here.

• A list is an odd creature
• A list is an odd creature, take 2
• A list is an odd creature, take 3
• A list is an odd creature, take 4

A fourth entry in the stakes to illustrate a list. Thanks to Eugene who posted this item from Cyriak's collection (click here for the animated version):Previous entries:

• A list is an odd creature
• A list is an odd creature, take 2
• A list is an odd creature, take 3

Mandelbrot Maps was written by Iain Parris as an MSc project, and updated by Edward Mallia and Taige Liu. (Here's the original.) Jim Hanks used it to generate the cover for his latest album Dedication. That's a nice recognition of Ian, Edward, and Taige---well done, folks!

I mentioned to my first-year students that a list is an odd creature: it has only a head and a tail, where the tail is itself a creature with only a head and a tail, and so on. I challenged them to produce a picture, and Dan Benveniste came up with this:


I like the recursion, but it's not really a creature, is it? Further attempts encouraged! Previous entries:

• A list is an odd creature
• A list is an odd creature, take 2