What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common

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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

relatively accessible

relatively accessible introduction to this work.

I would stress the word "relatively". This is not as clearly written as the material deserves.

A gentler start might be

A gentler start might be with the following two blog posts:
Seemingly Impossible Functional Programs, and A Haskell Monad for Infinite Search in Finite Time.

Thanks, these are nicer. I

Thanks, these are nicer. I still think there is room for a better introduction. I guess I am a bit spoiled.

Nicer to come?

Since they say on their download page:

We would have liked to include more material and more remarks of an expository nature, and more references to other people's related work, but we had a hard limit of 12 pages.

we can hope that they will write an expanded and clarified edition in the near future.

Indeed. My comments are

Indeed. My comments are meant to urge them to do so soon.

Variations on a theme

Great paper! I've written a further note inspired by theirs, also as a literate Haskell program. My code improves on theirs in a few ways, notably by using type classes to characterize valuation types, and by using QuickCheck to describe and check relevant properties.

A course in the making?

I've written a further note inspired by theirs, also as a literate Haskell program.

Really nice!

I can't help but feel that this could be used as the basis for a course called "Foundations of Mathematics through Computation".

I encourage anyone who wanted a clearer exposition of the ideas in the OP to check this "note" out.

It is not really analogous to the OP

Wadler just briefly mentions the Tychonoff Theorem and does not actually address it.

It would be more appropriate to say that this is a cleaner Haskell solution.

Very minor problem

In the "Partial order" section of your literate Haskell program, you have this definition:

> dominates :: Sup r => r -> r -> Bool

But where you show that it's lazy in its second argument you have the wrong return value:

*Main> Win `dominates` undefined

(That should be 'True' rather than 'Win'.)