球拍合同依赖评估两次？

Question

#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 作为依赖项需要相应的守卫再次触发。

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

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

Answer 1

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

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

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

> (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: broke its own contract
  promised: integer?
  produced: #f
  in: the 1st argument of
      the f argument of
      (->i
       ((f (-> integer? integer?))
        (v (f) (λ (v) (> (f v) 0))))
       (result any/c))
  contract from: (anonymous-module m2)
  blaming: (anonymous-module m2)
   (assuming the contract is correct)
```
我已经强调了合同错误中包含责备信息的地方，你可以看到它责备m2，这是有道理的。这不是一个有趣的案例，因为它是非依赖案例中提到的第二个潜在的责任方。
不过，ctc契约其实有点不对劲！请注意，v 上的合约将 f 应用于 v，但它从不检查 v 是否为整数。出于这个原因，如果 v 是其他东西，f 将以无效的方式被调用。¹ 您可以通过给出一个非整数值来查看此行为v:
```
> (foo add1 "hello")
foo: broke its own contract
  promised: integer?
  produced: "hello"
  in: the 1st argument of
      the f argument of
      (->i
       ((f (-> integer? integer?))
        (v (f) (λ (v) (> (f v) 0))))
       (result any/c))
  contract from: (anonymous-module m1)
  blaming: (anonymous-module m1)
   (assuming the contract is correct)
```
上面的合约错误是一样的（Racket对这几种合约违规提供了同样的“break its own contract”信息），但是blame信息是不一样的！它现在指责 m1，这是合同的实际来源。这就是indy指责党

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

从技术上讲，这对于扁平合同来说是可以避免的，因为扁平合同在最初的合同附加过程之后永远不会发出违反合同的信号。然而，->i 组合子目前没有实现任何这样的优化，因为它可能不会对性能产生重大影响，并且合约实现已经相当复杂（尽管如果有人想实现它，它可能被接受）。

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

^{1.事实证明，->d 合约组合器根本没有捕捉到这个问题，所以 add1 最终在这里引发了合约违规。这就是创建 ->i 的原因，也是 ->i 优于 ->d 的原因。}

球拍合同依赖评估两次？

racket contract dependency evaluation twice?

contract

racket