Property based testing in Unison
Tags: unison, testing, functional
Published: 2020-01-21 18:01:05

#### 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](https://dev.to/jdsteinhauser/intro-to-property-based-testing-2cj8) with some pointing to a number of different [approaches](https://fsharpforfunandprofit.com/posts/property-based-testing-2/).

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"](https://dev.to/petets/eliminate-consecutive-duplicates-57hi) 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.

```unison
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](https://www.unisonweb.org/docs/tour#a-property-based-test). 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](https://en.wikipedia.org/wiki/Associative_property)!

And here is one way to prove that the natural number addition assosiative property holds in `Unison`:
```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](https://www.unisonweb.org/docs/tour#syntax-notes) 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).

```ucm
.> 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](https://www.unisonweb.org/docs/language-reference#abilities-and-ability-handlers).

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

```unison
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.

```unison
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`


```unison
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.

```unison
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

```unison
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

```unison
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

```unison
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

```unison
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
```unison
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
```unison
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

```unison
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

```unison
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

```unison
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.