Recent papers

Philip Wadler

Propositions as Sessions

Philip Wadler. Journal of Functional Programming, Best Papers of ICFP 2012. (See also: conference version.)

Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994), and by Caires and Pfenning (2010), among others, this paper presents CP, a calculus in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), by Honda, Kubo, and Vasconcelos (1998), and by Gay and Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and presents a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yield a language free from deadlock, where deadlock freedom follows from the correspondence to linear logic.

Available in: pdf, doi.


Propositions as Types

Philip Wadler. Draft, March 2014.

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.

Available in: pdf.


Blame, coercions, and threesomes, precisely

Jeremy Siek, Peter Thiemann, and Philip Wadler. Draft, March 2014.

We systematically present four calculi for gradual typing: the blame calculus of Wadler and Findler (2009); a novel calculus that pinpoints blame precisely; the coercion calculus of Henglein (1994); and the threesome calculus of Siek and Wadler (2010). Threesomes are given a syntax that directly exposes their origin as coercions in normal form, a more transparent presentation than that found in Siek and Wadler (2010) or Garcia (2013).

Available in: pdf


Topics in Lambda Calculus and Life

Philip Wadler. International Summer School on Trends in Computing, Tarragona, 22–26 July 2013.

Three two-hour talks cover a range of topics:


A practical theory of language-integrated query

James Cheney, Sam Lindley, Philip Wadler. ICFP 2013.

Language-integrated query is receiving renewed attention, in part because of its support through Microsoft's LINQ framework. We present a theory of language-integrated query based on quotation and normalisation of quoted terms. Our technique supports abstraction over values and predicates, composition of queries, dynamic generation of queries, and queries with nested intermediate data. Higher-order features prove useful even for constructing first-order queries. We prove that normalisation always succeeds in translating any query of flat relation type to SQL. We present experimental results confirming our technique works, even in situations where Microsoft's LINQ framework either fails to produce an SQL query or, in one case, produces an avalanche of SQL queries.

Earlier versions of this paper were named "The essence of language-integrated query"

Available in: pdf, doi, supplementary materials and code, FP Days slides, SCRIPT workshop slides.


Topics in Lambda Calculus and Life

Philip Wadler. Midlands Graduate School, Leicester, 8–12 April 2013.

Five talks covering a range of topics:


You and Your Research and The Elements of Style

Philip Wadler. Talk, Programming Languages Mentoring Workshop, POPL, 22 January 2013.

Advice from Hamming, Strunk and White, Knuth, and others on how to best conduct and communicate your research.

Available in: slides, blog.


Propositions as Sessions

Philip Wadler. International Conference on Functional Programming (ICFP), Copenhagen, September 2012.

Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994), and by Caires and Pfenning (2010), among others, this paper presents CP, a calculus in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), by Honda, Kubo, and Vasconcelos (1998), and by Gay and Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and presents a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yield a language free from deadlock, where deadlock freedom follows from the correspondence to linear logic.

Available in: pdf, doi.


Church's Coincidences

Philip Wadler. Turing Centennial Celebration, Princeton, 10–12 May 2012 and keynote SICSA PhD Conference, Glasgow, 20–22 June 2012.

The foundations of computing lay in a coincidence: Church's lambda calculus (1933), Herbrand and Godel's recursive functions (1934), and Turing's machines (1935) all define the same model of computation. Another coincidence: Gentzen's intuitionistic natural deduction (1935) and Church's simply-typed lambda calculus (1940) define isomorphic systems. We review the history and significance of these coincidences, with an eye to Turing's role.

Available in: pdf, video.


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.

Available in: doi, pdf, redex model.

ACM DL Author-ize serviceBlame for all
Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, Philip Wadler
POPL '11, 2011


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.

Available in: doi. pdf,


Threesomes, With and Without Blame

Jeremy G. Siek and Philip Wadler, Symposium on Principles of Programming Languages (POPL), Madrid, January 2010.
(See also: STOP version).

How to integrate static and dynamic types? Recent work focuses on casts to mediate between the two. However, adding casts may degrade tail calls into a non-tail calls, increasing space consumption from constant to linear in the depth of calls.

We present a new solution to this old problem, based on the notion of a threesome. A cast is specified by a source and a target type---a twosome. Any twosome factors into a downcast from the source to an intermediate type, followed by an upcast from the intermediate to the target---a threesome. Any chain of threesomes collapses to a single threesome, calculated by taking the greatest lower bound of the intermediate types. We augment this solution with blame labels to map any failure of a threesome back to the offending twosome in the source program.

Herman, Tomb, and Flanagan (2007) solve the space problem by representing casts with the coercion calculus of Henglein (1994). While they provide a theoretical limit on the space overhead, there remains the practical question of how best to implement coercion reduction. The threesomes presented in this paper provide a streamlined data structure and algorithm for representing and normalizing coercions. Furthermore, threesomes provide a typed-based explanation of coercion reduction.

Available in: doi, pdf.


Monadic constraint programming

Tom Schrijvers, Peter Stuckey, and Philip Wadler Journal of Functional Programming 19(6):663—697, 2009.

