从类型方案构造表达式

Question

所以我被要求找到以下类型的表达式：

(int -> ((int -> (bool -> int)) -> (bool -> int)))

所以我构造了以下代码来生成（bool -> int）但是这是困扰我的组合：

(%which (T)
        (%typing '(lambda (f)
                    (lambda (x)
                      (succ (f (not x)))))
                 T))

谁能告诉我有什么好的规则或方法？:)

Answer 1

就个人而言，我认为当您从类型中删除多余的括号时（就像非程序员会写的那样）时，它会变得更加明显：

int -> (int -> bool -> int) -> bool -> int

所以你应该写一个函数，它被赋予三个参数并返回一个int。也就是说，解决方案必须以以下形式表示：

lambda n. lambda f. lambda b. ____

但是你如何填补这个洞呢？好吧，看看您从参数中获得的类型，很容易看出您可以通过将f应用于n并b将它们插入在一起，从而产生int。所以：

lambda n. lambda f. lambda b. f n b

这是一个解决方案。但是仔细观察这个术语，人们会注意到最里面的λ实际上可以被eta减少，给出一个更简单的术语：

lambda n. lambda f. f n

但实际上，这个问题有点退化，因为返回一个 int 总是微不足道的。所以最简单的解决方案可能是：

lambda n. lambda f. lambda b. 0

得出解决方案的一般方案通常是通过对类型结构的简单归纳：如果你需要一个函数，那么写下一个lambda并递归地处理主体。如果您需要元组，请记下元组并递归地处理其组件。如果你需要一个基元类型，你可以选择一个常量。如果你需要一些你没有的东西（通常在多态的情况下），在范围内寻找一些函数参数，这些参数会给你这样的东西。如果该参数本身是一个函数，请尝试递归构造一个合适的参数。

Answer 2

有几个

工具可以从类型派生实现（通过 Curry/Howard 对应）。一个例子是Djinn。有一个介绍，展示了一般如何从类型生成术语。

你也许可以了解更多关于 Curry-Howard 的信息，并将类型到代码工具移植到 Scheme？

Answer 3

对于您问题的细节（而不是一般技术），以下是我的方法：

(int -> ((int -> (bool -> int)) -> (bool -> int)))可以简化为(A -> ((A -> B) -> B)) A = int和B = (bool -> int)。这个简化版本很容易构建：

(lambda (a)
  (lambda (f)
    (f a)))

很容易看出为什么这样做：a有类型 A，f有类型 (A -> B) ，所以调用 (f a) 将导致B。为了给这些变量具体化类型，a有类型 int ，f有类型 (int -> (bool -> int)) ，结果当然是 (bool -> int) 。

因此，现在您需要找到一个合适的函数，该函数具有 (int -> (bool -> int)) 类型以插入 f 参数。举个例子非常简单：

(lambda (n)
  (lambda (negate?)
    ((if negate? - +) n)))

以下是如何使用这些函数：

> (define (foo a)
    (lambda (f)
      (f a)))
> (define (bar n)
    (lambda (negate?)
      ((if negate? - +) n)))
> (define baz ((foo 42) bar))
> (baz #t)
-42
> (baz #f)
42

Answer 4

这是我搜索的解决方案：

（λ（i） （λ （f） （λ （b） （succ （（f （succ i）） （not b）

））））））

可以通过以下方式确认： （%其中 （T） （%键入 '（λ（i） （λ （f） （λ （b） （succ （（f （succ i）） （not b））））））） T））

Succ 确保它是一个整数而不是 --> bool。