Programming Languages: Application and Interpretation【譯16】

初翻： @MrMathematica

原文：PLAI 第二版

GitHub：PLAI-cn

GitBook：PLAI-cn

翻譯聲明見 Github 倉庫

16 動態地檢查程序中的不變數：契約

類型系統提供了豐富且有價值的表示程序不變數的方式。然而，它們也代表了一種重要的權衡，因為並非所有程序的非平凡屬性都可以被靜態驗證。【注釋】此外，即使某個屬性可以設計靜態方法解決，註解和計算複雜度的負擔也可能過大。因此，我們所關心的一些屬性不可避免地只能被忽略或在運行時解決。本章我們來討論運行時檢查不變數。

這是一個正式的定理，被稱為賴斯定理。

實際上，每種編程語言都包含某種形式的斷言機制，使程序員能夠編寫比語言的靜態類型系統允許的更豐富的屬性。在沒有靜態類型的語言中，這些屬性可能以簡單的類型斷言開始：例如，某個參數是否為數。然而，斷言語言通常是整個編程語言，因此任何謂詞都可以用作斷言：例如，某個加密包的實現可能希望確保某些參數通過素性測試，或者某個平衡二叉搜索樹可能想要確保其子樹確實是平衡且有序的。

16.1 以契約實現謂詞

因此很容易想到如何實現簡單的契約（contract）。【注釋】契約包含一個謂詞。它讀入一個值並將謂詞應用於該值。如果值能通過謂詞判斷，則契約原樣返回該值；否則，該契約會報告錯誤。其行為只能是返回原值或報錯：它不應以任何方式更改值。簡而言之，對於能通過謂詞的值，契約本身就是恆等函數。

下面我們將使用#lang plai語言，原因有兩個。首先，這更好地模擬了動態類型語言編程。其次，為了簡單起見，我們將契約寫成類型化的斷言，但是在靜態類型語言中，它們將由類型檢查器處理，使得我們無法看到運行時行為。從效果來看，「關閉」類型檢查器會更容易。然而，即使在靜態類型的世界裡，契約也是非常有意義的，因為它們增強了程序員可以表達的不變數。

我們使用如下函數編碼該本質：

(define (make-contract pred?) (lambda (val) (if (pred? val) val (blame "violation"))))(define (blame s) (error contract "~a" s))

契約的例子：

(define non-neg?-contract (make-contract (lambda (n) (and (number? n) (>= n 0)))))

（在靜態類型語言中，檢查number?當然是不必要的，因為它可以在類型系統中使用契約函數的方式靜態檢查！）假設我們要確保計算平方根時不會得到虛數；可以這麼寫

(define (real-sqrt-1 x) (sqrt (non-neg?-contract x)))

在很多語言中，斷言是寫作語句而不是表達式，所以另一種編寫方式是：

(define (real-sqrt-2 x) (begin (non-neg?-contract x) (sqrt x)))

（在某些情況下，這種形式更清晰，因為它在函數的開始部分清晰地聲明了參數的期望值。它還確保參數只被檢查一次。實際上，在某些語言中，契約可以寫入函數頭部中 ，從而改善介面給出的信息。）現在，如果將real-sqrt-1或real-sqrt-2應用於4，則它們產生2，但如果應用於-1，則會引發違反契約的錯誤。

16.2 標籤、類型和對值的觀測

到這裡我們已經重現了大多數語言中斷言系統的本質。還有什麼要討論的？我們先假設手上的語言不是靜態類型的。我們希望編寫的斷言至少要能重現傳統的類型不變數，甚至更多。前述的make-contract可以覆蓋所有標準類型的屬性，比如檢查數、字元串等等，假設語言提供了合適的謂詞，或者可以從已有的謂詞中構造出來。是這樣嗎？

回想一下，即使我們最簡單的類型語言也不僅僅只包含數等基本類型，還包含構造類型。儘管其中的一些，如鏈表和向量，似乎並不是很難，但一旦涉及賦值、性能和問責，挑戰就來了，後面將討論它們。然而，函數就很難處理了。

