Lambda the Ultimate

What Sequential Games, the Tychonoff Theorem, and the Double-Negation Shift have in Common, Martin Escardo and Paulo Oliva, to appear in MSFP 2010.

This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functional programming language Haskell, which

1. optimally plays sequential games,
2. implements a computational version of the Tychonoff Theorem from topology, and
3. realizes the Double-Negation Shift from logic and proof theory.

The functional makes sense for finite and infinite (lazy) lists, and in the binary case it amounts to an operation that is available in any (strong) monad.

In fact, once we define this monad in Haskell, it turns out that this amazingly versatile functional is already available in Haskell, in the standard prelude, called sequence, which iterates this binary operation. Therefore Haskell proves that this functional is even more versatile than anticipated, as the function sequence was introduced for other purposes by the language designers, in particular the iteration of a list of monadic effects (but effects are not what we discuss here).

One of the most durable and productive analogies in semantics is the analogy between computability and continuity. Depending on how you read the history, this idea might even predate computers: Brouwer proved that all intuitonistic functions on the reals were continuous.

Over the last few years, Escardo and his collaborators have done a lot of cool stuff showing how this network of ideas can be turned into miraculous-looking little programs, so it's very nice to see a relatively accesible introduction to this work.

The PEPM Symposium/Workshop series aims to bring together researchers and practitioners working in the areas of program manipulation, partial evaluation, and program generation. PEPM focuses on techniques, theories, tools, and applications of analysis and manipulation of programs.

The 2011 PEPM workshop will be based on a broad interpretation of semantics-based program manipulation in a continued effort to expand the scope of PEPM significantly beyond the traditionally covered areas of partial evaluation and specialization and include practical applications of program transformations such as refactoring tools, and practical implementation techniques such as rule-based transformation systems. In addition, it covers manipulation and transformations of program and system representations such as structural and semantic models that occur in the context of model-driven development. In order to reach out to practitioners, there is a separate category of tool demonstration papers.

Topics of interest for PEPM'11 include, but are not limited to:

• Program and model manipulation techniques such as transformations driven by rules, patterns, or analyses, partial evaluation, specialization, program inversion, program composition, slicing, symbolic execution, refactoring, aspect weaving, decompilation, and obfuscation.
• Program analysis techniques that are used to drive program/model manipulation such as abstract interpretation, static analysis, binding-time analysis, dynamic analysis, constraint solving, type systems, automated testing and test case generation.
• Analysis and transformation for programs/models with advanced features such as objects, generics, ownership types, aspects, reflection, XML type systems, component frameworks, and middleware.
• Techniques that treat programs/models as data objects including meta-programming, generative programming, deep embedded domain-specific languages, program synthesis by sketching and inductive programming, staged computation, and model-driven program generation and transformation.
• Application of the above techniques including experimental studies, engineering needed for scalability, and benchmarking. Examples of application domains include legacy program understanding and transformation, DSL implementations, visual languages and end-user programming, scientific computing, middleware frameworks and infrastructure needed for distributed and web-based applications, resource-limited computation, and security.

We especially encourage papers that break new ground including descriptions of how program/model manipulation tools can be integrated into realistic software development processes, descriptions of robust tools capable of effectively handling realistic applications, and new areas of application such as rapidly evolving systems, distributed and web-based programming including middleware manipulation, model-driven development, and on-the-fly program adaptation driven by run-time or statistical analysis.

Full details are available on the official site.

Type Classes as Objects and Implicits

Type classes were originally developed in Haskell as a disciplined alternative to ad-hoc polymorphism. Type classes have been shown to provide a type-safe solution to important challenges in software engineering and programming languages such as, for example, retroactive extension of programs. They are also recognized as a good mechanism for concept-based generic programming and, more recently, have evolved into a mechanism for type-level computation. This paper presents a lightweight approach to type classes in object-oriented (OO) languages with generics using the CONCEPT pattern and implicits (a type-directed implicit parameter passing mechanism).

This paper also shows how Scala’s type system conspires with implicits to enable, and even surpass, many common extensions of the Haskell type class system, making Scala ideally suited for generic programming in the large.

Martin Odersky and team's design decisions around how to do type classes in a unified OO and FP language continue to bear fascinating fruit. Implicits look less and less like "poor man's type classes," and more and more like an improvement upon type classes, in my opinion given a quick read of this paper.