Episode 21

Faith Evolution and Programming Languages, from Haskell to Java
Philip Wadler

Faith and evolution provide complementary--and sometimes conflicting--models of the world, and they also can model the adoption of programming languages. Adherents of competing paradigms, such as functional and object-oriented programming, often appear motivated by faith. Families of related languages, such as C, C++, Java, and C#, may arise from pressures of evolution. As designers of languages, adoption rates provide us with scientific data, but the belief that elegant designs are better is a matter of faith. This talk traces one concept, second-order quantification, from its inception in the symbolic logic of Frege through to the generic features introduced in Java 5, touching on aspects of faith and evolution. The remarkable correspondence between natural deduction and functional programming informed the design of type classes in Haskell. Generics in Java evolved directly from Haskell type classes, and are designed to support evolution from legacy code to generic code. Links, a successor to Haskell aimed at AJAX-style three-tier web applications, aims to reconcile some of the conflict between dynamic and static approaches to typing.

Parametricity (Types are Documentation)
Tony Morris

Philip Wadler tells us, Write down the definition of a polymorphic function on a piece of paper. Tell me its type, but be careful not to let me see the function's definition. I will tell you a theorem that the function satisfies.

Danielsson, Hughes, Jansson & Gibbons tell us, Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.

What does this mean and how might it be applied?

Parametric Execution Models
Daniel Spiewak

Among the small boatload of challenges facing developers of asynchronous software is that of testability. It is very difficult to practically write concurrent algorithms which are then unit- and integration-tested in a repeatable fashion without relying on unreliable mechanisms like timeouts. Furthermore, such systems are often very difficult to refactor in any significant fashion, due to the rigid hard-coding of the asynchronous mode of execution. As one might expect, this is not merely a problem faced in concurrency, but rather an issue whenever an execution order or effect must be propagated through a series of computations while simultaneously remaining open to variant implementations.

This talk will explore the use of generic effects to abstract over the execution model of functions and even entire modules, allowing external constraints to drive the fundamental shape of the computation itself. We will pay particularly close attention to some of the benefits these techniques can provide in the realm of testability and the ability to reason about our requirements at the type level.