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