2

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

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

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

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

谁能告诉我任何好的规则或方法？:)

4

4 回答 4

1

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

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

所以你应该写一个给定三个参数并返回一个int. 也就是说，解决方案必须可以用以下形式表示：

lambda n. lambda f. lambda b. ____

但是你如何填补这个洞？好吧，看看你从参数中得到什么类型，很容易看出你可以通过应用and将它们连接f在一起，产生一个. 所以：nbint

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

这是一种解决方案。但是仔细观察这个术语会发现，最里面的 lambda 实际上可以被 eta-reduced，给出一个更简单的术语：

lambda n. lambda f. f n

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

lambda n. lambda f. lambda b. 0

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

于 2012-05-26T16:34:25.860 回答
0

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

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

于 2012-05-26T13:26:47.640 回答
0

对于您的问题的具体细节（而不是一般技术），我可能会这样做：

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

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

很容易看出为什么会这样：a有 typeA和fhas type (A -> B)，所以调用(f a)会导致B. 要将具体类型赋予这些变量，ahas type int，fhas type (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
于 2012-05-26T14:32:24.507 回答
0

这是我搜索的解决方案：

(lambda (i) (lambda (f) (lambda (b) (succ ((f (succ i)) (not b))))))

可以通过以下方式确认： (%which (T) (%typing '(lambda (i) (lambda (f) (lambda (b) (succ ((f (succ i)) (not b)))))) T))

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

于 2012-05-27T08:36:28.407 回答