Announcing Arrow Analysis - a Kotlin compiler plug-in

• by Alejandro Serrano
• •
• February 02, 2022
• •
• arrow• kotlin• functional programming
• |
• 8 minutes to read.

We are pleased to announce the first public release of Arrow Analysis! Arrow Analysis is a plug-in for the Kotlin compiler, which supercharges your compilation pipeline with new checks in order to make your code safer and more robust. This is also our first public plug-in using the Arrow Meta compiler framework.

Concise and flow-aware

Take some small yet obviously wrong code in Kotlin: we should not be accessing the third element of an empty list. Still, the compiler happily accepts this code; an exception will haunt us at run time. 👻

val wrong = emptyList<Int>().get(2)

If you enable Arrow Analysis in your project, these ghosts go away. The compilation shows the following error message:

e: Example.kt: (1, 18): pre-condition `index within bounds` is not satisfied in `get(2)`
  -> unsatisfiable constraint: `((2 >= 0) && (2 < emptyList<Int>().size))`
  -> `2` bound to param `index` in `kotlin.collections.List.get`
  -> main function body

This check focuses on a very common, yet very hard to track, problem in Kotlin: out-of-bounds indexing. The right thing would be to always check the size of the list. But, obviously, doing so at every point incurs in a performance overhead. For that reason, we need to mentally track those sizes, and ensure that every use of get is fine.

This is in fact a simple case: no call to get should be allowed on an empty list. But Arrow Analysis is not a simple linter that checks your code against a predefined set of wrong patterns. The tool is aware of your data and control flow. For example, the following is accepted, since we have ensured that the list is not empty by checking its size, so the call to first is correct.

fun List<Int>.firstOrZero() = when (this.size) {
  0 -> 0
  else -> this.first()
}

This awareness means that Arrow Analysis has a low rate of false positives. Other tools cannot raise a flag for every usage of get because otherwise the report would be full of potential-yet-already-handled problems. Arrow Analysis solves this problem of error proliferation by making the checks more aware of its surroundings.

The code above makes it crystal clear we are checking sizes, but the same result would be obtained with a more idiomatic version that uses isNotEmpty.

fun List<Int>.firstOrZero() =
  if (this.isEmpty()) 0 else this.first()

Arrow Analysis supports the definition of fields, and we have included as part of the laws of the standard library that isNotEmpty is equivalent to size > 0. Had we missed some important law, you can write it yourself, because Arrow Analysis is fully extensible. Feel free to have a look at those laws yourself. 🔍

Extensible

Arrow Analysis ships with checks for many functions in Kotlin’s standard library. In addition, it exposes mechanisms to introduce checks in your own functions and classes. In other words, you can extend the set of checks that Arrow Analysis performs on your code.

For example, we may ask Arrow Analysis to guarantee that the value passed to the age parameter in any call to this buildPerson is not negative by adding a precondition.

fun buildPerson(name: String, age: Int) {
  pre(age >= 0) { "age must not be negative" }
  // do other stuff
}

After that, any call to buildPerson for which such a condition over age is not guaranteed will be flagged as an error. This may be because we can certainly see that the value is problematic (like in a call buildPerson("me", -1)) or because we don’t have enough information to guarantee it (if the data comes from user input, for example).

Maybe the concept of age is so common in your domain that you want to introduce a specific Age class. You can then attach the property of being greater or equal to 0 as an invariant of the class, something that should always be true of the value.

class Age(val n: Int) {
  init { require(n >= 0) }
}

Built upon proven technology

Arrow Analysis is able to perform complex reasoning. One of my favorite examples is this type for positive numbers. In the case of the plus operator, the check uses the fact that both this.value and other.value are positive (because the invariant declared in the Positive class) to deduce that this.value + other.value is also positive, and as a result we are allowed to call the Positive constructor.

class Positive(val value: Int) {
  init { require(value > 0) }

  fun operator plus(other: Positive) =
    Positive(this.value + other.value)
}

To perform its duty, Arrow Analysis uses a SMT solver. These kind of solvers have been used for more than a decade in both academic and industrial environments, and provide an incredible amount of reasoning power over simple types such as booleans and integers.

Easy to set up

Why not give Arrow Analysis a try? It’s as easy as adding the following line in your Gradle build file:

buildscript {
  dependencies {
    classpath("io.arrow-kt.analysis.kotlin:io.arrow-kt.analysis.kotlin.gradle.plugin:2.0")
  }
}

apply(plugin = "io.arrow-kt.analysis.kotlin")

This takes care of applying the compiler plug-in to your project, and comes with a big set of checks for many types in Kotlin’s standard library, including collections.

There is more to come!

This first release of Arrow Analysis is already a booster for the Kotlin compiler. But work in such a tool never ends, and in fact we are already working on many improvements:

• The current version includes powerful reasoning over numbers, but the reasoning on strings is limited (we only know a bit about their lengths). We aim to extend this functionality to cover string operations and regular expressions, another common source of invariants for types. To do so, we are sending patches to the java-smt library.
• Something similar can be said about mutable variables: there is some preliminary support, but will improve in upcoming versions. Right now, Arrow Analysis works best with functional and immutable domain modeling.
• Reporting as part of the Gradle build is great, but if made part of a CI pipeline, those warnings may be easily missed. We are working on integration with GitHub’s Code Scanning to report those errors as part of the review. This is a preliminary example.
• Kotlin is a great language that builds upon the greater Java ecosystem. Using the same core technology, we have built a Java compiler plug-in.

Join us on this journey

These are just a few of the highlights of what you can do Arrow Analysis. Our Quick Start tells you how to make your code safer with just a few lines of Gradle configuration. For more detailed info and documentation, please visit Arrow-kt.io.

If you are interested in contributing, learning, or have any questions about Arrow Analysis, Arrow Meta, or the Arrow project as a whole, don’t be shy and join us on the Kotlin Slack in the #arrow channel. We are an inclusive group of people committed to providing the best experience to our users and community, and we look forward to seeing you there!