A constraint programming system combines two essential components: a constraint solver and a search engine. The constraint solver reasons about satisfiability of conjunctions of constraints, and the search engine controls the search for solutions by iteratively exploring a disjunctive search tree defined by the constraint program. In this paper we give a monadic definition of constraint programming in which the solver is defined as a monad threaded through the monadic search tree. We are then able to define search and search strategies as first-class objects that can themselves be built or extended by composable search transformers. Search transformers give a powerful and unifying approach to viewing search in constraint programming, and the resulting constraint programming system is first class and extremely flexible.

Available in: pdf, doi.


The RPC Calculus

Ezra Cooper and Philip Wadler. Principles and Practice of Declarative Programming (PPDP), Coimbra, 2009.

Several recent language designs have offered a unified language for programming a distributed system, with explicit notation of locations; we call these "location-aware" languages. These languages provide constructs allowing the programmer to control the location (the choice of host, for example) where a piece of code should run, which can be useful for security or performance reasons. On the other hand, a central mantra of WWW system engineering prescribes that web servers should be "stateless": that no "session state" should be maintained on behalf of individual clients—that is, no state that pertains to the particular point of the interaction at which a client program resides. Many implementations of locationaware languages are not at home on the web: they hold some kind of client-specific state on the server. We show how to implement a symmetrical location-aware language on top of a stateless server.

Available in: pdf.
Slides from PPDP 09: pdf.


Blame for all

Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler Workshop on Script to Program Evolution (STOP), Genova, 2009.

We present a language that integrates statically and dynamically typed components, similar to the gradual types of Siek and Taha (2006), and extend it to incorporate parametric polymorphism. Our system permits a dynamically typed value to be cast to a polymorphic type, with the type enforced by dynamic sealing along the lines proposed by Pierce and Sumii (2000), Matthews and Ahmed (2008), and Neis, Dreyer, and Rossberg (2009), in a way that ensures all terms satisfy relational parametricity. Our system includes a notion of blame, which allows us to show that when more-typed and less-typed portions of a program interact, that any type failures are due to the less-typed portion.

Available in: doi, pdf.
Slides from STOP 2009: pdf. Technical report: pdf.


Threesomes, With and Without Blame

Jeremy G. Siek and Philip Wadler. Workshop on Script to Program Evolution (STOP), Genova, 2009.

The blame calculus of Wadler and Findler gives a high-level semantics to casts in higher-order languages. The coercion calculus of Henglein, on the other hand, provides an instruction set for casts whose normal forms ensure space efficiency. In this paper we address two questions: 1) can space efficiency be obtained in a high-level semantics? and 2) can we precisely characterize the relationship between the high and low-level semantics of casts? Towards answering both of these questions, we design a cast calculus that summarizes a sequence of casts as a threesome cast that contains a source type, a target type, and a third middle type that is the greatest lower bound of all the types in the sequence. We show that the threesome calculus is equivalent to the blame calculus and to one of the coercion-based, blame-tracking calculi of Siek, Garcia, and Taha. We also show that the threesome calculus is space efficient and obtain a tighter bound than that of Herman, Tomb, and Flanagan.


Available in: doi, pdf.

The RPC Calculus

Ezra Cooper and Philip Wadler. Principles and Practice of Declarative Programming (PPDP), Coimbra, 2009.

Several recent language designs have offered a unified language for programming a distributed system, with explicit notation of locations; we call these "location-aware" languages. These languages provide constructs allowing the programmer to control the location (the choice of host, for example) where a piece of code should run, which can be useful for security or performance reasons. On the other hand, a central mantra of WWW system engineering prescribes that web servers should be "stateless": that no "session state" should be maintained on behalf of individual clients—that is, no state that pertains to the particular point of the interaction at which a client program resides. Many implementations of locationaware languages are not at home on the web: they hold some kind of client-specific state on the server. We show how to implement a symmetrical location-aware language on top of a stateless server.

Available in: pdf.
Slides from PPDP 09: pdf.


Well-typed programs can't be blamed

Philip Wadler and Robert Bruce Findler. ESOP 2009. (See also: Scheme workshop version, ICFP submission.)

We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtyping, and show that these recombine to yield naive subtyping. Naive typing has previously appeared in type systems that are unsound, but we believe this is the first time naive subtyping has played a role in establishing type soundness.

Available in: pdf.
Slides from AOSD 2008: pdf.


The Essence of Form Abstraction

Ezra Cooper, Sam Lindley, Philip Wadler, Jeremy Yallop. APLAS 2008.

Abstraction is the cornerstone of high-level programming; HTML forms are the principal medium of web interaction. However, most web programming environments do not support abstraction of form components, leading to a lack of compositionality. Using a semantics based on idioms, we show how to support compositional form construction and give a convenient syntax.

Available in: pdf.


Idioms are oblivious, arrows are meticulous, monads are promiscuous

Sam Lindley, Philip Wadler, Jeremy Yallop. MSFP 2008.

We revisit the connection between three notions of computation: Moggi's monads, Hughes's arrows and McBride and Paterson's idioms (also called applicative functors). We show that idioms are equivalent to arrows that satisfy the type isomorphism A ~> B = 1 ~> (A -> B) and that monads are equivalent to arrows that satisfy the type isomorphism A ~> B = A -> (1 ~> B). Further, idioms embed into arrows and arrows embed into monads.

Available in: pdf.


Philip Wadler,