从文法中生成随机术语（简单类型的 lambda 演算）

Question

我有以下语法表示 Haskell 中的简单类型 lambda 演算 (STLC)。我在文献中看到了很多关于如何生成随机 lambda 项的论文，但想知道 Haskell 中是否有任何库可以从下面的语法生成随机实例？我有兴趣只生成一次程序。

我看到了一个名为 QuickCheck 的库，但它可以用于此目的吗？

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)

我的第二个问题是，我知道有许多基准可用于 Java 和 Python 等语言，但我尝试为 lambda 演算寻找类似的东西，但找不到任何东西。 STLC 或无类型 lambda 演算的基准是否可用？

Answer 1

我真的不知道有哪个库可以重复使用。该库可能还会将您锁定在绑定结构的特定方法中，例如 De Bruijn、Names、(P)HOAS 或 bound.

但是我知道 Haskell 中的一个实现会随机生成紧密、类型正确的术语：https://github.com/Gabriel439/Haskell-Morte-Library/blob/3c61df86985a7ccf97fe0765deac73f06b12c476/test/ClosedWellTyped.hs#L38

也许这足以让你滚动？

Answer 2

是的，QuickCheck 库就是您所需要的。

首先我假设 Name 是 String 的类型同义词？当然，在 STLC 中生成 lambda 项会带来一个特殊的问题。 Quickcheck 允许您在 Gen Monad 中生成术语，允许组合生成术语。类型的默认 Gen 可以通过创建类型类 Arbitrary 的所述类型实例来声明。也就是说，一旦你有了一个嵌套类型的生成器，你就可以用它来创建一个使用它的值构造函数的生成器。

举个例子，我们可以为 lambda 抽象编写一个生成器，它接受名为 x 或 y 的 Tint 类型的参数并返回一个布尔值（假设您已经编写了一个生成器 boolExpr ) 如:

intLambda :: Gen Expr
intLambda = Lam Tint <$> elements ["x","y"] <*> (boolExpr :: Gen Expr)

（注意我使用的是 Applicative Notation，在这个 Monad 中通常更优雅。）

Gen 模块的 the hackage documentation 是一个不错的起点。许多QuickChecks模块是专门用于执行测试的，这似乎不是您主要关心的问题。

从文法中生成随机术语（简单类型的 lambda 演算）

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

haskell

lambda-calculus

quickcheck