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 inputlist [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 outputlist [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 outputlist 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 inputlist U would be equal to the outputlist 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 asx
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 operationinit ++ [last, last]
.
 The U list containing
 Unrelated to the cornercase above, C ++ [x] will be compressible, for any value
x
regardless of whetherx
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 theuse
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 testpredicate function?
The predicate functionchecks if after compression an outputlist contains less elements than the inputlist. 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.
Top comments (0)