Martin Escardo and Paulo Oliva have been working on the selection monad and related functionals. The selection monad `S(X) = (X -> R) -> X` is a cousin of the continuation monad `C(X) = (X -> R) -> R` and it has a lot of useful and surprising applications. I recommend their recent paper “What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common” which they wrote for MSFP 2010 (if you visit the workshop you get to hear Martin live). They explain things via examples written in Haskell, starting off with the innocently looking functional `ox` (which i I am writting as
ox in Haskell for “crossed O”):
ox :: [(x -> r) -> x] -> ([x] -> r) -> [x]
ox  p = 
ox (e : es) p = a : ox es (p . (a:))
where a = e (\x -> p (x : ox es (p . (x:))))
It is just four lines of code, so how complicated could it be? Well, read the paper to find out. If you are ready for serious math, have a look at this paper instead.
Already a while ago videolectures.net published this tutorial on Computer Verified Exact Analysis by Bas Spitters and Russell O’Connor from Computability and Complexity in Analysis 2009. I forgot to advertise it, so I am doing this now. It is about an implementation of exact real arithmetic whose correctness has been verified in Coq. Russell also gave a quick tutorial on Coq.
These are the slides and the extended abstract from my MSFP 2008 talk. Apparently, I forgot to publish them online. There is a discussion on the Agda mailing list to which the talk is somewhat relevant, so I am publishing now.
Abstract: Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions as types, because it allows the realizers to use computational effects such as non-termination, store and exceptions. Therefore, we can use realizability as a framework for program development and extraction which allows any style of programming, not just the purely functional one that is supported by the Curry-Howard correspondence. In joint work with Christopher A. Stone we developed RZ, a tool which uses realizability to translate specifications written in constructive logic into interface code annotated with logical assertions. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools. In our experience, RZ is useful for specification of non-trivial theories. While the use of computational effects does improve efficiency it also makes it difficult to reason about programs and prove their correctness. We demonstrate this fact by considering non-purely functional realizers for a Brouwerian continuity principle.
Download: msfp2008-slides.pdf, msfp2008-abstract.pdf
I have been writing lecture notes on computable mathematics. One of the questions that came up was whether it is possible to simulate the booleans in the simply-typed $\lambda$-calculus. This is a nice puzzle in functional programming. If you solve it, definitely let me know, although I suspect logicians did it a long time ago. Continue reading How to simulate booleans in simply typed lambda calculus?
I show how monads in Haskell can be used to structure infinite search algorithms, and indeed get them for free. This is a follow-up to my blog post Seemingly impossible functional programs. In the two papers Infinite sets that admit fast exhaustive search (LICS07) and Exhaustible sets in higher-type computation (LMCS08), I discussed what kinds of infinite sets admit exhaustive search in finite time, and how to systematically build such sets. Here I build them using monads, which makes the algorithms more transparent (and economic). Continue reading A Haskell monad for infinite search in finite time