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