Seemingly impossible constructive proofs

In the post Seemingly impossible functional programs, I wrote increasingly efficient Haskell programs to realize the mathematical statement

$\forall p : X \to 2. (\exists x:X.p(x)=0) \vee (\forall x:X.p(x)=1)$

for $X=2^\mathbb{N}$, the Cantor set of infinite binary sequences, where $2$ is the set of binary digits. Then in the post A Haskell monad for infinite search in finite time I looked at ways of systematically constructing such sets $X$ with corresponding Haskell realizers of the above omniscience principle.

In this post I give examples of infinite sets $X$ and corresponding constructive proofs of their omniscience that are intended to be valid in Bishop mathematics, and which I have formalized in Martin-Löf type theory in Agda notation. This rules out the example $X=2^\mathbb{N}$, as discussed below, but includes many interesting infinite examples. I also look at ways of constructing new omniscient sets from given ones. Such sets include, in particular, ordinals, for which we can find minimal witnesses if any witness exists.

Agda is a dependently typed functional programming language based on Martin-Löf type theory. By the Curry-Howard correspondence, Agda is also a language for formulating mathematical theorems (types) and writing down their proofs (programs). Agda acts as a thorough referee, only accepting correct theorems and proofs. Moreover, Agda can run your proofs. Here is a graph of the main Agda modules for this post, and here is a full graph with all modules.

The topology of the set of all types

It is well known that, both in constructive mathematics and in programming languages, types are secretly topological spaces and functions are secretly continuous. I have previously exploited this in the posts Seemingly impossible functional programs and A Haskell monad for infinite search in finite time, using the language Haskell. In languages based on Martin-Löf type theory such as Agda, there is a set of all types. This can be used to define functions $\mathbb{N} \to \mathrm{Set}$ that map numbers to types, functions $\mathrm{Set} \to \mathrm{Set}$ that map types to types, and so on.

Because $\mathrm{Set}$ itself is a type, a large type of small types, it must have a secret topology. What is it? There are a number of ways of approaching topology. The most popular one is via open sets. For some spaces, one can instead use convergent sequences, and this approach is more convenient in our situation. It turns out that the topology of the universe $\mathrm{Set}$ is indiscrete: every sequence of types converges to any type! I apply this to deduce that $\mathrm{Set}$ satisfies the conclusion of Rice’s Theorem: it has no non-trivial, extensional, decidable property.

To see how this works, check:

The Agda pages can be navigated be clicking at any (defined) symbol or word, in particular by clicking at the imported module names.

Running a classical proof with choice in Agda

As a preparation for my part of a joint tutorial Programs from proofs at MFPS 27 at the end of this month with Ulrich Berger, Monika Seisenberger, and Paulo Oliva, I’ve developed in Agda some things we’ve been doing together.

Using

for giving a proof term for classical countable choice, we prove the classical infinite pigeonhole principle in Agda: every infinite boolean sequence has a constant infinite subsequence, where the existential quantification is classical (double negated).

As a corollary, we get the finite pigeonhole principle, using Friedman’s trick to make the existential quantifiers intuitionistic.

This we can run, and it runs fast enough. The point is to illustrate in Agda how we can get witnesses from classical proofs that use countable choice. The finite pigeonhole principle has a simple constructive proof, of course, and hence this is really for illustration only.

The main Agda files are

These are Agda files converted to html so that you can navigate them by clicking at words to go to their definitions. A zip file with all Agda files is available. Not much more information is available here.

The three little modules that implement the Berardi-Bezem-Coquand, Berger-Oliva and Escardo-Oliva functionals disable the termination checker, but no other module does. The type of these functionals in Agda is the J-shift principle, which generalizes the double-negation shift.

How eff handles built-in effects

[UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.]

From some of the responses we have been getting it looks like people think that the io effect in eff is like unsafePerformIO in Haskell, namely that it causes an effect but pretends to be pure. This is not the case. Let me explain how eff handles built-in effects.

Programming with effects II: Introducing eff

[UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.]

This is a second post about the programming language eff. We covered the theory behind it in a previous post. Now we turn to the programming language itself.

Please bear in mind that eff is an academic experiment. It is not meant to take over the world. Yet. We just wanted to show that the theoretical ideas about the algebraic nature of computational effects can be put into practice. Eff has many superficial similarities with Haskell. This is no surprise because there is a precise connection between algebras and monads. The main advantage of eff over Haskell is supposed to be the ease with which computational effects can be combined.