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

#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的文档似乎没有提及此行为。

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

来源

2016-12-14 Albert Netymk

这和我一样对你感到困惑，所以我借此机会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子模块定义的，但是，使用合同的功能被在单独的定义子模块，。有两种可能的情景怪在这里：

的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合约实际上有点不对！请注意0上的合同适用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)
```
合同错误的顶部是相同的（球拍提供相同的“打破了自己的合同”的消息对这类合同违规），但是这些责任信息是不同的！现在责备m1，这是合同的实际来源。这是指责派对的indy。

这个区别是什么意思是合同必须应用两次。它将它们应用于每个明确责任方的信息：首先它将它们应用于合同责任，然后将它们应用于功能责任。

从技术上讲，对于平面合同，这是可以避免的，因为在初始合同附件处理后，平面合同永远不会发出违反合同的信号。然而，目前的组合器并没有实现任何这样的优化，因为它可能不会对性能产生重大影响，并且合同实现已经相当复杂（尽管如果有人想实施它，它可能会被接受）。

一般来说，虽然，合同预计是无状态的和幂（平合约预计将简单谓词），所以没有任何真正的保证，这不会发生，->i只是使用它来实现它的细粒度的责备信息。

^{1.事实证明，在->d合同组合子不抓住这个问题好，所以add1结束了在这里养违反合同。这就是为什么->i创建的原因，这就是为什么->i比->d更受青睐。}

来源

2016-12-16 19:14:16

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

回答

相关问题