Lambda the Ultimate

This is just a series of blog posts so far, as far as I can tell. But Andrej Bauer's work has been mentioned here many times, I am finding these posts extremely interesting, and I'm sure I will not be alone. So without further ado...

Programming With Effects. Andrej Bauer and Matija Pretnar.

I just returned from Paris where I was visiting the INRIA πr² team. It was a great visit, everyone was very hospitable, the food was great, and the weather was nice. I spoke at their seminar where I presented a new programming language eff which is based on the idea that computational effects are algebras. The language has been designed and implemented jointly by Matija Pretnar and myself. Eff is far from being finished, but I think it is ready to be shown to the world. What follows is an extended transcript of the talk I gave in Paris. It is divided into two posts. The present one reviews the basic theory of algebras for a signature and how they are related to computational effects. The impatient readers can skip ahead to the second part, which is about the programming language.

This notice comes a little late, but the latest version of OCaml, version 3.12, has been released. Surprisingly, for a point release there's a lot of interesting new language features:

Some of the highlights in release 3.12 are:

• Polymorphic recursion is supported, using explicit type declarations on the recursively-defined identifiers.
• First-class modules: module expressions can be embedded as values of the core language, then manipulated like any other first-class value, then projected back to the module level.
• New operator to modify a signature a posteriori: S with type t := tau denotes signature S where the t type component is removed and substituted by the type tau elsewhere.
• New notations for record expressions and record patterns: { lbl } as shorthand for { lbl = lbl }, and { ...; _ } marks record patterns where some labels were intentionally omitted.
• Local open let open ... in ... now supported by popular demand.
• Type variables can be bound as type parameters to functions; such types are treated like abstract types within the function body, and like type variables (possibly generalized) outside.
• The module type of construct enables to recover the module type of a given module.
• Explicit method override using the method! keyword, with associated warnings and errors.

I'm especially intrigued by first-class modules, and the destructive signature operations, both of which should make it much easier to write libraries.

Intel Concurrent Collections...provides a mechanism for constructing [programs] that will execute in parallel while allowing the application developer to ignore issues of parallelism such as low-level threading constructs or the scheduling and distribution of computations. The model allows the programmer to specify high-level computational steps including inputs and outputs without imposing unnecessary ordering on their execution... Data is either local to a computational step or it is explicitly produced and consumed by them. An application in this programming model supports multiple styles of parallelism (e.g., data, task, pipeline parallel). While the interface between the computational steps and the runtime system remains unchanged, a wide range of runtime systems may target different architectures (e.g., shared memory, distributed) or support different scheduling methodologies (e.g., static or dynamic).

In short CnC purports to be a "a graph-based data-flow-esque deterministic parallel programming model". An open-source Haskell edition of the software was recently released on Hackage.

A series of blog posts describe the implementation: #1, #2, #3, #4, #5 (the last post links to a draft paper).

Personally, I would have preferred a more concise and down to earth description on the whole thing. If you have experiences to share, please do.

Milawa: A Self-Verifying Theorem Prover for an ACL2-Like Logic

Milawa is a "self-verifying" theorem prover for an ACL2-like logic.

We begin with a simple proof checker, call it A, which is short enough to verify by the "social process" of mathematics.

We then develop a series of increasingly powerful proof checkers, call them B, C, D, and so on. We show that each of these is sound: they accept only the same formulas as A. We use A to verify B, and B to verify C, and so on. Then, since we trust A, and A says B is sound, we can trust B, and so on for C, D, and the rest.

Our final proof checker is really a theorem prover; it can carry out a goal-directed proof search using assumptions, calculation, rewrite rules, and so on. We use this theorem prover to discover the proofs of soundness for B, C, and so on, and to emit these proofs in a format that A can check. Hence, "self verifying."

This might help inform discussions of the relationship between the de Bruijn criterion (the "social process" of mathematics) and formal verification. I think it also serves as an interesting signpost on the road forward: it's one thing to say that starting with a de Bruijn core and evolving a more powerful prover is possible in principle; it's another thing for it to actually have been done. The author's thesis defense slides provide a nice, quick overview.

Functional Pearl: Species and Functors and Types, Oh My! Brent Yorgey, draft.

