[Haskell-cafe] What is the state of the art in testing code generation?

Chris Warburton chriswarbo at googlemail.com
Tue Jul 15 12:15:24 UTC 2014

oleg at 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:


More information about the Haskell-Cafe mailing list