What is the state of the art in testing code generation?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

What is the state of the art in testing code generation?

oleg-30

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: What is the state of the art in testing code generation?

Chris Warburton
[hidden email] 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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: What is the state of the art in testing code generation?

Tom Ellis
In reply to this post by oleg-30
On Tue, Jul 15, 2014 at 06:26:52AM -0400, [hidden email] 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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe