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

# Category Archives: Guest post

# Exact real arithmetic in Haskell

*HERA* is an implementation of exact real arithmetic in Haskell using the approach by Andrej Bauer and Iztok Kavkler, see these and these slides. It uses the fast multiple precision floating point library MPFR. Download source, and see documentation and examples of usage at my home page.

[*Note by Andrej:* this is a guest post by AleÅ¡ Bizjak, a first-year student of mathematics at my department. I am very proud of the excellent work he did on his summer project.]

# Seemingly impossible functional programs

Andrej has invited me to write about certain surprising functional

programs.

The first program, due to Ulrich Berger (1990), performs exhaustive

search over the “Cantor space” of infinite sequences of binary

digits. I have included references at the end. A weak form of

exhaustive search amounts to checking whether or not a total predicate

holds for all elements of the Cantor space. Thus, this amounts to

universal quantification over the Cantor space. Can this possibly be

done algorithmically, in finite time?

Continue reading Seemingly impossible functional programs