Handling function partiality

Last modified on


Consider the following snippet:

def isqrt_option(num: Int): Option[Int] = {
  num match {
    case x if x >= 0 => Some(math.sqrt(x).toInt)
    case _ => None
  }
}

Conceptually, isqrt_option is a partial function from natural numbers to natural numbers that returns square root of its input rounded down. This function represents a specific type of partial function, the details of which will be discussed shortly.

1. Flavours of partiality - the callee side

Section missing id

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:

final case object NegativeInputArgument(value: Int)

def isqrt_either(num: Int): Either[NegativeInputArgument, Int] = {
  num match {
    case x if x >= 0 => Right(math.sqrt(x).toInt)
    case x => Left(NegativeInputArgument(x))
  }
}

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!):

/**
  * @param num non-negative integer
  */
def isqrt_assert(num: Int): Int = {
  assert(num >= 0)
  math.sqrt(num).toInt
}

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

final case class NonNegInt private (value: Int) {
  assert(value >= 0)
}
object NonNegInt {
  def refine(i: Int): Option[NonNegInt] =
    if (i > 0) Some(NonNegInt(i))
    else None

  // A macro would allow us to specify literal non-negative integers.
  implicit def literal(x: Int): NonNegInt = macro applyImpl
}

def isqrt_refined(num: NonNegInt): Int =
  math.sqrt(num.value).toInt

2. The caller side

Section missing id

Let's now shift our focus to the caller side of isqrt function. Consider a scenario where the caller has already ensured that num is positive:

val num = ...
if (num > 0) {
  ...
  val r = isqrt_option(num)
  r match {
    case Some(x) => ...
    case None =>
      // OOPS, what do we do here?
  }
}

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:

val num = ...
if (num > 0) {
  ...
  val r = isqrt_assert(num)
  // No need to match on r, it's already an Int.
  ...
}

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 extremely convenient.

Using the refinement-based solution:

val num = ...
NonNegInt.refine(num) match {
  case Some(num) =>
    ...
    val r = isqrt_refined(num)
    // No need to match on r, it's already an Int.
    ...
  case None =>
    ...
}

This code is elegantly simple, but problems can arise when we try to compute the square root of a square root.

val r = isqrt_refined(num)
val r1 = isqrt_refined(r) // OOPS, doesn't compile

We have to modify the definition of isqrt_refined:

def isqrt_refined(num: NonNegInt): NonNegInt =
  NonNegInt.make(math.sqrt(num.value).toInt) match {
    case Some(n) => n
    case None => ???
  }

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).

It's important to note that assert can be a valuable tool when used appropriately. While it might seem tempting to avoid or minimise its use, understanding its role and functionality can significantly improve your code's robustness and reliability.

References

  1. linkcode-contracts