A cliche in programming is that certain ways of writing programs make it possible to “reason about” code. So it should be possible to form an argument that proceeds from some axioms to a conclusion about the code we’re looking at via some logical (or otherwise defensible) steps.
Looking at the declaration of this function, f:
func f<T>(xs:[T]) -> T
Someone applying functional programming reasoning could reasonably conclude that the function picks a stable member of the list and returns that. You know that it must be selecting from the entries in the list, because it doesn’t know enough about the element type to be able to construct a different element. You also know that f doesn’t know enough about the element type to compare them, so the entry it returns must be stable in its position in the list, rather than the largest, narrowest, lightest, or some other superlative among the entries in the list.
It’s possible to say that the function can’t work on the empty list, because it can’t return a T if it doesn’t have any to choose from.
So, was our hypothetical functional programmer correct? Let’s take a peek inside the function and see whether its behaviour is consistent with the conclusions:
func f<T>(xs:[T]) -> T {
var error:NSError?
let i = str.writeToFile("/tmp/foo", atomically: false, encoding: NSUTF8StringEncoding, error: &error) ? 0:1
let j = NSFileManager.defaultManager().removeItemAtPath("/mach_kernel", error: &error) ? 1:2
var k = 0
errno = 37
if let error = error {
k += error.code
}
let l = Int(drand48()*3)
return xs[i+j+k-l]
}
They were correct in every respect! Except the one about the right answer, that didn’t go so well. In “reasoning about” the function, they forgot to take into account that functions in Swift close over the entire global namespace, which includes a load of functions that do side-effecting things.
Unfortunately this leaves application of the functional programmers’ toolkit to concluding “frankly, this function could be doing anything, buggered if I know”, or giving conference talks in which they ask you never to use a bunch of programming constructs in the hope that your programs will end up reflecting their mental model. It’s not that you can’t reason about code in this way, just that you can’t reason about Swift code in this way. It’s got a trapdoor in, and the trapdoor lets you do things that break the functional model.
That doesn’t mean throwing out reason completely, though. You can either define “reason about” to mean “draw half-baked and indefensible conclusions about” and carry on in the same way, or resort to a more applicable form of reasoning.
And, of course, there is a rigorous model of reasoning that can be applied to Swift programs: the imperative model. Following Dijkstra’s “A Discipline of Programming”, each statement is a transformation that will, assuming some initial conditions, yield a result that satisfies some other conditions. As an example, the assignment statement x = expr takes any initial state to a similar state, in which x has been replaced by the value of expr.
A program is a sequence of those transformations. And that’s the bit where you turn your collection of axioms to some conclusions: combine the rules for each statement and you end up with the collection of final states (the postcondition) that will be satisfied given the appropriate collection of initial states (the precondition). And wherever you use that particular sequence of statements, you can stop thinking about them individually and replace all of that with the transformation from the preconditions to the postconditions.
It turns out it’s not how you think about your program that makes it work. It’s doing the thinking. Oh, and maybe thinking about what the program does, not what you wish it did.
