Handling function partiality

Last modified on June 28, 2020 by Alex

Consider the following snippet:

Conceptually, isqrt_option is a partial function from natural numbers to natural numbers that returns square root of its input rounded down. It has a particular flavour of partiality as I will explain soon.

Flavours of partiality - the callee side

There are many ways to implement a partial function. We have already seen how we can use Optional return values to implement partiality. We can similarly use Either:

Sometimes you want to use an assertion instead because of some really complex type refinement (e.g. inter-dependency between multiple input data structures), that would be difficult to express in types without a dependently typed language (or even then!):

Alternatively, we can use type refinements (using refined Scala library or something similar).

The caller side

Imagine that a caller of isqrt function has already verified that num is positive:

We can see that using Optional return values just moves partiality to the call-site. The problem is that even though we know that num > 0, most modern compilers are not able to infer that the None case is impossible (the only exception that I know of is Code Contracts for C#, which has some very similar functionality).

Let’s see how the same code would look like if we used isqrt_assert:

Notice that this coding style will necessarily result in some runtime failures due to your logical errors (which are bound to happen sooner or later!), but it is mighty convenient.

Using the refinement-based solution:

Beautiful. But… what if we wanted to compute a square root of a square root?

We have to modify the definition of isqrt_refined:

With a better compiler or language perhaps this could have been avoided, but sooner or later, the asserts will creep back in into your code. In dependently typed languages that will happen when you are just too tired to prove some property of your code, so you invoke believe_me. And no matter how good a compiler is, the halting problem will prevent it from proving all of potential code properties (but it could still have insanely large coverage, being able to say prove 99.999999% of all properties).

Don’t hate the assert, it is your friend! You just need to learn to use it in a tasteful way.