Property testing in Unison

Quick reminder that Unison is still in public alpha!

Parts of the language, testing functionality and libraries that appear in this post might be subject to change.

On properties

There are a lot of very good resources on property testing out there with some pointing to a number of different approaches.

Depending on whom you ask and what your current level of familiarity is, identifying properties of the code being delivered may fall under the "easier said than done" column. I will use the compress function from my previous blog post "Eliminate consecutive duplicates" to try and highlight what the process might look like.

This post is meant to help the reader explore:

• property based testing as a concept and practice.
• the Unison programming language.
• just how easy it is to write property tests in Unison.

Remind me about compress real quick?

Being parametric on type a when given an input-list [a] compress will remove consecutive elements in the list, if any exist. Do not be afraid of some level of formality: for two lists [1, 2, 3] and [1, 1, 1], the former would be classed as non compressible, whereas the latter would be classed as compressible. The result of the compression being the output-list [1].

In the previous blog post I implemented compress in multiple ways and here's the one I want to test using property tests.

base.List.compress: [a] -> [a]
base.List.compress as = case as of
  [] -> []
  [x] -> [x]
  [x, y] ++ rest ->
    if (x == y) then base.List.compress (y +: rest)
    else x +: base.List.compress (y +: rest)

What will be our testing criterion?

In the following section, C denotes a compressible list, and U a list that cannot be compressed. A list is compressible if after compress is applied to it, the output-list contains less elements than the input.

This is an arbitrarily picked criterion and different criteria could be selected, hence why I called it "our" criterion. Another criterion might be that an input-list U would be equal to the output-list U.

What are (some of) the properties of compress?

Non compressible list properties

• The minimum U list is the empty list.
• Any list [x] (containing a single element) is equally not compressible.
• U ++[x] will be non compressible, for any value x as long as x is not equal to the last element.
• The above can be generalised so that U ++ U will be compressible if the head and tail of U are the same element.
• Inversely: removing elements one at a time from a U list and finally reaching the point of the empty list, produces a sequence of U lists.

Compressible list properties

• For each element x, the list [x, x] is the minimum non empty C list.
• The above can be generalised in two ways:
  • The U list containing head +: tail can be converted to a C list by means of the operation [head, head] ++ tail.
  • The U list containing init :+ last can be converted to a C list by means of the operation init ++ [last, last].
• Unrelated to the cornercase above, C ++ [x] will be compressible, for any value x regardless of whether x is equal to the last element of C or not (as the compressible section does not need to be in the end).
• Generalising the above: C ++ U is compressible, just like U ++ C is compressible, just like C ++ C is compressible.
• U ++ U will be compressible if the head and tail of U are the same element.

Whether a list can be compressed or not is all about content. As long as the equal consecutive elements are always one next to the other, a class of list manipulation operations like reversing will not affect the ability of the list to compress or not.

The lists of properties above might not necessarily be exhaustive but we have more than a few to work with. Note that properties are a mathematical concept so there is a certain degree of lack of formal notation and formal definition in the section above, as well as some leaps in logic that might not hold water from a strict mathematical perspective. The focus of this post however is not math, but Unison.

Now what about Unison specifically?

The relevant section of the documentation can be found in the Unison tour. Please follow the link and have a read!

Here is a step by step breakdown of what the pieces involved:

• A use .base.test.v1 statement.
• Each line that declares a property test must begin with test>.
• The test> expression is followed by the name of the test this "path" reflects the namespace under which the test will be added.
• The property itself, as in the content of the go function.
• A call to the runs function specifying how many times to run which test, in the example, 100 go

I know that the addition of natural numbers is associative!

And here is one way to prove that the natural number addition assosiative property holds in Unison:

use builtin.Nat +

test> tests.base.Nat.associative = 
  go _ = a = !nat
         b = !nat
         c = !nat
         expect (((a + b) + c) == (a + (b + c)))
  runs 100 go

What just happened?

There is a Unison syntax guide that is part of the tour:

• ucm had a hard time time finding out which of all the functions called + the code was referring to, so it was guided to pick the one for natural numbers by the use statement.
• The delayed ability to generate a natural number (nat) was forced with the exclamation mark syntax (!nat).
• Which means that the nat function, for each call, produced one natural number.
• The expect function was used to test the property.
• The property was expressed as a boolean equality check.
• The go function and contained code block is the test, and it ignores its first argument _.
• Ignoring the first argument is the mechanism in Unison to make a function lazy (caveat: if my understanding of the documentation is correct).
• The aptly named runs function is what actually "runs" the "property" 100 times.

What building blocks does Unison provide?

Unison comes with generators that are exposed by the Gen ability under the base.test.v1 namespace to produce values of given types. We can build on top of the nat and list (generator and function respectively) to craft genetators and functions that produce lists of that are known to meet certain criteria, for use in property tests. The generators are not random (as I originally thought).

.> view base.test.v1.nat

  base.test.v1.nat : '{Gen} Nat
  base.test.v1.nat = '(Gen.sample Weighted.nats)

