Mutability and loops

Λrrow Analysis supports mutability at the level of functions (but not yet at the level of classes). However, when you declare something with var, things get tricky. 👻

When a local variable x is immutable

val x = COMPLICATED_THING

the check knows upfront that any usage of x correspond to the same COMPLICATED_THING, wherever it’s used later on. However, if the declaration uses var, at the point in which we use x the value inside of it may be completely different from the first one!

The way out of this problem is to promise Λrrow Analysis that some condition over a mutable variable will always be true for the entire computation:

• the check can base its reasoning on this promise,
• but we need to check that you obbey your promise every time you try to give a new value.

We call this promise an invariant of the mutable variable.

As a consequence, if you do not declare an invariant, Λrrow Analysis knows nothing about your variable. Here’s an example which is “obviously” correct, but not accepted by the tool:

import arrow.analysis.post

fun usesMutability(x: Int): Int {
  var z = 2
  return z.post({ it > 0 }) { "greater than 0" }
}

e: declaration `usesMutability` fails to satisfy the post-condition: ($result > 0)

Let’s declare an invariant. We use the same syntax as post-conditions, but use the special function invariant instead. Note that even though syntactically the invariant reads as part of the initial value, it really talks about the mutable variable being declared (z in this case) . After attaching this information to the variable, we are free to re-assign the variable, but we need to keep our promise.

import arrow.analysis.invariant
import arrow.analysis.post

fun usesMutability(x: Int): Int {
  var z = 2.invariant({ it > 0 }) { "invariant it > 0" }
  z = 3
  return z.post({ it > 0 }) { "greater than 0" }
}

Of course, if we don’t keep our promise, Λrrow Analysis won’t be happy.

import arrow.analysis.invariant
import arrow.analysis.post

fun usesMutability(x: Int): Int {
  var z = 2.invariant({ it > 0 }) { "invariant it > 0" }
  z = 0 // 0 is not > 0
  return z.post({ it > 0 }) { "greater than 0" }
}

e: invariants are not satisfied in `z = 0`

Loops

One place in which mutability is hard to avoid is loops. Our recommendation is to think carefully about invariants for your mutable variables, because a good choice will determine what can be checked. Here’s an example in which we compute the length of a list using a mutable integral variable:

import arrow.analysis.invariant
import arrow.analysis.post

fun <A> List<A>.count(): Int {
  var count = 0.invariant({ it >= 0 }) { "z >= 0" }
  for (elt in this) { count = count + 1 }
  return count.post({ it >= 0 }) { "result >= 0" }
}

We are investigating ways to introduce additional information in the tool, like for looping exactly many times as the size of the list.