Documentation

Extrapolate can generalize counter-examples of any types that are Arguable.

Arguable types must first be instances of

• Listable, so Extrapolate knows how to enumerate values;
• Express, so Extrapolate can represent then manipulate values;
• Name, so Extrapolate knows how to name variables.

There are no required functions, so we can define instances with:

instance Arguable OurType

However, it is desirable to define both background and subInstances.

The following example shows a datatype and its instance:

data Stack a = Stack a (Stack a) | Empty

instance Arguable a => Arguable (Stack a) where
  subInstances s  =  instances (argTy1of1 s)

To declare instances it may be useful to use type binding operators such as: argTy1of1, argTy1of2 and argTy2of2.

Instances can be automatically derived using deriveArguable which will also automatically derivate Listable, Express and Name when needed.

Used in the definition of subInstances in Arguable typeclass instances.

A type is Listable when there exists a function that is able to list (ideally all of) its values.

Ideally, instances should be defined by a tiers function that returns a (potentially infinite) list of finite sub-lists (tiers): the first sub-list contains elements of size 0, the second sub-list contains elements of size 1 and so on. Size here is defined by the implementor of the type-class instance.

For algebraic data types, the general form for tiers is

tiers  =  cons<N> ConstructorA
       \/ cons<N> ConstructorB
       \/ ...
       \/ cons<N> ConstructorZ

where N is the number of arguments of each constructor A...Z.

Here is a datatype with 4 constructors and its listable instance:

data MyType  =  MyConsA
             |  MyConsB Int
             |  MyConsC Int Char
             |  MyConsD String

instance Listable MyType where
  tiers =  cons0 MyConsA
        \/ cons1 MyConsB
        \/ cons2 MyConsC
        \/ cons1 MyConsD

The instance for Hutton's Razor is given by:

data Expr  =  Val Int
           |  Add Expr Expr

instance Listable Expr where
  tiers  =  cons1 Val
         \/ cons2 Add

Instances can be alternatively defined by list. In this case, each sub-list in tiers is a singleton list (each succeeding element of list has +1 size).

The function deriveListable from Test.LeanCheck.Derive can automatically derive instances of this typeclass.

A Listable instance for functions is also available but is not exported by default. Import Test.LeanCheck.Function if you need to test higher-order properties.