.> view base.test.v1.list

  base.test.v1.list : '{Gen} a -> '{Gen} [a]
  base.test.v1.list g =
    'let
      size = !nat
      List.map (_ -> !g) (range 0 size)

The Gen ability is handled by the Unison test runtime. The how exactly is beyond our scope at this time. If you are not fully familiar with abilities, they are covered in the documentation.

What is the test-predicate function?

The predicate functionchecks if after compression an output-list contains less elements than the input-list. To make the tests a bit more readable the compression is hidden inside the predicate.

should_compress: [a] -> Boolean
should_compress as = (size . compress) as < size as

should_not_compress: [a] -> Boolean
should_not_compress = not . should_compress

Compressible generators

To benefit from compositionality begin by coding a generator that produces a minimum compressible list (the content of which could be randomised). This generator can then be peppered on to other lists to make any otherwise non compressible list always compressible.

base.test.v1.min_compressible : '{Gen} a -> '{Gen} [a]
base.test.v1.min_compressible g =
  'let
    x = !g
    [x, x]

min_compressible gets passed an argument g that is a delayed generator of type a. The generator is forced to produce a value with !g

base.test.v1.compressible : '{Gen} a -> '{Gen} [a]
base.test.v1.compressible g =
  'let
    !(min_compressible g) ++ !(list g)

Syntactically, same as above, !(min_compressible g) forces min_compressible to return a minimum compressible list, the content of which is produced by the generator g, and !(list g) does the same, except the list produced by !(list g) is not structured.

Non compressible generators

Having a second look at the base.test.v1.list list generator, there is no guarantee that consecutive calls of the g generator that it reuses for the value of each element, will not yield the same value twice.

Furthermore g is passed as an argument so without an in depth understanding of how g could behaved the list generator is bound to always produce unexpected results for a whole class of generators like a constant generator that always produces a fixed value.

Narrowing the scope for natural numbers only, here is one way to produce a non compressible list.

base.test.v1.non_compressible : '{Gen} [Nat]
base.test.v1.non_compressible =
  'let
    start = !nat
    size  = !nat
    List.map (i -> start + i) (range 0 size)

The list begins with a natural number and all numbers after it are sequenced after incrementing so there can be no consecutive duplicates. But, there is no guarantee that consecutive calls of this generator will not end up producing lists that when concatenated are compressible, for example [1, 2, 3] and [3]. To avoid this we would need to code a generator that produces two lists at the same time, to ensure their content cannot be compressed when appended (beyond the scope of this blog).

Let's write some properties then!

The minimum non compressible list is the empty list

test> tests.compress.emptyIsNotCompressible = 
  go _ = expect (should_not_compress [])
  runs 1 go

In a language where there would be a need to import a unit test library and a separate property test library, one might be tempted to code a simple unit test as a property test of a single run, to save the time and energy of dealing with multiple test libraries. In this instance and at this point in time in the evolution of Unison: it does not really matter. The test result is cached regardless.

Every list of a single element is non compressible

test> tests.compress.singleElement = 
  go _ = expect (should_not_compress [!nat])
  runs 1 go       

Every non compressible list can be sequentially deconstructed to non compressible lists

recurse: ([a] -> Boolean) -> [a] -> Boolean
recurse pred as = 
  pred as && case (as, as) of 
    (_ +: t, i :+ _) -> recurse pred t && recurse pred i
    ([], []) -> pred []

test> tests.compress.decomposeU = 
  go _ = l = !(non_compressible)
         expect (recurse should_not_compress l)
  runs 100 go

A non compressible list appended to a non compressible list is compressible under some circumstances

test> tests.compress.uAppendU = 
  go _ = a = !(non_compressible)
         b = !(non_compressible)
         lambda = case (a, b) of
           (_ :+ l, h +: _) -> 
             if h == l then should_compress else should_not_compress
            _ -> should_not_compress
         expect (should_not_compress a 
           && should_not_compress b && lambda (a ++ b) )
  runs 100 go       

Every non empty minimum compressible list can be compressed

test> tests.compress.minimumCompressible = 
  go _ = expect (should_compress !(min_compressible nat))
  runs 100 go       

Every compressible list appended to a non compressible list results in a compressible list

test> tests.compress.cAppendU = 
  go _ = a = !(min_compressible nat)
         b = !non_compressible
         expect (should_compress a && should_not_compress b && should_compress (a ++ b))
  runs 100 go       

Every non compressible list appended to a compressible list results in a compressible list

test> tests.compress.uAppendC = 
  go _ = a = !non_compressible
         b = !(min_compressible nat)
         expect (should_compress (a ++ b))
  runs 100 go       

Every compressible list appended to a compressible list results in a compressible list

test> tests.compress.cAppendC = 
  go _ = a = !(min_compressible nat)
         b = !(min_compressible nat)
         expect (should_compress (a ++ b))
  runs 100 go       

Every compressible list extended by an element is still compressible

test> tests.compress.extendC = 
  go _ = a = !(compressible nat)
         b = !nat
         expect (should_compress a && should_compress (a ++ [b]))
  runs 100 go

Closing note

I hope I have managed to communicate in this post just how easy and pleasant it is to work with Unison when it comes to property based testing.