generator for functions

[fredldh]

I was wondering if there is a good way to generate random members of inductive types whose constructor may contain arrows (like bind operator in Monad.) It may be helpful for generating random programs if there is a default generator for such types including functions.

[Lysxia]

The best solution for QuickChick is probably to imitate Haskell QuickCheck with a splittable PRNG. The missing piece is an actual implementation of a splittable PRNG that would go right here instead of abusing OCaml's stateful semantics. There's actually some code that's already written to generate functions (CoArbitrary.v) if we solve that.

I have a branch using pringo but I haven't had the time to figure out ocaml/coq packaging.

[liyishuai]

I read it as generating a random instance of type A -> B.
This can be derived from a default value B and a list of key-value pairs list (A * B), which we can already generate.
I am trying to implement it here (incomplete).

[Lysxia]

CoArbitrary is also meant to generate functions, with better coverage and performance than key-value pairs when the domain A is large.