作為示例，我們來看這個函數：

(define d/dx (lambda (f) (lambda (x) (/ (- (f (+ x 0.001)) (f x)) 0.001))))

其靜態類型是：

((number -> number) -> (number -> number))

（它讀入一個函數，並生成其導數——也是個函數。）假設我們想用契約來處理這種情況。

根本的問題是，在大多數語言中，我們無法直接將其表示為謂詞。大多數語言的運行時系統關於值的類型存儲了非常有限的信息——相對於我們目前所看到的類型，這些信息太過有限，我們應該用不同的名稱來描述它們；傳統上它們被稱為標籤（tag）。【注釋】有些情況下，標籤與我們認為是類型的不謀而合：例如，數會帶上標識其為數的標籤（甚至可能是某種特定類型的數）、字元串帶有標識其為字元串的標籤，等等。因此，我們可以基於這些標籤的值來編寫謂詞。

已經有一些工作試圖保存豐富的類型信息，從源程序到較低的抽象層次、一直到彙編語言，但這些都是研究工作。

當我們處理結構化值時，情況就複雜了。向量將會帶有標籤聲明它是向量，但不會指明它的元素是什麼類型的值（而且它們甚至可能都不是同一類型）；不過，程序通常也可以獲得向量的大小，從而遍歷向量來收集此信息。（然而，關於結構化值後面還更多有待討論的。）

思考題

編寫契約，檢查只包含偶數的鏈表。

這就是：

(define list-of-even?-contract (make-contract (lambda (l) (and (list? l) (andmap number? l) (andmap even? l)))))

（同樣，請注意，如果我們靜態地知道這是數的鏈表，則無需問前兩個問題。）類似地，對象可能只將自己標識為對象，而不提供其他信息。但是，在允許對對象結構進行反射（reflection）的語言中，契約仍可以收集它所需的信息。

然而，在任何語言中，當遇到函數時就出問題了。我們一般將函數的類型理解為包含其輸入和輸出的類型，但是對運行時系統，函數只是帶有函數標籤的不透明對象，可能還有一些非常有限的元數據（如函數的參數數量）。運行時系統甚至難以分辨函數是否讀入和生成函數——而非其他類型的值——更不用說判斷它是否讀入並生成(number -> number)類型的函數了。

這個問題很好地體現在JavaScript的（錯誤命名的）typeof運算符中。傳給其數或字元串等基本類型的值，typeof會返回對應類型名字的字元串（例如"number"）。對於對象，它返回"object"。最要命的是，對於函數它返回"function"，沒有額外的信息。

出於這個原因，typeof對這個操作符來說可能是個糟糕的名字。它應該被稱為tagof，為未來的可能出現的JavaScript靜態類型系統留下的typeof這個名字。

總而言之，這意味著當遇到函數時，函數契約只能檢查它是否的確是函數（如果不是，那顯然是錯誤的）。它無法檢查有關該函數的定義域和值域的任何信息。我們要放棄嗎？

16.3 高階契約

為了確定要做什麼，我們先回憶一下契約最初提供了什麼保證。在前述的real-sqrt-1中，我們要求參數是非負的。然而，只有在real-sqrt-1被實際使用時才會進行檢查，並且僅檢查實際傳入的值。例如，如果程序包含片段

(lambda () (real-sqrt-1 -1))

但該thunk一直沒被調用，那麼程序員將永遠不會看到這裡的契約被違反。事實上，可能在程序的這次運行中沒有調用此thunk，但在後一次運行中調用到了；因此，該程序包含一個潛在的契約錯誤。出於此原因，通常最好用靜態類型來表示不變數；但在使用契約時，我們明白，僅當程序執行到相關位置時，我們才會收到錯誤通知。

這是有用的見解，因為它為我們的函數問題提供了解決方案。對於指明的函數值，我們立即檢查它真的是函數。但是，我們不會忽略定義域和值域的契約，而是延遲處理。我們在函數（每次）實際作用於某個值時檢查定義域契約，並在函數實際返回值時檢查值域契約。

