Subtracting natural numbers: types and usability

For several years now I have been working on a functional teaching language for discrete mathematics, called Disco. It has a strong static type system, subtyping, equirecursive algebraic types, built-in property-based testing, and mathematically-inspired syntax. If you want to know more about it in general, you can check out the GitHub repo, or give it a try on replit.com.

In this blog I want to write about a particular usability issue surrounding the type of the subtraction operation, partly because I think some might find it interesting, and partly because forcing myself to clearly articulate possible solutions may help me come to a good resolution.

The problem with subtraction

Disco supports four basic numeric types: natural numbers \(\mathbb{N}\), integers \(\mathbb{Z}\), “fractional” numbers \(\mathbb{F}\) (i.e. nonnegative rationals), and rational numbers \(\mathbb{Q}\). These types form a subtyping lattice, with natural numbers being a subtype of both integers and fractionals, and integers and fractionals in turn being subtypes of the rationals. All the numeric types support addition and multiplication; the integers allow negation/subtraction, the fractionals allow reciprocals/division, and rationals allow both.

So what is the type of \(x - y\)? Clearly it has to be either \(\mathbb{Z}\) or \(\mathbb{Q}\); that’s the whole point. Natural numbers and fractional numbers are not closed under subtraction; \(\mathbb{Z}\) and \(\mathbb{Q}\) are precisely what we get when we start with \(\mathbb{N}\) or \(\mathbb{F}\) and decide to allow subtraction, i.e. when we throw in additive inverses for everything.

However, this is one of the single biggest things that trips up students. As an example, consider the following function definition:

fact_bad : N -> N
fact_bad(0) = 1
fact_bad(n) = n * fact_bad(n-1)

This looks perfectly reasonable on the surface, and would work flawlessly at runtime. However, it does not typecheck: the argument to the recursive call must be of type \(\mathbb{N}\), but since \(n-1\) uses subtraction, it cannot have that type.

This is very annoying in practice for several reasons. The most basic reason is that, in my experience at least, it is very common: students often write functions like this without thinking about the fact that they happened to use subtraction along the way, and are utterly baffled when the function does not type check. This case is also extra annoying since it would work at runtime: we can clearly reason that if \(n\) is a natural number that is not zero, then it must be \(1\) or greater, and hence \(n-1\) will in fact be a natural number. Because of Rice’s Theorem, we know that every decidable type system must necessarily exclude some programs as untypeable which nonetheless do not “go wrong”, i.e. exhibit no undesirable behavior when evaluated. The above fact_bad function is a particularly irksome example.

To be clear, there is nothing wrong with the type system, which is working exactly as intended. Rather, the problem lies in the fact that this is a common and confusing issue for students.

Implementing factorial

You may be wondering how it is even possible to implement something like factorial at all without being able to subtract natural numbers. In fact, there are two good ways to implement it, but they don’t necessarily solve the problem of student confusion.

• One solution is to use an arithmetic pattern and match on n+1 instead of n, like this:

  fact_ok1 : N -> N
  fact_ok1(0) = 1
  fact_ok1(n+1) = (n+1) * fact_ok1(n)

  This works, and it’s theoretically well-motivated, but feels somewhat unsatisfying: both because we have to repeat n+1 and because this style of definition probably feels foreign to anyone except those who have played with a Nat algebraic data type (which excludes the vast majority of Discrete Math students).

• Another solution is to use a saturating subtraction operator, \(x \mathbin{\dot -} y = \max(0, x - y)\). In Disco this operator is written x .- y. Unlike normal subtraction, it can have the type \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\), so we can rewrite the factorial function this way:

  fact_ok2 : N -> N
  fact_ok2(0) = 1
  fact_ok2(n) = n * fact_ok2(n .- 1)

  The .- operator is also theoretically well-motivated, being the “monus” operator for the commutative monoid of natural numbers under addition. However, in my experience, students are annoyed and confused by this. They often do not understand when and why they are supposed to use .-. Of course, better error messages could help here, as could better pedagogy. This is actually my current approach: this semester I talked about the difference between \(\mathbb{N}\) and \(\mathbb{Z}\) very early, hitting on the fact that \(\mathbb{N}\) is not closed under subtraction, and explicitly made them explore the use of the .- operator in their first homework assignment. We’ll see how it goes!

