One of the interesting challenges when dealing with generic programming is testing. How could you possibly achieve extensive test coverage for a piece of code that works with arbitrary types? Suppose for instance that we have implemented a generic equality function:
val equals : 'T -> 'T -> bool
One of the properties we would expect this function to satisfy is reflexivity.
Put formally, the predicate
let reflexivity (t:'T) = equals t t
should return true for any value of any type.
The Standard Approach
Using a random testing tool like FsCheck, a common strategy to validate this would unfold as follows:
[<Property>] let ``Int Reflexivity`` (x : int) = reflexivity x [<Property>] let ``String Reflexivity`` (x : string) = reflexivity x [<Property>] let ``2-Tuple Reflexivity`` (x : string * int) = reflexivity x [<Property>] let ``List Reflexivity`` (x : (string * int) list) = reflexivity x [<Property>] let ``List of List Reflexivity`` (x : (string * int) list list) = reflexivity x ...
Expanding on tested types ad nauseam, until we finally convince ourselves that coverage is sufficient. But is it? How can we be sure that (string * int) list
correctness implies correctness for (int * string) list
? What about large tuple arities? We will always be forgetting something.
Generic Property Tests
I have been toying with the idea of generic property tests for quite a while now, but only the recent performance improvements in FsCheck 3 (currently in prerelease) have made this approach feasible. For starters, we will need to provide a rank-2 encoding for predicates:
type Predicate = abstract Invoke : 'T -> bool
Which permits declaration of generic predicate values (currently not a possibility with F# lambdas, which must be fixed on their argument types)
let reflexivity = { new Predicate with member __.Invoke t = equals t t }
The goal is to use FsCheck in a way where generic predicates can be tested against random values of random types.
Defining a Type Algebra
Let’s start by defining the kind of types we would like to be testing. To do this we define a type algebra, or a “type of types”:
type TypeAlg = | BaseType of BaseType | List of TypeAlg | Array of TypeAlg | Option of TypeAlg | Tuple of TypeAlg list and BaseType = Bool | Byte | Int | String
Each instance of type TypeAlg
represents an actual F# type. For instance, the value Tuple [BaseType Int; Option(BaseType String)]
represents the type int * string option
. As a first exercice, let’s try implementing a pretty-printer for the algebra:
let rec prettyprint ta = match ta with | BaseType Bool -> "bool" | BaseType Byte -> "byte" | BaseType Int -> "int" | BaseType String -> "string" | List element -> sprintf "(%s) list" (prettyprint element) | Array element -> sprintf "(%s) []" (prettyprint element) | Option element -> sprintf "(%s) option" (prettyprint element) | Tuple elements -> elements |> Seq.map prettyprint |> String.concat " * " |> sprintf "(%s)"
Importantly, it is possible to map any TypeAlg representation to its corresponding System.Type
runtime instance like so:
let rec meaning ta : System.Type = match ta with | BaseType Bool -> typeof<bool> | BaseType Byte -> typeof<byte> | BaseType Int -> typeof<int> | BaseType String -> typeof<string> | List element -> typedefof<_ list>.MakeGenericType(meaning element) | Array element -> (meaning element).MakeArrayType() | Option element -> typedefof<_ option>.MakeGenericType(meaning element) | Tuple [] -> typeof<unit> | Tuple elements -> elements |> Seq.map meaning |> Seq.toArray |> FSharp.Reflection.FSharpType.MakeTupleType
We can use TypeShape to take that semantic mapping one step further: bring the type into scope as a generic argument.
open TypeShape.Core let visitTAlg (visitor : ITypeShapeVisitor<'R>) (tAlg : TypeAlg) : 'R = let sysType : Type = meaning tAlg let shape : TypeShape = TypeShape.Create sysType shape.Accept visitor
We can verify the behaviour by running
let getType = { new ITypeShapeVisitor<System.Type> with member __.Visit<'T>() = typeof<'T> } |> visitTAlg getType (BaseType Int) // typeof<int> getType (Option (BaseType (String)) // typeof<string option>
Putting it all Together
Let’s now see how we can use this technique to obtain a random tester for generic predicates. Consider the following function:
open FsCheck let checkTAlg (predicate : Predicate) (tAlg : TypeAlg) : bool = printfn "Testing %s" (prettyprint tAlg) let checker = { new ITypeShapeVisitor<bool> with member __.Visit<'T>() = Check.QuickThrowOnFailure<'T -> bool> predicate.Invoke true } visitTAlg checker tAlg
The implementation accepts a generic predicate and a type representation, uses TypeShape to bring the type into scope as a type variable, then calls FsCheck with the predicate instantiated to the reified type.
The key observation for converting this function into a generic property test is that TypeAlg
is an algebraic data type, and FsCheck is capable of generating random instances for type out of the box:
let checkGeneric (predicate : Predicate) = Check.QuickThrowOnFailure<TypeAlg -> bool>(checkTAlg predicate)
We are now ready to random test our reflexivity
property:
checkGeneric reflexivity
which yields the following output:
Testing (bool) [] Ok, passed 100 tests. Testing byte Ok, passed 100 tests. Testing ((bool) option) list Ok, passed 100 tests. Testing bool Ok, passed 100 tests. Testing (string * byte) Ok, passed 100 tests. Testing ((string) option) option Ok, passed 100 tests. Testing ((bool * ((((((()) []) []) option) option) list) [] * byte * int * string * string * int * bool * int * int * int * byte)) option Ok, passed 100 tests. ...
In effect this call will test 100 randomly generated types with 100 randomly generated values each.
Conclusions
Applying the above technique when testing generic programs code has proven to be extremely effective. It has allowed me to discover both implementation bugs of the generic programs themselves, as well as obscure bugs of the core TypeShape library. My previous, handwritten test suite had failed to catch any of those issues. If interested, have a look at this source file for an example of a more complete implementation of the technique.
A few of the code samples run off the margin – the Predicate object expression is a bit difficult due to this, since it requires scrolling but is only one line. Could you break the lines up a bit so that scrolling isn’t required?
Love the article. Really interesting technique.
Thanks for the feedback. I changed the indentation, hope it looks better now.
I cloned your work to use Check.Generic only, and found the performance with FsCheck 2.x satisfactory. Great work.
Interesting, the issue seems to have been fixed since 2.10
https://github.com/fscheck/FsCheck/issues/309