這顯然和make-contract不是一種模式。因此，我們給make-contract起個更具描述性的名稱：它檢查即時的（immediate）契約（即當前可以完整檢查的契約）。

在Racket契約系統中，即時契約被稱為扁平的（flat）。這個術語有點誤導，因為它們也可以保護數據結構。

(define (immediate pred?) (lambda (val) (if (pred? val) val (blame val))))

相比之下，函數契約讀入兩個契約作為參數——分別表示對定義域和值域的檢查——並返回謂詞。這個謂詞作用於需要滿足契約的值。首先，它會檢查給定的值實際上是函數：這部分仍然是即時的。然後，我們創建一個代理（surrogate）函數，由它來應用「剩餘的」契約——檢查定義域和值域——但其他方面與原函數行為相同。

創建代理這一行為背離了傳統的斷言機制，也就是只是簡單地檢查而不改變值。相反，對於函數，如果想要檢查契約，我們必須使用新創建的代理。因此，一般來說我們需要創建封裝函數，它會讀入契約和值，並創建該值的保護版本：

(define (guard ctc val) (ctc val))

一個非常簡單的例子，假設我們要用數契約包裝add1函數（使用稍後定義的函數契約的構造函數function）：

(define a1 (guard (function (immediate number?) (immediate number?)) add1))

我們希望a1本質上綁定到以下代碼：

(define a1 (lambda (x) (num?-con (add1 (num?-con x)))))

其中(lambda (x) ...)是代理；它會add1的調用之處前後調用數值契約。回憶一下，在沒有違規的情況下，契約的行為就是恆等函數，所以這個程序在不違規的情況下行為於add1完全相同。

為了達到此目的，我們使用下面的function定義。【注釋】請記住，我們還必須確保給定的值真的是函數（這裡的add1的確是，這一點可以立即檢查，這也是為什麼在我們將代理綁定到a1時此項檢查已經消失的原因）：

(define (function dom rng) (lambda (val) (if (procedure? val) (lambda (x) (rng (val (dom x)))) (blame val))))

簡單起見，我們這裡假設單參數函數，不過擴展到多參數的情況很簡單。事實上，更複雜的契約甚至可以檢查參數之間的關係。

要理解這是如何工作的，我們來替換參數。為了保持代碼可讀性，我們先構造number?契約檢查器，並將其命名：

(define num?-con (immediate number?))= (define num?-con (lambda (val) (if (number? val) val (blame val))))

回到a1的定義。我們先調用guard：

(define a1 ((function num?-con num?-con) add1))

接下來調用函數契約的構造函數：

(define a1 ((lambda (val) (if (procedure? val) (lambda (x) (num?-con (val (num?-con x)))) (blame val))) add1))

調用左括弧-左括弧-lambda得：

(define a1 (if (procedure? add1) (lambda (x) (num?-con (add1 (num?-con x)))) (blame add1)))

請注意，這一步會檢查被保護的值的確是函數。因此我們得到

(define a1 (lambda (x) (num?-con (add1 (num?-con x)))))

這正是我們想要獲得的代理，對於不違規的調用，其行為就是add1。

思考題

有多少種方式可以違背上述的add1契約？

三種方式，分別對應於三個契約構造函數：

1. 被封裝的值可能不是函數；
2. 被封裝的是函數，它可能被作用於不為數的值；或者
3. 被封裝的是函數，輸入也是數，但其返回值不是數類型。

練習

編寫示例實現這三種違規行為，並觀察契約系統的行為。你能改進錯誤信息以更好地區分這些情況嗎？

同樣的封裝技術也適用於d/dx：

(define d/dx (guard (function (function (immediate number?) (immediate number?)) (function (immediate number?) (immediate number?))) (lambda (f) (lambda (x) (/ (- (f (+ x 0.001)) (f x)) 0.001)))))

練習

