racket - Racket 契约(Contract)依赖性评估两次？

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)

输出是

0
0
1
1
2
#t

我不清楚为什么将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中介绍的印地怪语义。本文中提出的关键思想是，对于从属合同，实际上可能有三方可能因违反合同而受到指责。

对于正常职能的合同，有两个可能有罪的当事方。第一个是最明显的一个，即调用方。例如：

> (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参数
（-> i
（（f（->整数？整数？））
（v（f）（λ（v）（>（f v）0））））
（结果任何/ c））
合同来自：（匿名模块m2）
怪：（匿名模块M2）
（假设合同是正确的）

我在合同错误中强调了包括责备信息的内容，您可以看到它是指责m2，这是有道理的。这不是一个有趣的案例，因为这是非独立案例中提到的第二个潜在的非议方。
但是，ctc合同实际上有点错误！请注意，v上的协定将f应用于v，但是它从不检查v是整数。因此，如果v是其他名称，则会以无效的方式调用f。1您可以通过为v提供非整数值来看到此行为：

>（foo add1“ hello”）
foo：违反了自己的合同
承诺：整数？
产生：“你好”
在：的第一个参数
的f参数
（-> i
（（f（->整数？整数？））
（v（f）（λ（v）（>（f v）0））））
（结果任何/ c））
合同来自：（匿名模块m1）
指责：（匿名模块M1）
（假设合同是正确的）

合同错误的顶部是相同的（对于这些类型的合同违规，Racket提供了相同的“打破自己的合同”消息），但是责任信息却不同！现在，它归咎于m1，这是合同的实际来源。这是印地怪聚会。


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

从技术上讲，这对于平板合同可以避免，因为在初始合同附加过程之后，平板合同永远不会表示违反合同。但是，->i组合器当前未实现任何此类优化，因为它可能不会对性能产生重大影响，并且合同的实现已经相当复杂（尽管如果有人想要实现它，则可能会被接受） ）。

但是，一般而言，合同应该是无状态的并且是幂等的（平合同应该是简单的谓词），因此实际上并不能保证不会发生这种情况，->i只是使用它来实现其细粒度怪信息。



1.事实证明，->d合同组合器根本无法解决此问题，因此add1最终在这里引发了合同违约。这就是创建->i的原因，也是为什么->i优于->d的原因。