Given the number of patterns to show, shows a ShowFunction value.

> putStrLn $ showFunction undefined True
True

> putStrLn $ showFunction 3 (id::Int->Int)
\x -> case x of
      0 -> 0
      1 -> 1
      -1 -> -1
      ...

> putStrLn $ showFunction 4 (&&)
\x y -> case (x,y) of
        (True,True) -> True
        _ -> False

In the examples above, "..." should be interpreted literally.

This can be used as an implementation of show for functions:

instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
  show  =  showFunction 8

See showFunctionLine for an alternative without line breaks.

Same as showFunction, but has no line breaks.

> putStrLn $ showFunctionLine 3 (id::Int->Int)
\x -> case x of 0 -> 0; 1 -> 1; -1 -> -1; ...
> putStrLn $ showFunctionLine 3 (&&)
\x y -> case (x,y) of (True,True) -> True; _ -> False

This can be used as an implementation of show for functions:

instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
  show  =  showFunction 8

ShowFunction values are those for which we can return a list of functional bindings.

Instances for showable algebraic datatypes are defined using bindtiersShow:

instance ShowFunction Ty where bindtiers  =  bindtiersShow

A drop-in implementation of bindtiers for showable types.

Define instances for showable algebraic datatypes as:

instance ShowFunction Ty where bindtiers  =  bindtiersShow

A functional binding in a showable format. Argument values are represented as a list of strings. The result value is represented by Just a String when defined or by Nothing when undefined.

Given a ShowFunction value, return a list of Bindings. If the domain of the given argument function is infinite, the resulting list is infinite.

Some examples follow. These are used as running examples in the definition of explainedBindings, describedBindings and clarifiedBindings.

• Defined return values are represented as Just Strings:

  > bindings True
  [([],Just "True")]

• Undefined return values are represented as Nothing:

  > bindings undefined
  [([],Nothing)]

• Infinite domains result in an infinite bindings list:

  > bindings (id::Int->Int)
  [ (["0"], Just "0")
  , (["1"], Just "1")
  , (["-1"], Just "-1")
  , ...
  ]

• Finite domains result in a finite bindings list:

  > bindings (&&)
  [ (["False","False"], Just "False")
  , (["False","True"], Just "False")
  , (["True","False"], Just "False")
  , (["True","True"], Just "True")
  ]

  > bindings (||)
  [ (["False","False"], Just "False")
  , (["False","True"], Just "True")
  , (["True","False"], Just "True")
  , (["True","True"], Just "True")
  ]

• Even very simple functions are represented by an infinite list of bindings:

  > bindings (== 0)
  [ (["0"], Just "True")
  , (["1"], Just "False")
  , (["-1"], Just "False")
  , ...
  ]

  > bindings (== 1)
  [ (["0"], Just "False")
  , (["1"], Just "True")
  , (["-1"], Just "False")
  , ...
  ]

• Ignored arguments are still listed:

  > bindings ((\_ y -> y == 1) :: Int -> Int -> Bool)
  [ (["0","0"], Just "False")
  , (["0","1"], Just "True")
  , (["1","0"], Just "False")
  , ...
  ]

• Again, undefined values are represented as Nothing. Here, the head of an empty list is undefined:

  > bindings (head :: [Int] -> Int)
  [ (["[]"], Nothing)
  , (["[0]"], Just "0")
  , (["[0,0]"], Just "0")
  , (["[1]"], Just "1")
  , ...
  ]

Returns a set of bindings explaining how a function works. Some argument values are generalized to "_" when possible. It takes as argument the maximum number of cases considered for computing the explanation.

A measure of success in this generalization process is if this function returns less values than the asked maximum number of cases.

This is the first function in the clarification pipeline.

• In some cases, bindings cannot be "explained" an almost unchanged result of bindings is returned with the last binding having variables replaced by "_":

  > explainedBindings 4 (id::Int->Int)
  [ (["0"],Just "0")
  , (["1"],Just "1")
  , (["-1"],Just "-1")
  , (["_"],Just "2") ]

• When possible, some cases are generalized using _:

  > explainedBindings 10 (||)
  [ (["False","False"],Just "False")
  , (["_","_"],Just "True") ]

  but the resulting "explanation" might not be the shortest possible (cf. describedBindings):

  > explainedBindings 10 (&&)
  [ ( ["False","_"],Just "False")
  , (["_","False"],Just "False")
  , (["_","_"],Just "True") ]

• Generalization works for infinite domains (heuristically):

  > explainedBindings 10 (==0)
  [ (["0"],Just "True")
  , (["_"],Just "False") ]

• Generalization for each item is processed in the order they are generated by bindings hence explanations are not always the shortest possible (cf. describedBindings). In the following examples, the first case is redundant.

  > explainedBindings 10 (==1)
  [ (["0"],Just "False")
  , (["1"],Just "True"),
  , (["_"],Just "False") ]

  > explainedBindings 10 (\_ y -> y == 1)
  [ (["_","0"],Just "False")
  , (["_","1"],Just "True")
  , (["_","_"],Just "False") ]

Returns a set of bindings describing how a function works. Some argument values are generalized to "_" when possible. It takes two integer arguments:

1. m: the maximum number of cases considered for computing description;
2. n: the maximum number of cases in the actual description.

As a general rule of thumb, set m=n*n+1.

This is the second function in the clarification pipeline.

This function processes the result of explainedBindings to sometimes return shorter descriptions. It chooses the shortest of the following (in order):

• regular unexplained-undescribed bindings;
• regular explainedBindings;
• explainedBindings with least occurring cases generalized first;

Here are some examples:

• Sometimes the result is the same as explainedBindings:

  > describedBindings 100 10 (||)
  [ (["False","False"],Just "False")
  , (["_","_"],Just "True") ]

  > describedBindings 100 10 (==0)
  [ (["0"],Just "True")
  , (["_"],Just "False") ]

• but sometimes it is shorter because we consider generalizing least occurring cases first:

  > describedBindings 100 10 (&&)
  [ ( ["True","True"],Just "True")
  , ( ["_","_"],Just "False") ]

  > describedBindings 100 10 (==1)
  [ (["1"],Just "True"),
  , (["_"],Just "False") ]

  > describedBindings 100 10 (\_ y -> y == 1)
  [ (["_","1"],Just "True")
  , (["_","_"],Just "False") ]

Returns a set of variables and a set of bindings describing how a function works.

Some argument values are generalized to "_" when possible. If one of the function arguments is not used altogether, it is ommited in the set of bindings and appears as "_" in the variables list.

This is the last function in the clarification pipeline.

It takes two integer arguments:

1. m: the maximum number of cases considered for computing the description;
2. n: the maximum number of cases in the actual description.

As a general rule of thumb, set m=n*n+1.

Some examples follow:

• When all arguments are used, the result is the same as describedBindings:

  > clarifiedBindings 100 10 (==1)
  ( ["x"], [ (["1"],Just "True"),
           , (["_"],Just "False") ] )

• When some arguments are unused, they are omitted in the list of bindings and appear as "_" in the list of variables.

  > clarifiedBindings 100 10 (\_ y -> y == 1)
  ( ["_", "y"], [ (["1"],Just "True")
                , (["_"],Just "False") ] )

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.