Property Testing Generic Programs

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.

Advertisements