Total functions in untyped languages
Does it even have meaning?
Watch the Clojure Documentary!
I was explaining an idea from my book to a coworker. I was saying that total functions can reduce defensive coding and simplify code. My coworker commented that it’s kind of meaningless to talk about totality in an untyped language.
I don’t agree, but I do understand the idea. It is much harder to define total function in an untyped language than in a typed language. When you’ve got types, you can say “A function is total if it returns a value (instead of throwing an error) for any arguments that pass the type checker.” It’s a straightforward definition. Or so it seems.
Totality is an idea from mathematics, specifically in the field of computability. A function is total if every combination of arguments in the domain of the function results in a value in its range. The domain and range are each sets of values. The domain specifies valid arguments while the range specifies valid return values.
And here we see a major problem: We’re using domain in two different ways. One is about the valid arguments to a function. The other is domain as in domain modeling, where it means the area of concern of your software. It’s tricky to talk about the first when in the context of the second.
Division is total in mathematics. Division’s domain is
ℝ x (ℝ - 0)
and the range is ℝ. That means division is defined for pairs of real numbers where the second element is not zero. That’s what we learned in high school algebra.
But in programming, division is the prime example of a partial function. How come? Well, when you define the function in a type language like this:
function divide(a: number, b: number): number
You get a function that can throw an exception—so it’s not total—even after it passes the type checker:
divide(1, 0) //=> Exception! Divide by zero.
What we see is that we’ve mapped the “set of values” idea of domain from math onto the “types of arguments” idea in programming languages. It’s an imperfect mapping. And it’s a mapping many of us have gladly accepted. The function is partial because the language cannot express the domain perfectly.
That’s why the whole concept of total functions is important. It gets us thinking about the gaps in our mappings. It gets us thinking about how to do a better mapping. Or about what kinds of checks on the arguments we should do before we call a function or after we get a return value. In short, it’s about safety and trust.
But notice that even in typed languages, there is a gap in the mapping from domain to types. The gap may be smaller than with untyped languages, but there can be a gap. My colleague said it’s meaningless, which implies a Church Typing mindset. It implies that because there are no checks for types, you could pass anything, such as:
(+ “a” 4) ;=> Exception! Expected Number but got String.
That means that even venerable addition is not total in Clojure. I think this is a little disingenuous. This is obviously an incorrect program, even if in general, incorrectness is hard to define in untyped languages. The correct set of values is well-known for + even if it’s not written down. And for any function, all we have to do is write it down—in documentation—and the intended domain is explicit.
I don’t want this essay to be a debate about static vs. dynamic typing. This essay is about totality and how to define it. Totality is really a concept that came from computability theory. It’s for asking questions like “does function f halt for all integer inputs.” The domain is specified by the problem, not the function. That’s why division is partial in programming: The domain is specified from outside, by the language’s choice of types.
In programming we use totality to consider the possible and probable inputs of a function. We concede that we must make imperfect tradeoffs between ideal mathematical objects and available language features. In most type systems, we can’t say “it’s a number, but it can’t be zero” and have the type checker ensure it’s correct.
So I’ve come up with a definition that takes the pragmatics of the idea into account:
A function is total if it returns a valid domain value for every combination of valid domain values as arguments.
In this definition, “valid domain value” is doing a lot of work. It’s purposefully vague. But it asks you, the domain modeler, to consider your domain (in the business domain sense) and the meaningful values in it. It asks you to consider what subset of those values are valid. These often don’t correspond perfectly to types in your language. Ideally there would be a perfect overlap between the domain of a function and the business domain values. Where the overlap is not perfect is where you should look.
I want programmers to think past types and peer deep into the domain. I want them to ask these questions:
What are the meaningful domain values that this function is meant to operate on?
Does that set constitute a cohesive concept?
Are there values that are conceptually cohesive that it won’t work for?
How can I map the set of domain values this function is defined on to language features to get some kind of safety guarantees?
This definition also has a curious effect. Let me demonstrate in Clojure. Let’s say I’m definition a function that should only be defined over non-negative numbers. I don’t have complex numbers in my business domain:
(defn square-root [x] …)
If I’m conscientious, I’ll add a docstring explaining the domain of the function (the set of arguments it is defined over):
(defn square-root
“The square root of a non-negative number.”
[x]…)
Great! But I want the domain to be enforced in code. In Clojure, I might write:
(defn square-root
“The square root of a non-negative number.”
[x]
(assert (not (neg? x)))
…)
Awesome! I’ve now made the function total! We’ve expressed the domain of the function adequately using the features of the language. Ironically, though, we have written code that is more likely to throw when totality is usually defined as throwing less often. But we’re also defining what are valid arguments. Calling (square-root -1) throws an AssertionError, indicating that you, the programmer, violated the contract. So it is total, considering the explicitly defined domain of the function.
These are the kinds of questions I wrestle with when writing a book. I know I use the idea of total function all the time when programming in Clojure. I think it’s valuable. But Clojure doesn’t have types, so what can it mean? Why do others believe it can’t mean anything? I think it’s important to get these ideas right. If you were ever wondering what takes so long to write a book, it’s reading, thinking, digging, conversing until I feel like I’ve got a handle on it.
When you’re working on software design, or any kind of design, there are always hard questions. You can’t rely on pat answers. Instead, you need conceptual models to give you different perspectives. Total functions is one of those. It helps you focus on the failure modes of your functions: Could this function be passed something that will break it? Will it ever return an unexpected value? What would cause it to throw an exception? It’s not about writing code according to some rule, or using a language feature in a particular pattern. You have to think broader than that.