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

[oleg at okmij.org]

Tom Ellis wrote:
> The first impediment to using QuickCheck is that my EDSL is typed.  I don't
> know how to generate random terms in the presence of types.

First I should point out Magic Haskeller (which generates typed
(Haskell) terms and then accepts those that satisfy the given
input-output relationship).
        http://nautilus.cs.miyazaki-u.ac.jp/~skata/MagicHaskeller.html
It is MagicHaskeller on Hackage.

The most straightforward method is to generate random terms and filter
well-typed ones. This is usually a bad method since many or most
randomly generated terms will be ill-typed. 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. 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). It has been done, in a
mainstream functional language: OCaml. The code can be re-written for
Haskell using the tricks for non-determinism with sharing (the Share
monad). Due to many deadlines I cannot re-write myself, not until the
middle of the next week. Also, I don't know your type system.

If you are curious about the OCaml code, it can be found at
        http://okmij.org/ftp/kakuritu/type_inference.ml

The main function is

let rec typeof : gamma -> term -> tp = fun gamma exp ->
 match exp () with
  | I _    -> int
  | V name -> begin try List.assoc name gamma
                    with Not_found -> fail ()
              end
  | L (v,body) ->
      let targ = new_tvar() in
      let tbody = typeof ((v,targ) :: gamma) body in
      arr targ tbody
   | A (e1,e2) ->
       let tres = new_tvar() in
       tp_same (typeof gamma e1) (arr (typeof gamma e2) tres);
       tres

It can infer a type of a term (or fail if it is will-typed), it can
generate well-typed terms one-by-one, or it can generate all terms
of a particular structure (e.g., with two lambdas at the top) and/or
of a particular type or type shape (e.g., an arrow).