Property Based Testing in Elm with elm-check

Property-based testing is a style of testing that focuses on making claims about your system and attempting to disprove these claims. The goal of elm-check is to automate this process.

The most common method of testing is unit-testing. Unit-testing consists in manually stating assertions that certain inputs yield certain outputs. While familiar, this approach has several drawbacks.

1. Writing assertions is a very boring and tedious process.
2. More often than not, the inputs chosen to test are completely arbitrary and may give little insight to the correctness of your system.
3. Even if a unit test did fail, the failed unit may or may not be helpful to diagnose your problem.

The way elm-check solves these problems is by

1. Automate the generation of unit tests
2. Use random number generation to explore an arbitrarily large sample of your input space
3. Compute a minimal failing case which is then more representative of the issue encountered in your system by the test.

How it works

elm-check is centered around the idea of claims and investigators. You make a claim of truth about your system and have an investigator check the claim.

For example, suppose you wanted to test a function to reverse a list of elements.

reverse : List a -> List a

For this to be a correct reverse function, there are a number of properties that must hold true, such as:

1. Reversing a list twice yields the original list
2. Reversing does not modify the length of a list

You can make these claims in elm-check as follows:

claim_reverse_twice_yields_original =
  claim
    "Reversing a list twice yields the original list"
  `that`
    (\list -> reverse (reverse list))
  `is`
    (identity)
  `for`
    list int


claim_reverse_does_not_modify_length =
  claim
    "Reversing a list does not modify its length"
  `that`
    (\list -> length (reverse list))
  `is`
    (\list -> length list)
  `for`
    list int

As, you can see, elm-check defines a DSL for writing claims. The code reads very simply.

The first claim claims that reversing a list twice yields the original list. The string passed to claim is used for displaying, so make it as descriptive as necessary. Then that takes your actual statement about reverse, i.e. reversing it twice. is takes your expected statement about reverse, i.e. that it is the identity function. This is analogous to expected vs actual in unit testing. You expect that reversing a list twice is equivalent to not doing anything to the list. for then takes an investigator for the claim. In this case, list int will investigate the space of possible lists of integers and will try to disprove the claim.

You can then test each claim individually using the quickCheck function:

result1 = quickCheck claim_reverse_twice_yields_original
result2 = quickCheck claim_reverse_does_not_modify_length

Or you can group these claims in a suite and check the suite:

suite_reverse =
  suite "List Reverse Suite"
    [ claim_reverse_twice_yields_original
    , claim_reverse_does_not_modify_length
    ]

result = quickCheck suite_reverse

quickCheck will take either a single claim or a suite of claims and will run 100 checks on each claim to attempt to disprove each claim. quickCheck will then return a descriptive result of the checks performed.

You can then visualize these results using the display function:

main = display result

And, voila, in just a few lines of code, you have made two different claims about the reverse function and performed 200 checks and displayed the results.

Simple example

Let us look at a very simple example to get a feel for how to use elm-check.

Suppose we wanted to test that multiplication and division are inverse operations.

You would make this claim as follows:

claim_multiplication_division_inverse =
  claim
    "Multiplication and division are inverse operations"
  `that`
    (\(x, y) -> x * y / y)
  `is`
    (\(x, y) -> x)
  `for`
    tuple (float, float)

Now, if you run quickCheck on this claim and displayed it in the browser with display, you would get:

Multiplication and division are inverse operations FAILED after 1 check!
  - Counter example: (0,0)
  - Actual: NaN
  - Expected: 0

This result shows that elm-check has found a counter example, namely (0,0) which falsifies the claim. This is obviously true because division by 0 is undefined, hence the NaN value.

We can solve this issue by adding this condition to our actual statement and modify it as follows:

claim_multiplication_division_inverse =
  claim
    "Multiplication and division are inverse operations"
  `that`
    (\(x, y) -> if y == 0 then x else x * y / y)
  `is`
    (\(x, y) -> x)
  `for`
    tuple (float, float)

So, we added the condition where if y is 0, we simply return x. Now, let's see what elm-check gives us now if we run quickCheck.

Multiplication and division are inverse operations FAILED after 1 check!
  - Counter example: (0.0001073802195855836,0.00013967437556471545)
  - Actual: 0.00010738021958558358
  - Expected: 0.0001073802195855836

Uh-oh, a new counter example. So, we can see that the actual and the expected values are incredibly close. From their closeness we can easily infer that something went wrong in the rounding. This is exactly what has happened as this is a floating-point error.

An interesting thing to note is that the counter example found was incredibly close to the original one of (0,0). How come? The float investigator has the ability to generate any random float. So, what has happened here?

