I have the following grammar representing the simply typed lambda calculus (STLC) in Haskell. I saw a lot of papers in the literature about how to generate random lambda terms but was wondering if there are any libraries in Haskell that can generate random instances from the grammar below? I am interested in generating the programs only once.
I saw a library called QuickCheck but can this be used for this purpose?
data Vtype = Tint
| Tbool
| Tfun Vtype Vtype
deriving (Eq, Data)
data Expr = Vi Int
| Vb Bool
| Vv Name
| App Expr Expr
| Lam Vtype Name Expr
deriving (Eq, Data)
My second question is, I know there are many benchmarks available for languages like Java and Python, but I tried looking for something like that for the lambda calculus and could not find anything. Is there any chance benchmarks for STLC or the untyped lambda calculus are available?
Yes, the QuickCheck library is what you need.
First I assume that Name is a type synonym for String?
Of course generating lambda terms in the STLC poses a particular problem.
Quickcheck lets you generate terms in the Gen Monad, allowing for compositional generation of terms. Default Gens for a Type can be declared by making said type instance of the typeclass Arbitrary. That is, once you have a generator of a nested type, you can use it to create a generator of a value constructor using it.
To give you an example, we could write a generator for a lambda abstraction taking a parameter of type Tint named x or y and returning a Bool (assuming you have written a generator boolExpr) as:
intLambda :: Gen Expr
intLambda = Lam Tint <$> elements ["x","y"] <*> (boolExpr :: Gen Expr)
(Note I am using Applicative Notation, which is often more elegant in this Monad.)
A good place to get started is the hackage documentation for the Gen module. A lot of QuickChecks modules are especially for executing the tests, which it seems is not your primary concern.