Some tempting and expedient, but wrong, solutions

One solution that sounds nice on the surface is to just pun the notation: why not just have a single operator -, but make it behave like .- on types without negation (\(\mathbb{N}\) and \(\mathbb{F}\)), and like normal subtraction on \(\mathbb{Z}\) and \(\mathbb{Q}\)? That way students wouldn’t have to remember to use one version or the other, they can just use subtraction and have it do the right thing depending on the type.

This would be sound from a type system point of view; that is, we would never be able to produce, say, a negative value with type \(\mathbb{N}\). However, in the presence of subtyping and type inference, there is a subtle problem from a semantics point of view. To understand the problem, consider the following function:

f : N -> Z
f(n) = (-3) * (n - 5)

What is the output of f(3)? Most people would say it should be (-3) * (3 - 5) = (-3) * (-2) = 6. However, if the behavior of subtraction depends on its type, it would also be sound for f(3) to output 0! The input 3 and the constant 5 can both be given the type \(\mathbb{N}\), in which case the subtraction would act as a saturating subtraction and result in 0.

What’s going on here? Conceptually, one of the jobs of type inference, when subtyping is involved, is to decide where to insert type coercions. (Practically speaking, in Disco, such coercions are always no-ops; for example, all numeric values are represented as Rational, so 3 : N and 3 : Q have the same runtime representation.) An important guiding principle is that the semantics of a program should not depend on where coercions are inserted, and type-dependent-subtraction violates this principle. f(3) evaluates to either 6 or 0, depending on whether a coercion from \(\mathbb{N}\) to \(\mathbb{Z}\) is inserted inside or outside the subtraction. Violating this principle can make it very difficult for anyone (let alone students!) to understand the semantics of a given program: at worst it is ambiguous or undefined; at best, it depends on understanding where coercions will be inserted.

What about having - always mean subtraction, but crash at runtime if we try to subtract natural numbers and get something less than 0? That way we can use it as long as we “know it is safe” (as in the factorial example). Unfortunately, this has the exact same issue, which the above example with f(3) still illustrates perfectly: f(3) can either evaluate to 6 or crash, depending on exactly where coercions are inserted.

Typechecking heuristics?

Another interesting option would be to make typechecking a bit smarter, so that instead of only keeping track of the type of each variable, we also sometimes keep track of values we statically know a variable can and can’t have in a certain context. We could then use this information to allow subtraction to have a type like \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) as long as we can statically prove it is safe. For example, after matching on 0 in the first line of fact_bad, in the second line we know n cannot be 0, and we could imagine using this information to decide that the expression n - 1 is safe. This scheme would not change the semantics of any existing programs; it would only allow some additional programs to typecheck which did not before.

Of course, this would never be complete—there would always be examples of Disco programs where we can prove that a certain subtraction is safe but the heuristics don’t cover it. But it might still go a long way towards making this kind of thing less annoying. On the other hand, it makes errors even more mysterious when they do happen, and hard to understand when a program will and won’t typecheck. Perhaps it is best to just double down on the pedagogy and get students to understand the difference between \(\mathbb{N}\) and \(\mathbb{Z}\)!

Division?

As a final aside, note that we have the same issue with division: x / y is only allowed at types \(\mathbb{F}\) or \(\mathbb{Q}\). If we want to divide integers, we can use a different built-in operator, // which does integer division, i.e. “rounds down”. However, this is not nearly as bad of an issue in practice, both because some students are already used to the idea of integer division (e.g. Python makes the same distinction), and because wanting to divide integers does not come up nearly as often, in practice, as wanting to subtract natural numbers.