DepTyCheck

A library for property-based testing with dependent types and automatic derivation of generators for Idris 2

Status

🚧 The library is under heavy construction 🚧

For now, it lacks most of things required for normal property-based testing, like support for properties and fancy testing operations. Also, for now we do not support such important thing as shrinking.

The current focus for now is on test data generators and automatic derivation of them.

Generators

Generators in the simplest case produce a bunch of values of appropriate type:

genSomeStrings : Gen NonEmpty String
genSomeStrings = elements ["one", "two", "three"]

You can combine several generators into one:

genMoreStrings : Gen NonEmpty String
genMoreStrings = oneOf [genSomeStrings, elements ["more", "even more"]]

Note

All generators listed in oneOf are meant to be distributed uniformly between each other as a whole thing. That is, in genMoreStrings values "one", "two" and "three" have the same probability to be generated and this probability is 2/3 of probability for "more" or "even more" to appear.

So, the following generator is not equivalent to the genMoreStrings from above:

genMoreStrings' : Gen NonEmpty String
genMoreStrings' = elements ["one", "two", "three", "more", "even more"]

In genMoreStrings' all values are distributed uniformly.

To achieve the same result with reusing genSomeStrings generator, we need to dig into it deeper with alternativesOf function:

genMoreStrings'' : Gen NonEmpty String
genMoreStrings'' = oneOf $ alternativesOf genMoreStrings ++ alternativesOf (elements ["more", "even more"])

Note

There are also functions based on the alternativesOf, allowing to map values from all alternatives in a single expression named mapAlternativesOf and mapAlternativesWith.

You can also operate with alternatives as with applicative functors or monads.

For example, consider a generator of lists with length not greater than given. There are a lot of possible implementations, but consider a recursive one:

genListsN : Gen NonEmpty a -> (n : Nat) -> Gen NonEmpty $ List a
genListsN _    Z     = [| [] |]
genListsN genA (S n) = oneOf $ [| [] |]
                            :: [| [genA] :: alternativesOf (genListsN genA n) |]

Distribution of lengths of lists produced by this generator is uniform, thanks to alternativesOf function.

Note

If we were not using alternativesOf at all (say, with expression [| genA :: genListsN genA n |]), probability of getting a list of length n+1 would be 2 times less than getting a list of length n.

Generators can be combined with operations from Applicative interface:

data X = MkX String String

genStrPairs : Gen NonEmpty X
genStrPairs = [| MkX genSomeStrings genMoreStrings |]

Note

The number of alternatives acquired by alternativesOf function of an applicative combination of two generators is a product of numbers of alternatives of those generators.

Unlike, say, in QuickCheck, generators can be empty. This is important for dependent types. For example, Fin 0 is not inhabited, thus we need to have an empty generator if we want to have a generator for any Fin n (and sometimes we really want):

genFin : (n : Nat) -> Gen MaybeEmpty $ Fin n
genFin Z     = empty
genFin (S n) = elements' $ allFins n

As you can see from examples above, there is a special marking of generator's emptiness in the first type argument of the Gen type.

Generators are also monads:

genAnyFin : Gen MaybeEmpty Nat => Gen MaybeEmpty (n ** Fin n)
genAnyFin @{genNat} = do
  n <- genNat
  f <- genFin n
  pure (n ** f)

Distribution of a generator built by monadic bind is such that the whole continuation (i.e. RHS of >>=) applied to some x has the same probability to produce the result as the probability for x to appear.

Thus, in the example above probability of particular natural n to come in the result is the same as probability of this n to come on the given genNat. After that, all fins for each particular n are distributed evenly, because it is a property of genFin.

You need to use alternativesOf if you want all possible resulted values to be distributed evenly, e.g.:

genAnyFin' : Gen MaybeEmpty Nat => Gen MaybeEmpty (n ** Fin n)
genAnyFin' @{genNat} = oneOf $ do
  n <- alternativesOf genNat
  f <- alternativesOf $ genFin n
  pure (n ** f)

Here we are using special monadic syntax support for lists of generators produced by alternativesOf function.

In the last example, all results of genFin 1 and all results of genFin 2 would not be distributed equally in the case when genNat is elements [1, 2], when they are distributed equally in the example of genAnyFin. I.e., particular generator's application genAnyFin @{elements [1, 2]} would be equivalent to oneOf [pure (1**0), elements [(2**0), (2**1)]] where genAnyFin' @{elements [1, 2]} would be equivalent to elements [(1**0), (2**0), (2**1)]. Thus, they have the same domain, but different distributions.

Despite monadic bind of generators interprets left-hand side generators as a whole, it looks inside it when the resulting generator is being asked for alternatives by alternativesOf function or its variants.

