oleg@okmij.org writes:
One should generate well-typed terms from the beginning, without any rejections. That is actually not difficult: one merely needs to take the type checker (which one has to write anyway) and run it backwards.
In the ideal case, this can be done automatically, eg. see the first "Sample application" on http://kanren.sourceforge.net/ In general, the more information we throw away, the "less reversible" it becomes, and hence the more code we need to support going backwards.
Perhaps it is not as simple as I made it sound, depending on the type system (for example, the type inference for simply-typed lambda-calculus without any annotations requires guessing. One has to guess correctly all the type, otherwise the process becomes slow).
We don't need to guess if we generate the terms and the types at the same time; we just have to plug them into the right positions, which may be a little tedious compared to just writing "arbitrary".
Also, I don't know your type system.
That's what put me off replying originally. The richer the types, the more difficult it will be to generate terms for them. Choosing between Ints, Strings, Bools, etc. and simple collections thereof is pretty trivial. Finding an inhabitant of some huge auto-generated type containing predicates, constraints, relations, etc. requires a theorem-prover ;) Also related, on the subject of generating typed terms: http://research.microsoft.com/en-us/people/dimitris/every-bit-counts.pdf Cheers, Chris