違反此契約的方式有七種，分別對應於七個契約構造函數。根據需要，傳入（錯誤的）參數或修改代碼，以違反它們中的每一個。是否可以改進錯誤報告，以正確識別每種違規行為？

請注意，嵌套函數的契約推遲了兩處即時契約的檢查，而不是一處。這符合我們的期望，因為即時契約只能報告實際值的問題，所以直到應用於實際值之前，它們無法報告任何錯誤。但是，這確實意味著「違規」這個概念很微妙：傳遞給d/dx的函數值可能的確違反了契約，但這類違規只有在傳遞或返回數值之後才會被觀測到。

16.4 便捷語法

之前我們看到了兩種扁平契約的使用風格，分別由real-sqrt-1和real-sqrt-2體現。這兩種風格各有缺點。後者讓人聯想到傳統的斷言系統，它不能用於高階值（函數），因為被封裝的值才需要檢查。（當然，傳統的斷言系統只處理扁平契約，所以它們忽略了這個細微的差別。）前者將值的使用放與契約之中，理論上這可行，但有三個缺點：

1. 開發人員可能會忘記封裝某些使用。
2. 契約在每次使用中都會被檢查一次，在多次使用時這是浪費。
3. 程序混合了契約檢查和其功能行為，降低了可讀性。

幸運的是，一般情況下，明智地使用語法糖就可以解決此問題。例如，假設我們要將契約附加到函數的參數上，那麼開發人員可以這麼編寫：

(define/contract (real-sqrt (x :: (immediate positive?))) (sqrt x))

意圖是用positive?來保護x，但只在函數調用時只執行一次檢查。這應該轉化為：

(define (real-sqrt new-x) (let ([x (guard (immediate positive?) new-x)]) (sqrt x)))

也就是說，宏為每個標識符生成新名稱，然後將用戶給出的名稱關聯到新名稱的封裝版本。這個宏的實現如下：