For example, alternativesOf being applied to genAnyFin @{elements [1, 2]} would produce two alternatives. Sometimes this can be undesirable, thus, a forgetAlternatives function exists. It allows to forget actual structure of a generator in terms of its alternatives.

Consider one more alternative of genAnyFin, now the given genNat is wrapped with forgetAlternatives:

genAnyFin'' : Gen MaybeEmpty Nat => Gen MaybeEmpty (n ** Fin n)
genAnyFin'' @{genNat} = do
  n <- forgetAlternatives genNat
  f <- genFin n
  pure (n ** f)

In this case, alternativesOf being applied to genAnyFin'' @{elements [1, 2]} would return a single alternative.

Note

Search for alternatives through the series of monadic binds can go to the first generator that is produced with no alternatives.

Consider three generators:

• do { e1 <- elements [a, b, c]; e2 <- elements [d, e, f]; pure (e1, e2) }
• do { e1 <- elements [a, b, c]; e2 <- forgetAlternatives $ elements [d, e, f]; pure (e1, e2) }
• do { e1 <- forgetAlternatives $ elements [a, b, c]; e2 <- elements [d, e, f]; pure (e1, e2) }

The first two generators would have three alternatives each when inspected by alternativesOf, where the third one would have only one.

But if you do alternativesOf for each of generators returned by the first alternativesOf and concatenate the results, the first example would give you nine alternatives, where the second one still would give you three. You can use deepAlternativesOf function with depth argument of 2 for this.

This, actually, violates monadic laws in some sense. Say, alternativesOf can distinct between pure x >>= f and f x if generator f x is, say, of form elements [a, b, c], because in the first case it would produce a single alternative, when in the second there will be three of them. However, according to the generated result these two generators shall be equivalent.

Note

Please notice that deepAlternativesOf can "see" through forgetAlternatives, so count of deep alternatives of depth 2 for the third case would still be 3. If you really need to hide the full structure even from the deepAlternativesOf, you can be much stronger version called forgetStructure:

• do { e1 <- forgetStructure $ elements [a, b, c]; e2 <- elements [d, e, f]; pure (e1, e2) }

This this case both alternativesOf and even deepAlternativesOf would give you the single alternative. But please keep in mind that monadic composition of a generator with forgotten structure and some significantly empty generator function (like oneOf [g1, forgetStrcuture g2 >>= f]) may have unexpected distribution of values. Probability of values produced by the f related to the probability of values produced by g1 may be divided by the probability of the generator forgetStructure g2 >>= f to produce a non-empty value.

When you are using the weaker forgetAlternatives instead of forgetStructure, distributions are more predictable in case when g2 has some non-trivial structure of alternatives.

Also, here you can see that we can use generators as auto-parameters, thus no need in a separate thing like QuickCheck's Arbitrary.

You can also see that having a dependent type to generate, we can consider different ratio between given and generated type arguments. Technically speaking, Fin n and (n ** Fin n) are different types, but pragmatically, genFin and genAnyFin both generate elements of type Fin n, but the first one takes n as a given value, and the second one generates value for the type argument along with the main value.

You can read more on the design of generators in documentation.

Derivation of generators

DepTyCheck supports automatic derivation of generators using the datatype definition.

For now, it is not tunable at all, however, it is planned to be added.

Derived generators are total. Since for now generators are finite, it was decided to use explicit fuel pattern to support recursive data types. For simplicity, fuel pattern is used for all derived generators.

To invoke derivation, we use deriveGen macro:

genNat : Fuel -> Gen MaybeEmpty Nat
genNat = deriveGen

It uses very powerful metaprogramming facility of Idris 2 programming language for analysing the data structure which generator is derived for and producing code of the asked generator at compile time. This facility is called elaborator reflection, and you can find some kind of tutorial for this here. To enable it, you have to add %language ElabReflection to the source code before the first call to the macro.

However, beware of possible high resources consumption of this stage. In our non-trivial examples, derivation may take several hours and tens of gigabytes of memory. We work for improvements of this, however we hope that new core of the Idris compiler would solve this issue completely.

Of course, we do not support all possible dependent types. For example, for now, we do not support type-polymorphic types and GADTs which have function calls in type indices of their constructors. However, we are constantly working for widening supported types.

Note

For now, derivation is supported only for MaybeEmpty generators.

More on design of derivator can be found in documentation.

Usage and installation

For building and testing we use pack package manager.

Note

Notice, that we've gone mad as far as possible, so even calling for makefile of Sphinx for building documentation is done through pack and prebuild action inside an appropriate ipkg file.

Despite that, to make LSP working well, only a single code-related ipkg file is left in the top-level folder of the project.

The main pack's collection we test the library against is the one mentioned in the last section of the library version. Also, we test against the latest pack collection nightly. Here is the status of the latest such run: . We try to use as fresh version of the Idris 2 compiler and thirdparty libraries as possible.