The idea, as far as I understand it, is to generate a list of mappings from a to b, and convert that list to a function.
There are a bunch of functions to change these: map works as usual, to change the b into c, but we can also have coMap (profunctor?) that works on the input instead of on the output: given a z -> a function, it changes a -> b to z -> b.
The simplest generated functions map all values to some default value, and more complicated functions have exceptions from the default (ie. "map 9 to 1, map everything else to 0"). Such functions with exceptions do shrink towards the "no exception" case (a constant function).
A classic poster child example of "hey we can generate functions" in the PBT context is testing that map f (filter p xs) == filter p (map f xs). (This is not true.)
The idea, as far as I understand it, is to generate a list of mappings from
a
tob
, and convert that list to a function.There are a bunch of functions to change these: map works as usual, to change the
b
intoc
, but we can also havecoMap
(profunctor?) that works on the input instead of on the output: given az -> a
function, it changesa -> b
toz -> b
.The simplest generated functions map all values to some default value, and more complicated functions have exceptions from the default (ie. "map 9 to 1, map everything else to 0"). Such functions with exceptions do shrink towards the "no exception" case (a constant function).
Prior art:
A classic poster child example of "hey we can generate functions" in the PBT context is testing that
map f (filter p xs) == filter p (map f xs)
. (This is not true.)