从语法生成随机项（简单类型的 lambda 演算）答案

【问题标题】：Generating random terms from a grammar (simply typed lambda calculus)从语法生成随机项（简单类型的 lambda 演算）
【发布时间】：2019-09-18 04:14:54
【问题描述】：

我有以下语法表示 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 演算的机会基准？

【问题讨论】：

是的，有用于此目的的库hackage.haskell.org/package/generic-random 不过，您可能需要先学习如何使用 QuickCheck 或其他一些随机库。
你想只生成类型良好的术语，还是垃圾也可以？
理想的类型良好的术语，但即使不是，我也可以使用任何随机术语，然后用我的类型检查器过滤它们
您可以使用fair backtracking monad 进行操作。几年前我写了一个blog post。
并不是说他的语言包含Lam，一个绑定结构。

标签： haskell lambda-calculus quickcheck

【解决方案1】：

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

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

也许这足以让你滚动？

【讨论】：

【解决方案2】：

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

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

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

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

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

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

【讨论】：

请注意，这不会产生语义正确的程序。结果，生成的生成器将非常缓慢地生成非平凡的 lambda 项。此外，在隐藏复杂性所在方面也有点误导：提出["x", "y"] 是这里的难点，并且取决于boolExpr 的结果以进行任何合理的实施。
@SebastianGraf 这就是为什么我说在 STLC 中生成 lambda 项会带来特殊问题。我给出了一个相当虚假的例子，只是为了展示图书馆的能力。我绝对同意编写一个好的生成器很难，但这需要 OP 来解决。