[jwarden]

One case where a function is often not substitutable for an array is equality testing. In a language where any two arrays with the same elements in the same order are equal ([1,2] == [1,2]), the same cannot always be true of two equivalent functions. That is because extensionally equality is undecidable for arbitrary functions.

Arrays and functions may be mathematically equivalent but on a programming language level they are practically different.

[cionx]

I don’t understand this argument. Just because functional extensionality is undecidable for arbitrary functions doesn’t mean that it is undecidable for every class of functions.

In the specific situation, let’s say that by an array we mean a finite, ordered list whose entries are indexed by the numbers 0, 1, …, n - 1 for some natural number n. Let’s also say that two arrays are equal if they have the same length and the same value at each position (in other words, they have “the same elements in the same order”).

If we now want to represent a function f as an array arr such that f(i) = arr[i] for every possible input i of f, then this will only be possible for some very specific functions: those whose domain are the set {0, 1, …, n - 1} for some natural number n. But for any two such functions f, g : {0, 1, …, n - 1} → t, their extensional equality is logically equivalent to the equality of the corresponding arrays: you really can check that f and g are extensionally equal by checking that they are represented by equal arrays.

[jwarden]

Right, so for a subset of functions, a language could implement an extensional equality test operator `==` for two functions by calling the functions for every possible input. It would be prohibitively slow for some functions, but correct.

But for other functions, even that won't be possible.

The point is that functions and arrays may be practically different. You can always do an `==` test on the contents of two arrays, but you can't do the same for two arbitrary functions.