When Is A Functional Program Not A Functional Program?, John Longley. ICFP 1999.

In an impure functional language, there are programs whose behavior is completely functional (in that they behave extensionally on inputs) but the functions they compute cannot be written in the purely functional fragment of the language. That is, the class of programs with functional behavior is more expressive than the usual class of pure functional programs. In this paper we introduce this extended class of "functional" programs by means of examples in Standard ML, and explore what they might have to offer to programmers and language implementors.

After reviewing some theoretical background, we present some examples of functions of the above kind, and discuss how they may be implemented. We then consider two possible programming applications for these functions: the implementation of a search algorithm, and an algorithm for exact real-number integration. We discuss the advantages and limitations of this style of programming relative to other approaches. We also consider the increased scope for compiler optimizations that these functions would offer.

I like this paper because it shows how some of the most abstract bits of formal logic (realizability models of higher order logic) suggest actual programs you can write.

As a barely-related aside, even a brief look into this realizability stuff also taught me a good deal of humility -- for example, it seems that at higher types, what you can represent mathematically depends on the specific notion of computation you're using. So the mathematical consequences of the Church-Turing thesis are rather more subtle than we might initially expect. (Andrej Bauer discusses a related point in more detail in this blog post.)

## Recent comments

1 week 6 days ago

1 week 6 days ago

3 weeks 2 min ago

3 weeks 14 hours ago

3 weeks 19 hours ago

3 weeks 19 hours ago

3 weeks 19 hours ago

3 weeks 6 days ago

4 weeks 1 hour ago

4 weeks 5 hours ago