We've discussed species many times before, and discussed at least one introduction for functional programmers. Here's another, this time considerably less technical. I would say this paper succeeds fairly well in giving a conceptual overview and some useful intuition. If you found the Carette and Uszkay paper sketchy in places, you may find this a gentler introduction.

On the other hand, I don't really see how it counts as a Functional Pearl...

While I like the general idea, it seems this project didn't go far enough.

What I think would be cool is to develop are DSLs that compile to g-code. For example, putting my hacker hat on, I think it might be fun to build a DSL for describing mechanical (analog) computers, this will compile into g-code for cams, shafts, gears etc. that could then be manufactured using CNC machines and/or 3D printers...

The Monad Zipper by Bruno Oliveira and Tom Schrijvers

Limitations of monad stacks get in the way of developing highly
modular programs with effects. This pearl demonstrates that Functional
Programming’s abstraction tools are up to the challenge. Of
course, abstraction must be followed by clever instantiation: Huet’s
zipper for the monad stack makes components jump through unanticipated
hoops.

The monad zipper gives us new ways to compose monadic code operating with different transformer stacks. To put it another way, it extends our ability to compose systems using different ranges of effects.

Conal Elliott's weblog post from January, Can functional programming be liberated from the von Neumann paradigm?, makes the case that the kind of coupling to state which Haskell programs making use of the IO monad have, raise problems of the same sort that led to pure functional programming in the first place. Conal then goes on to sketch, with reference to his work on FRP and denotational design, some ideas about where purity should be leading language design.

Objects to Unify Type Classes and GADTs, by Bruno C. d. S. Oliveira and Martin Sulzmann:

We propose an Haskell-like language with the goal of unifying type classes and generalized algebraic datatypes (GADTs) into a single class construct. We treat classes as first-class types and we use objects (instead of type class instances and data constructors) to define the values of those classes. We recover the ability to define functions by pattern matching by using sealed classes. The resulting language is simple and intuitive and it can be used to define, with similar convenience, the same programs that we would define in Haskell. Furthermore, unlike Haskell, dictionaries (or
objects) can be explicitly (as well as implicitly) passed to functions and we can program in a simple object-oriented style directly.

A very interesting paper on generalizing and unifying type classes and GADTs. Classes are now first-class values, resulting in a language that resembles a traditional, albeit more elegant, object-oriented language, and which supports a form of first-class "lightweight modules".

The language supports the traditional use of implicit type class dispatch, but also supports explicit dispatch, unlike Haskell. The authors suggest this could eliminate much of the duplication in the Haskell standard library of functions that take a type class or an explicit function, eg. insert/insertBy and sort/sortBy, although some syntactic sugar is needed to make this more concise.

Classes are open to extension by default, although a class can also be explicitly specified as "sealed", in which case extension is forbidden and you can pattern match on the cases. Furthermore, GADTs can now also carry methods, thus introducing dispatch to algebraic types. This fusion does not itself solve the expression problem, though it does ease the burden through the first-class support of both types of extension. You can see the Scala influences here.

I found this paper via the Haskell sub-reddit, which also links to a set of slides. The authors acknowledge Scala as an influence, and as future work, suggest extensions like type families and to support more module-like features, such as nesting and opaque types.

A Lambda Calculus for Real Analysis

Abstract Stone Duality is a revolutionary paradigm for general topology that describes computable continuous functions directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis.

This language is applied to the Intermediate Value Theorem: the solution of equations for continuous functions on the real line. As is well known from both numerical and constructive considerations, the equation cannot be solved if the function "hovers" near 0, whilst tangential solutions will never be found.

In ASD, both of these failures and the general method of finding solutions of the equation when they exist are explained by the new concept of overtness. The zeroes are captured, not as a set, but by higher-type modal operators. Unlike the Brouwer degree, these are defined and (Scott) continuous across singularities of a parametric equation.

Expressing topology in terms of continuous functions rather than sets of points leads to treatments of open and closed concepts that are very closely lattice- (or de Morgan-) dual, without the double negations that are found in intuitionistic approaches. In this, the dual of compactness is overtness. Whereas meets and joins in locale theory are asymmetrically finite and infinite, they have overt and compact indices in ASD.

Overtness replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive analysis and recursive enumerability in recursion theory.

Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated Jean-Yves Girard's regrettably out-of-print Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX.