How to formulate and prove the statement "all functions are continuous" in an effectful functional language?

README.md

Are all functions continuous?

Mathematical background

Brouwer's statement "all functions are continuous" can be formulated without reference to topology as follows.

Definition: A functional f : (N → N) → N is continuous at a : N → N when there exists m : N such that, for all b : N → N, if ∀ k < m, a k = b k then f a = f b.

This says that the value of f a depends only on the initial segment a 0, a 1, ..., a (m-1).

The statement all functionals are continuous everywhere is valid in various models of intuitionistic mathematics, such as Kleene's number realizability and Kleene's function realizability. We can ask whether the statement is realized in any given functional programming language.

Definition: A modulus of continuity is a functional μ : ((N → N) → N) → (N → N) → N such that, for all f : (N → N) → N and a, b : N → N, if ∀ k < μ f a . a k = b k then f a = f b.

Essentially μ f a computes how much of a is needed to compute f a.

Implementing the modulus of continuity

It is impossible to implement μ in PCF and therefore also in Haskell. We necessarily need additional abilities that let μ inspect the workings of f. Here are a few attempts.

Pretend that int is the type of natural numbers

type nat = int

ML with references

Consider ML with references (and no other features). Then a possible μ:

let mu_ref f a =
  let k = ref 0 in
  let a' n = (k := max !k n; a n) in
    f a' ; !k

However:

1. We should at least require that f be hereditarily total (it terminates on total a).
2. Can f use its own local references? If yes, then we can break mu_ref. If no, is that not too restrictive?
3. How do we formulate the exact preconditions on f and a?
4. What is the theorem that needs to be proved, and how is it proved?

ML with exceptions

With exceptions (and no other features) we can do it as follows:

exception Abort

let mu_exc f x =
  let rec search k =
    try
      let y n = (if n < k then x n else raise Abort) in
        f y ; k
    with Abort -> search (k+1)
  in
    search 0

However:

1. What if f catches Abort? May it do so? What is the contract on f?
2. Would local exceptions help? If so, can f use its own local exceptions?

Other setups

1. In Haskell we could do everything inside a fixed monad. This is still not entirely easy, even if we figure out what it means for f to be "pure" (whatever that means).

2. Moving to a total language is probably helpful. However, keep in mind that μ does not exist in pure λ-calculus, so straight Agda or some such is out of the question.

3. Other effects can be used to implement a candidate μ, but it seems like they should be local (local references, local exceptions, delimited control) or else f has access to them.

A note on rigor

The proofs should be actual proofs, not hand-wavy arguments.

continuity.ml

type nat = int
let mu_ref f a =
  let k = ref 0 in
  let a' n = (k := max !k n; a n) in
    f a' ; !k

exception Abort
let mu_exc f x =
  let rec search k =
    try
      let y n = (if n < k then x n else raise Abort) in
        f y ; k
    with Abort -> search (k+1)
  in
    search 0