Well, to do this let us look back at the original claim:

claim_multiplication_division_inverse =
  claim
    "Multiplication and division are inverse operations"
  `that`
    (\(x, y) -> x * y / y)
  `is`
    (\(x, y) -> x)
  `for`
    tuple (float, float)

And this time, instead of displaying the results with display, let us use the alternative displayVerbose function which gives more detail about the test results.

Now, we get this output:

Multiplication and division are inverse operations FAILED after 1 check!
  - Counter example: (0,0)
  - Actual: NaN
  - Expected: 0
  - Seed: State 879767458 1052200661
  - Number of shrinking operations performed: 4
  - Before shrinking:
    - Counter example: (-14.074540141521613,-18.307399754018384)
    - Actual: -14.074540141521611
    - Expected: -14.074540141521613

From here we can see that there are a "seed", a "number of shrinking operations performed" and a "before shrinking" fields. The "seed" is there in order to reproduce test results. The "shrinking" stuff relates to a feature that elm-check provides called "shrinking".

Shrinking is the idea of shrinking a test case to a minimal representation. In this case, the investigator tuple (float, float) has found the original counter example (-14.074540141521613,-18.307399754018384). It has then taken this counter example and has searched for another counter example that is more minimal that still disproves the claim. It has then repeated this process until it finds no more minimal counter example that still disproves the claim, in this case, simply (0,0). Intuitively, (0,0) is as minimal an input as it gets. Having such minimal inputs is key to diagnosing problem.

As we have seen, this simple claim has enabled us to diagnose two gotchas about division. Get used to this as it is very common for individual claims to encounter multiple problems with a system.

Migrating from previous version (prior to Elm 0.15)

If you are currently using elm-check in Elm 0.14 code and would like to upgrade your tests to 0.15, you are going to like the new features and the simplified API.

API CORE

First of all, elm-check does not deal simply with the Random.Generator type.

The api is centered around two functions:

claim : String -> (a -> b) -> (a -> b) -> Investigator a -> Claim

check : Claim -> Int -> Seed -> Evidence

and three types : Claim, Investigator, and Evidence.

• Claim is exactly analogous to Property in the previous version. The difference between Claim and Property is that Claim captures an expected vs actual relation. This means that elm-check can and does generate actual unit tests unlike previously where you could only deal in predicates. If you still want to define claims as predicates, you can use the claimTrue function or the true combinator if you are using the DSL.

• Evidence is the result type from running check on a claim or a suite of claims. This is analogous to TestOutput in the previous version. The difference is that now Evidence has additional information regarding shrinking.

• Investigator is the new kid in town. elm-check still relies on random generation provided by the Random.Generator type but, now, elm-check ships with shrinking out of the box and the Investigator type provides this.

type alias Investigator a =
  { generator : Random.Generator a
  , shrinker  : Shrinker a
  }

-- type alias Shrinker a = a -> List a

If you are familiar with Haskell's QuickCheck, then Investigator is exactly like Arbitrary in Haskell. From a user point of view, the main difference between using investigators and generators is that investigators are not as composable as generators. You can use operations such as map, flatMap, etc... on generators but not on investigators. This is due to shrinking. The shrinking algorithms used in elm-check can be found in elm-shrink, the companion library to elm-check.

But, in case you are worried about the composability, here's a concrete example of implementing your own investigator for a custom data type.

type alias Vector =
  { x : Float
  , y : Float
  , z : Float
  }

vector : Investigator Vector
vector =
  let
      shrinker {x,y,z} =
        Vector
          `Shrink.map`    shrink float x
          `Shrink.andMap` shrink float y
          `Shrink.andMap` shrink float z

      generator =
        Vector
          `Random.map`    random float
          `Random.andMap` random float
          `Random.andMap` random float
  in
      investigator generator shrinker

As you can see, you have to define separately a shrinker and a generator with the provided map and andMap functions. The Random functions come from elm-random-extra and the Shrink functions come from elm-shrink. Hopefully, the above code shows that the process is not overly complicated. Note that Shrink.map is just an alias for List.map. There is unfortunately no magical map function on shrinkers. So, you have to capture the data from the record you wish to shrink and then re-map it Shrink.map.

Organizing Tests

One of the big features introduced in this version of elm-check is the ability to group claims together in suites using the suite function.

suite : String -> List Claim -> Claim

suite takes in a descriptive name for a suite and a list of claims and then outputs a claim. This makes suites themselves claims and thus arbitrarily nestable, which is key to represent your modules adequately.

For example, if you wanted to test the core List module, you could organize your claims as follows:

suite_list =
  suite "List Suite"
    [ suite "List Reverse"
      [ claim_reverse_reverse_identity
      , claim_reverse_preserves_length
      , ...
      ]
    , suite "List Append"
      [ claim_append_same_list_doubles_length
      , claim_append_lists_adds_length
      , claim_append_reverse_flip_reverse_append
      , ...
      ]
    , ...  
    ]

You can then simply call check or quickCheck on the entire suite as opposed to an individual claim as follows:

result = quickCheck suite_list

DSL

The DSL was mentioned above but was not fully fleshed out. First of all, it is important to precise that the DSL provided by elm-check is strictly optional. The main function to make claims is claim and there are versions of this supporting multiple arities and you are most welcome to use them if you are not into DSLs (or just not into this one).

The DSL provided by elm-check is super simple and it is used to generate claims. This is how it looks:

claim_multiplication_division_inverse =
  claim
    "Multiplication and division are inverse operations"
  `that`
    (\(x, y) -> x * y / y)
  `is`
    (\(x, y) -> x)
  `for`
    tuple (float, float)

Without the DSL, this looks like:

claim_multiplication_division_inverse =
  claim
    "Multiplication and division are inverse operations"
    (\(x, y) -> x * y / y)
    (\(x, y) -> x)
    (tuple (float, float))

Simple, just remove those infix functions in the middle.

There are three flavors of these infix functions:

• claim - that - is - for
• claim - true - for
• claim - false - for

The last two are equivalent to using the claimTrue and claimFalse respectively. If we rewrote the example with claim-true-for, it would look like this:

claim_multiplication_division_inverse =
  claim
    "Multiplication and division are inverse operations"
  `true`
    (\(x, y) -> x * y / y == x)
  `for`
    tuple (float, float)

Which is exactly equivalent to:

claim_multiplication_division_inverse =
  claimTrue
    "Multiplication and division are inverse operations"
    (\(x, y) -> x * y / y == x)
    (tuple (float, float))

claim-false-for is exactly equivalent to claim-true-for but it flips the boolean.

An important thing to note about the DSL, these functions only work with claim. They don't even work with the multi-arity versions of claim. So, if you want to do have claims with multiple arguments, you have to use tuples directly. Functions like claim2 or claim3 use tuples behind the scenes, but the type system in Elm is such that I couldn't figure out how to introduce the DSL while still providing he ability to work with claims of arbitrary number of arguments. The examples above were picked purposefully to illustrate how this would be done.

Missing from previous versions

Continuous checking is gone from this version. If you are using it, don't worry, it is getting replaced with a newer, shinier Task-based version. The goal here is to provide a means to capture the progression of a run of elm-check by running checks in tasks and sending the result to mailboxes. This will make continuous checking way more responsive than the previous Signal-based version which tended to perform terribly if the functions you were testing happened to be computationally intensive. So, watch this space and expect the browser runner to be dramatically improved as this feature is supported.

Elm-test integration

Another big feature of the new version of elm-check is an integration with elm-test. Now, elm-check provides a way to generate elm-test unit tests and assertions directly and can be used completely transparently alongside elm-test. Due to slight differences on the priorities of elm-check and elm-test, you must use a separate submodule to generate elm-test unit tests. The API provided by the Check.Test submodule is very analogous to the one provided by the regular Check module and moving between the two is very easy.

The main difference here is that you cannot use the types Claim and Evidence in Check.Test. Instead, you directly generate Test results as in elm-test.

Check.Test is centered around a single function called test.

test : String -> (a -> b) -> (a -> b) -> Investigator a -> Int -> Seed -> Test

test is basically what would happen if you slammed check and claim together. Given a name for the test, an actual statement, an expected statement, an investigator, n number of checks, and a random seed, test will generate n many unit tests using random generation. Furthermore, test will add in an extra minimal failing unit test in the case on of the assertions fail. Basically, test generates a suite of unit tests focused around a single property of your system. This means that you get both the ability to generate arbitrarily many unit tests, but also the ability to shrink these unit tests.

Think of Check.Test as a module dedicated to authoring elm-test unit tests. Since this process is separate from the rest of elm-check, these unit tests run in the elm-test runners without a problem and can be merged in with regular elm-test assertions into suites to your liking.

Note that the DSL doesn't work here unfortunately. The DSL is specifically made to work for claims whereas the idea here is mainly to provide compatibility with elm-test. Instead of stating claims about a system, the focus here is placed in generating tests (as you might be able to tell from the differently-named functions).

Finally Check.Test also provides an assert function which is analogous to claimTrue in Check:

assert : String -> (a -> Bool) -> Investigator a -> Int -> Seed -> Test

as well as multi-arity versions of both test and assert.