Turner‚ Bird‚ Eratosthenes: The Eternal Burning Thread

Abstract

Functional programmers have many things for which to thank the late David Turner: design decisions he made in his languages SASL, KRC, and Miranda over the last 50 years are still influential and inspiring now.

One example program that he popularized as an illustration of lazy evaluation and list comprehensions in SASL is a one-line recursive "sieve" to generate the infinite list of prime numbers. Turner called this algorithm The Sieve of Eratosthenes. In a lovely paper called "The Genuine Sieve of Eratosthenes" (JFP, 2009), Melissa O'Neill argued that Turner's algorithm is not in fact a faithful implementation of the algorithm, and gave a detailed presentation using priority queues of the real thing. She included a variation by Richard Bird, which uses only lists but makes clever use of circular programming. Bird describes his circular program again in his textbook "Thinking Functionally with Haskell", and sets its proof of correctness as an exercise. Unfortunately, his hint for a solution is incorrect. So what should a proof look like?

One of the last projects Turner worked on was the notion of "Total Functional Programming". He observed that most programs are already structurally recursive or corecursive, therefore guaranteed respectively terminating or productive, and conjectured that "with more practice we will find this is always true". Compelling as this vision is, it seems that we are still some way off achieving it. We explore Bird's circular Sieve of Eratosthenes as a challenge problem for Turner's Total Functional Programming.