球拍合同依賴性評估兩次？

#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

球拍合同依賴性評估兩次？

回答

相關問題