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

[Tom Ellis]

On Tue, Jul 15, 2014 at 06:26:52AM -0400, oleg at okmij.org wrote:
> 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.

This is very cool!

> 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.

My type system is not especially complicated, so I imagine I will be able to
build terms of arbitrary type straightforwardly without resorting to
rejection sampling.

However, this is not my main concern with the type system.  I have an AST
only some of whose terms are well typed, but I have a Haskell "front end" to
this AST and using Haskell's type system I ensure that I only create
well-typed terms of the AST.

A fairly dumb example (not of my EDSL, but probably easier to understand
than mine) might be like the following:

    f :: Func MyInt MyBool
    g :: Func MyBool MyDouble
    compose :: Func b c -> Func a b -> Func a c
    g `compose` f :: Func MyInt MyDouble

and the last term would result in something like

    Lam "x" (Ap "g" (Ap "f" "x"))

It's Haskell-typed terms like 'g `compose` f' that I don't know how to
generate programatically, and the fact that they all have different types
seems to be the problem.

Tom