两次球拍合同依赖性评估？答案

【问题标题】：racket contract dependency evaluation twice?两次球拍合同依赖性评估？
【发布时间】：2016-12-14 13:54:31
【问题描述】：

#lang racket

(module inside racket
  (provide
    (contract-out
      [dummy (->i ([x       (lambda (x) (begin (displayln 0) #t))]
                   [y (x)   (lambda (y) (begin (displayln 1) #t))]
                   [z (x y) (lambda (z) (begin (displayln 2) #t))]
                   )
                  any
                  )]
      )
    )

  (define (dummy x y z) #t)
  )

(require 'inside)

(dummy 1 2 3)

输出是

我不清楚为什么将 x 和 y 作为依赖项需要相应的防护再次触发。

->ihttp://docs.racket-lang.org/reference/function-contracts.html#%28form._%28%28lib.racket%2Fcontract%2Fbase..rkt%29.-~3ei%29%29 的文档似乎没有提到这种行为。

任何人都可以对此有所了解吗？

【问题讨论】：

标签： racket contract

【解决方案1】：

这让我和你一样困惑，所以我借此机会ask this question on the Racket mailing list。下面是对我发现的内容进行总结的尝试。

->i 组合器生成一个依赖合约，该合约使用论文Correct Blame for Contracts 中提出的indy blame 语义。论文中提出的关键思想是，对于依赖合同，实际上可能有三个方可能需要因违反合同而受到指责。

对于正常功能合同，有两个潜在的有罪方。第一个是最明显的，就是调用者。例如：

> (define/contract (foo x)
    (integer? . -> . string?)
    (number->string x))
> (foo "hello")
foo: contract violation
  expected: integer?
  given: "hello"
  in: the 1st argument of
      (-> integer? string?)
  contract from: (function foo)
  blaming: anonymous-module
   (assuming the contract is correct)

第二个潜在的罪魁祸首是函数本身；也就是说，实现可能与合同不匹配：

> (define/contract (bar x)
    (integer? . -> . string?)
    x)
> (bar 1)
bar: broke its own contract
  promised: string?
  produced: 1
  in: the range of
      (-> integer? string?)
  contract from: (function bar)
  blaming: (function bar)
   (assuming the contract is correct)

这两种情况都很明显。然而，->i 合约引入了第三个潜在的犯罪方：合约本身。

由于->i 合约可以在合约附加时执行任意表达式，因此它们可能会违反自身。考虑以下合同：

(->i ([mk-ctc (integer? . -> . contract?)])
      [val (mk-ctc) (mk-ctc "hello")])
     [result any/c])

这是一个有点傻的合同，但很容易看出它是一个顽皮的合同。它承诺只用整数调用mk-ctc，但依赖表达式(mk-ctc "hello") 用字符串调用它！归咎于调用函数显然是错误的，因为它无法控制无效的合约，但归咎于合约函数可能也是错误的，因为合约可以在完全隔离的情况下定义它所附加的功能。

为了说明这一点，请考虑一个多模块示例：

#lang racket

(module m1 racket
  (provide ctc)
  (define ctc
    (->i ([f (integer? . -> . integer?)]
          [v (f) (λ (v) (> (f v) 0))])
         [result any/c])))

(module m2 racket
  (require (submod ".." m1))
  (provide (contract-out [foo ctc]))
  (define (foo f v)
    (f #f)))

(require 'm2)

在此示例中，ctc 合约定义在 m1 子模块中，但使用该合约的函数定义在单独的子模块 m2 中。这里有两种可能的责备场景：

foo 函数显然无效，因为它将f 应用于#f，尽管合约为该参数指定了(integer? . -> . integer?)。您可以通过调用foo 来在实践中看到这一点：
```
> (foo add1 0)
foo：违反了自己的合同
  承诺：整数？
  制作：#f
  在：的第一个论点
      的 f 论点
      (->我
       （（f（->整数？整数？））
        (v (f) (λ (v) (> (f v) 0))))
       （结果任何/c））
  合同来自：（匿名模块 m2）
  责备：（匿名模块 m2）
   （假设合同正确）
```
我已经强调了合同错误中包含责备信息的地方，你可以看到它归咎于m2，这是有道理的。这不是一个有趣的案例，因为它是非依赖案例中提到的第二个潜在责任方。
然而，ctc 合约实际上有点错误！请注意v 上的合约将f 应用于v，但它从不检查v 是否为整数。出于这个原因，如果v 是别的东西，f 将以无效的方式被调用。¹您可以通过为v 提供非整数值来查看此行为：
```
> (foo add1 "你好")
foo：违反了自己的合同
  承诺：整数？
  产生：“你好”
  在：的第一个论点
      的 f 论点
      (->我
       （（f（->整数？整数？））
        (v (f) (λ (v) (> (f v) 0))))
       （结果任何/c））
  合同来自：（匿名模块 m1）
  责备：（匿名模块 m1）
   （假设合同正确）
```
上面的合约错误是一样的（Racket 对这些违反合约的行为提供相同的“破坏自己的合约”消息），但责备信息不同！它现在责备m1，这是合同的实际来源。这是indy责备方。

这种区别意味着合同必须应用两次。它将它们与每个不同的责任方的信息一起应用：首先将它们与合同责任一起应用，然后将它们与功能责任一起应用。

从技术上讲，对于固定合同可以避免这种情况，因为在初始合同附加过程之后，固定合同永远不会发出违反合同的信号。但是，->i 组合器目前没有实现任何此类优化，因为它可能不会对性能产生重大影响，并且合约实现已经相当复杂（尽管如果有人想实现它，它可能会被接受)。

不过，一般来说，合约应该是无状态的和幂等的（平面合约应该是简单的谓词），所以并不能保证这不会发生，@987654351 @ 只是使用它来实现其细粒度的责备信息。

^{1.事实证明，->d 合约组合器根本没有发现这个问题，所以add1 最终在这里引发了合约违规。这就是创建->i 的原因，也是为什么->i 比->d 更受青睐的原因。}

【讨论】：