[Haskell-cafe] What is the state of the art in testing code generation?
oleg at okmij.org
oleg at okmij.org
Tue Jul 15 10:26:52 UTC 2014
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).
More information about the Haskell-Cafe
mailing list