(define-syntax (define/contract stx) (syntax-case stx (::) [(_ (f (id :: c) ...) b) (with-syntax ([(new-id ...) (generate-temporaries #(id ...))]) #(define f (lambda (new-id ...) (let ([id (guard c new-id)] ...) b))))]))

有了這些（語法上的）便利，契約語言的設計師可以提高契約使用的可讀性、效率和健壯性。

16.5 擴展到複合數據結構

正如我們已經討論過的，將契約擴展到結構化數據類型（如鏈表、向量和用戶定義的遞歸數據類型）似乎很容易。只需要提供適當的對運行時觀測集。一般來說這取決於語言提供類型的精度。例如，正如我們之前討論過的，支持數據類型的語言不需要類型謂詞，但仍然會提供區分變體的謂詞；這種情況下，類型級別的「契約」檢查最好（也許必須）留給靜態類型系統，而由契約來斷言更精確的結構特性。

但是，這種策略可能會遇到嚴重的性能問題。例如，假設我們編寫了平衡二叉搜索樹，能以對數漸近時間（相對樹的大小）實現插入和查找。接下來我們將樹封裝在合適的契約中。遺憾的是，僅檢查契約就會訪問整個樹，從而用去線性時間！因此，理想情況下更好的策略是，構建樹的時候就（以增量方式）完成契約檢查，查找時則不需要再次檢查。

更糟的是，平衡和順序都是搜索樹的遞歸屬性。因此原則上，每個子樹都應滿足，所以每次遞歸調用都需要檢查。在插入過程中，由於插入是遞歸的，將在每個訪問的子樹上檢查契約。在大小為 的樹中，契約謂詞應用於 元素的子樹，然後應用於 元素的子子樹，依此類推，在最壞情況下，會訪問總數為 的元素——使我們預期的對數時間插入過程花費線性時間。

對這兩個例子，許多情況下都可以採用措施緩解。每個值都需要與它已經通過的一組契約相關聯（或內部存儲，或存儲於散列表中）。然後，當需要調用契約時，首先檢查它是否已被檢查過，如果有，則不再檢查。這實質上是將契約檢查記憶化（memoization），從而減少檢查的演算法複雜性。當然，對記憶化而言，最好值是不可變的。如果這些值可能發生變化，並且契約執行任意計算，那麼此優化可能無法做到可靠。

檢查數據結構還有一個微妙的問題。作為例子，考慮我們之前編寫的檢查數鏈表中所有值均是偶數的契約。假設我們已經用契約封裝了鏈表，但只對鏈表的第一個元素感興趣。當然，我們檢查了列表中的所有值，這可能需要很長時間。但更重要的是，用戶可能會爭辯說，報告鏈表第二個元素違規的行為本身違反了我們對契約檢查的期望，因為我們並未實際使用該元素。

這意味著推遲檢查某些值，即使它們可以即時被檢查。例如，可以將整個鏈錶轉換為包含延時檢查的封裝值，每個值僅在訪問時被檢查。這種策略可能很有吸引力，但編碼該策略並不簡單，尤其當存在別名的情況下會遇到問題：如果兩個不同的標識符引用同一鏈表，一個有契約保護而另一個沒有，我們必須確保它們都按預期運行（這通常意味著我們不能在鏈表中存儲任何可變狀態）。

16.6 再論契約和觀測

契約實現還有一個奇怪的普遍問題——遇到複雜數據時更甚。之前，我們抱怨說檢查函數的契約很難，因為我們觀測能力受限：我們能檢查的只有值是否是函數。在真實的語言中，數據結構的問題其實是相反的：我們的觀測能力過剩。例如，如果我們實施延遲檢查鏈表的策略，則很可能需要使用某個結構體來保存實際鏈表，並修改first和rest，以此（檢查契約後）獲取結構體中的值。但是，像list?這樣的函數現在可能返回false而不是true，因為結構體不是鏈表；因此，list?需要綁定到新函數上，遇到這些特殊的表示鏈表的延遲契約結構體也返回true。但契約系統作者還需要記得解決cons?、pair?，天知道還有多少其他函數都可以執行觀測操作。

一般來說，有一個觀測基本上不可能「修復」：eq?。通常情況下，每個值eq?它自己，即使函數也是如此。然而，函數封裝以後就是新的函數了，不但不eq?自己，也不應該，因為其行為真的不同了（儘管只是在違反契約的情況下，並且只在提供了足夠多的輸入值得以觀測到違規行為後）。然而，這意味著程序無法暗中保護自己，因為守護行為可以被觀測到。因此，惡意模塊有時可以檢測它收到的是否是受保護的值，如果是就正常運行，否則就不！

16.7 契約和賦值

我們無疑應該關注契約與賦值之間的相互作用，當契約延遲檢查——固有延遲或者以延遲方式實現——時更是如此。有兩件事值得關注。一是將契約值存儲在可變狀態中；二是為可變狀態編寫的契約。

當我們存儲契約值時，封裝策略確保契約檢查正常進行。在每個步驟，契約都會儘可能多地檢查現有的值，並創建包含其餘檢查的封裝值。因此，即使這個封裝值被存儲在可變狀態並在稍後檢索以供使用，它仍然包含這些檢查，並且當值最終被使用時它們將被執行。

另一個問題是編寫可變數據的契約，如box和向量。在這種情況下，我們可能必須為包含契約的整個數據類型創建封裝。然後，當數據類型中的值被替換為新值時，執行更新的操作（例如set-box!）需要從封裝中檢索契約，將其應用於新值並存儲新封裝的值。因此，這需要修改數據結構賦值操作符的行為，使其對契約值敏感。然而，賦值不會改變違規行為的發生點：即時契約即時發生，延時契約遇到（非法）輸入值時發生。

16.8 契約的組合

我們已經討論過所有基本數據類型的組合，本節很自然要契約的組合。正如之前討論的聯合和交叉類型一樣，我們應該考慮契約的聯合和交叉（分別是「或」與「和」）；還應當考慮取反。然而，契約只是表面上類似於類型，所以我們必須根據契約來考慮這些問題，而不是試圖將我們從類型學到的意義映射到契約領域。

直接的例子總是簡單的。聯合契約通過析取組合——事實上，因為是謂詞，其結果可以字面上用or組合——而交叉契約通過合取組合。我們依次調用謂詞，進行短路求值（譯註，參見後文），最後產生錯誤或返回契約的值。交叉契約通過合取（and）組合。而取反契約就是直接調用原始的契約，但對謂詞取反（通過not）。

在延遲、高階的情況下，契約組合要困難得多。例如，考慮對數到數的函數的契約進行取反。這裡取反到底是什麼意思？是否表示該函數不應接受數？或者如果接受了數，它不應該返回數？或兩者都要？特別是，我們如何執行這樣的契約？例如，如何檢查某個函數不接受數——是否期望在給予數時會產生錯誤？但請考慮用這樣的契約封裝的恆等函數；因為當給予數（或者其他任何值）時，它顯然不會出錯，這是否意味著應該等到它產生值，如果它確實產生了數，那麼拒絕它？但最糟糕的是，請注意，這意味著我們將在未定義的定義域中運行函數：顯然這會破壞程序中的不變數、污染堆棧、或使程序崩潰。

交叉契約要求值通過所有子契約。這意味著高階值需要重新封裝，檢查所有定義域子契約以及所有值域子契約。只要一個子契約沒有滿足，整個交叉（契約）都會失敗。

聯合契約更加微妙，因為任何一個子契約失敗都不直接導致值被拒絕。相反，它只是意味著這個子契約不再是所封裝值所遵守的契約；其他子契約仍然可能被遵守，只有當沒有任何子契約候選時才拒絕值。這意味著聯合契約的實現中必須記錄哪些子契約通過或失敗——這裡，記錄就意味著賦值。【注釋】由於每條子包契約失敗時，它將被從候選名單刪除，而剩下的會繼續執行。當沒有候選子契約時，系統必須報告違規行為。錯誤報告最好要提供導致每個子契約失敗的實際值（請記住，這些值可能嵌套在多層函數中）。

在類似Racket的多線程語言中，還需要加鎖以避免競爭條件。

Racket所實現的契約構造器和組合器對可接受的子契約形式提出了限制。這使得實現既有效率又能提供有用的錯誤消息。此外，上面討論的極端情況很少在實踐中出現——當然現在如果需要你知道如何實現它們。

16.9 問責

本節回過頭討論報告契約違反的問題。這指的不是列印什麼字元串，而是更重要的問題，報告什麼。我們將看到，此問題實際上是語義上的考慮。

為了說明這個問題，回想一下上面d/dx的定義，假設我們在沒有任何契約檢查的情況下運行。先假設我們將這個函數應用於完全不合適的string-append（它既不讀入也不產生數）。這麼做只會產生一個值：

> (define d/dx-sa (d/dx string-append))

（請注意，即使有契約檢查，這也會通過，因為函數契約的即時部分認可string-append是函數。）接下來假設我們將d/dx-sa應用於一個數，這應是正常行為：

> (d/dx-sa 10)string-append: contract violation expected: string? given: 10.001

請注意，錯誤報告位於d/dx函數體的內部。一方面，這完全是合理的：這是string-append不正確調用發生的地方。另一方面，錯誤並非來自d/dx，而來自聲稱string-append是合法的數到數的函數的代碼。但問題是，做這件事的代碼早已逃之夭夭；它已經不在堆棧中，因此也不在傳統錯誤報告機制的範圍內。

這個問題不是d/dx所特有的；事實上，大型系統中它很常見。這是因為系統——尤其是含有圖形、網路和其他外部介面的系統——中大量使用回調（callback）：對某個實體感興趣而被註冊的函數（或方法），要發某種狀態或值的信號時被調用。（在這裡，d/dx等價於圖形層，而string-append等價於傳給它（並由它存儲）的回調。）最終，系統層會調用回調。如果這會導致錯誤，那既不是系統層的錯誤，它收到的回調符合要求的契約，也不是回調本身的錯誤，它應該有合理的用途，只是被錯誤地提供給函數。相反，錯誤來源於引入這兩者的實體。然而，此時調用棧只包含回調（位於棧頂）和系統（位於其下）——唯一有錯的一方不在了。這種類型的錯誤因此非常難調試。

解決辦法是擴展契約系統，納入問責（blame）的概念。想法是，有效地記錄將一對組件組合在一起的那個實體，以便如果它們之間發生契約違規，我們可以將失敗歸因於該實體。請注意，這隻在函數的情況下才有實際意義，但為了一致性，我們以自然的方式也將問責擴展到即時契約中。

對於函數，請注意有兩種可能的失敗點：要麼它被給予了是錯誤的值（先驗條件），要麼是它生成了錯誤的值（後驗條件）。區分這兩種情況很重要，因為在前一種情況下，我們應該將錯誤歸咎於環境——這裡，也即實參表達式——而在後一種情況下（假設參數已經通過），則應歸咎於函數本身。（對即時值的自然擴展是我們只能對值值本身不滿足契約進行問責，也就是「後驗條件」）。

對於契約，我們引入術語正（positive）和負（negative）位置。對於一階函數，負位置是先驗條件，正位置是後驗條件。這麼看這似乎是不必要的額外術語。但我們很快就會看到，這兩個術語具有更一般的含義。

現在將情況推廣到契約的參數。之前，即時契約讀入一個謂詞，而函數契約讀入定義域和值域的契約。這點保持不變。不過它們返回的將是函數，此函數有兩個參數：正負位置的標籤。（這個標籤可以是任何合理的數據類型：抽象語法節點、緩衝區偏移量、或其他描述符。簡單起見，我們使用字元串。）這樣，函數契約將閉包於程序位置標籤，以便將來對非法函數的提供方進行問責。

現在由guard函數負責傳入契約調用位置的標籤：

(define (guard ctc val pos neg) ((ctc pos neg) val))

由blame顯示合適的標籤（由契約實現傳給它）：

(define (blame s) (error contract s))

假設我們像以前一樣，保護add1的使用。正負位置用什麼名字有意義呢？正位置是後驗條件：這裡的任何失敗都必須歸咎於add1的函數體。負位置是先驗條件：這裡的任何失敗都必須歸咎於add1的參數。因此：

(define a1 (guard (function (immediate number?) (immediate number?)) add1 "add1 body" ;add1函數體 "add1 input")) ;add1的輸入

假設傳給guard的不是函數，我們會期望在「後驗條件」位置出現錯誤：這並不是後驗條件的失敗，而是因為，如果調用的不是函數，不能去指責參數。（當然，這表明我們這裡擴展了術語「後驗條件」，更合理地應該使用術語「正（位置）」。）因為相信add1的實現只會返回數，所以我們預計它不可能讓後置條件失敗。當然，我們期望像(a1 "x")這樣的表達式觸發先驗條件錯誤，可以在"add1 input"位置處發出契約錯誤。相反，如果我們保護的函數違反了後驗條件，比如這樣，

(define bad-a1 (guard (function (immediate number?) (immediate number?)) number->string "bad-add1 body" "bad-add1 input"))

我們希望將責任被歸咎於"bad-add1 body"。

接下來討論如何實現這些契約構造函數。對於即時契約，我們說過應問責正位置：

(define (immediate pred?) (lambda (pos neg) (lambda (val) (if (pred? val) val (blame pos)))))

對於函數，我們可能想這麼寫

(define (function dom rng) (lambda (pos neg) (lambda (val) (if (procedure? val) (lambda (x) (dom (val (rng x)))) (blame pos)))))

但是這根本不能運作：它違反了契約所預期的簽名。這是因為，現在所有契約都期望輸入正負位置的標籤，也就是dom和rng不能像上面那樣使用。（另一個理由，函數體中用到了pos，但完全不含neg，儘管已經看到過一些例子，我們認為責任必須歸咎於neg所綁定的位置。）所以很明顯，我們要以某種方式使用pos和neg實例化的值域和定義域契約，以便它們「知道」和「記住」可能調用非法函數的地方。

最顯然的做法是用相同的dom和rng值實例化這些契約構造函數：

(define (function dom rng) (lambda (pos neg) (let ([dom-c (dom pos neg)] [rng-c (rng pos neg)]) (lambda (val) (if (procedure? val) (lambda (x) (rng-c (val (dom-c x)))) (blame pos))))))

現在所有簽名都匹配了，我們可以運行契約了。但這樣做時，返回不太對勁。比如，在我們最簡單的違反契約的例子中，返回是

> (a1 "x")contract: add1 body

咦？也許我們應該展開a1的代碼，來看看發生了什麼。

(a1 "x")= (guard (function (immediate number?) (immediate number?)) add1 "add1 body" "add1 input")= (((function (immediate number?) (immediate number?)) "add1 body" "add1 input") add1)= (let ([dom-c ((immediate number?) "add1 body" "add1 input")] [rng-c ((immediate number?) "add1 body" "add1 input")]) (lambda (x) (rng-c (add1 (dom-c x)))))= (let ([dom-c (lambda (val) (if (number? val) val (blame "add1 body")))] [rng-c (lambda (val) (if (number? val) val (blame "add1 body")))]) (lambda (x) (rng-c (add1 (dom-c x)))))

可憐的add1：它都沒有獲得機會！剩下的唯一問責標籤是"add1 body"，所以只能歸咎於它了。

等下會討論此問題，先來觀察上面的代碼，其中沒有任何函數契約的蹤跡。我們有的只是即時契約，當實際值（如果）發生時進行問責。這與我們之前所說只能觀測到即時值完全一致。當然，這隻適用於一階函數；當遇到高階函數時，這不再成立。

錯在哪裡？請注意，在add1函數體中只有綁定到rng-c的契約應該被問責。相反，add1的輸入中應該被問責的是綁定到dom-c的契約。看起來，在函數契約的定義域位置，正負標籤需要……交換。

考慮契約保護的d/dx，我們會發現情況確實如此。關鍵的見解是，當調用的函數作為參數時，「外部」成為「內部」，反之亦然。也就是說，d/dx的函數體——處於正位置——調用了被求微分的函數，將這個函數的函數體置於正位置，並將調用者——d/dx的函數體——置於負位置。因此，在契約的定義域一側，每次嵌套函數契約都會導致正負位置交換。

值域一側無需交換。繼續考慮d/dx。它返回的函數代表導數，所以它的輸入是數（代表計算導數的點），返回也是數（該點的導數）。這個函數的負位置就是使用微分函數的客戶——即先驗條件——正位置就是d/dx本身——即後驗條件——因為它負責生成導數。

這樣，我們就更正的、正確的函數構造函數的定義：

(define (function dom rng) (lambda (pos neg) (let ([dom-c (dom neg pos)] [rng-c (rng pos neg)]) (lambda (val) (if (procedure? val) (lambda (x) (rng-c (val (dom-c x)))) (blame pos))))))

練習

將此應用於之前的例子，確認得到的問責符合預期。此外，手動展開代碼以了解為何。

更進一步，假設我們定義d/dx的正位置標籤為"d/dx body"，負位置標籤為"d/dx input"。假設我們傳給它函數number->string（此函數明顯無法計算導數），然後將結果應用於10：

((d/dx (guard (function (immediate number?) (immediate string?)) number->string "n->s body" "n->s input")) 10)

這正確地表明，應該歸咎於將number->string假定為數函數提供給d/dx的表達式——而不是d/dx本身。

練習

手工計算d/dx，將其作用於所有相關的違規情況，並確認由此產生的問責是準確的。如果你將string->number傳給d/dx，附帶函數契約指明它將字元串映射到數，會發生什麼？如果你在沒有契約的情況下傳入相同的函數呢？

推薦閱讀：