CODEWITHSUNDEEP
haskelllambda-calculusquickcheck
Lana
Lana

Reputation: 1304

Generating random terms from a grammar (simply typed lambda calculus)

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?

Upvotes: 1

Views: 301

Answers (2)

cxandru
cxandru

Reputation: 158

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.

Upvotes: 1

Sebastian Graf
Sebastian Graf

Reputation: 3740

I don't really know of a library you could re-use. That library would probably also lock you in on a particular approach to binding constructs, like De Bruijn, Names, (P)HOAS or bound.

I however know of an implementation in Haskell that does generate close, well-typed terms randomly: https://github.com/Gabriel439/Haskell-Morte-Library/blob/3c61df86985a7ccf97fe0765deac73f06b12c476/test/ClosedWellTyped.hs#L38

Maybe this is enough to get you rolling?

Upvotes: 2

Related Questions