What is the state of the art in testing code generation?
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).
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
On Tue, Jul 15, 2014 at 06:26:52AM -0400, oleg@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
participants (3)
-
Chris Warburton -
oleg＠okmij.org -
Tom Ellis