复杂的球拍合同的目的是什么？

Question

我正在浏览球拍指南，刚刚完成了这一页：

https://docs.racket-lang.org/guide/contracts-first.html

由此产生的合同是如此错综复杂，以至于我都不敢相信我的眼睛：

(provide
 (contract-out
  [argmax
    (->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
         (r (f lov)
            (lambda (r)
              (cond
                [(empty? (rest lov)) (eq? (first lov) r)]
                [else
                 (define f@r (f r))
                 (define flov (map f lov))
                 (and (is-first-max? r f@r (map list lov flov))
                      (dominates-all f@r flov))]))))]))

我敢打赌，这个契约已经达到了比所需的实际实现更高的复杂性，尽管这个契约实际上并没有透露任何实现细节。更让我困惑的是，契约甚至不是一个编译时组件，就像Curry-Howard同构的类型系统的属性证明一样，所以它在任何意义上都不是经过认证的编程方法，而且肯定会带来运行时效果。在这种复杂程度下，我看不到做契约的好处，只是，比如说一些简单的数据类型检查，我可以看到更多的意义。

你能指出我没有注意到这种合同的必要性吗？

Answer 1

这是文档；文档的重点是尽可能多地涵盖合同系统的功能。

假设我烤婚礼蛋糕。我想向你展示你的婚礼蛋糕上可以有什么东西，所以我做了一个蛋糕，里面有你可能做的所有可能的装饰品，然后把它放在一个简单的基座上--甚至可能是一块纸板。你会不会看着这块蛋糕，抱怨它太花哨了？不是的。重点是，这是一个功能菜单；在阅读本文档之后，您应该能够理解所有不同部分的功能。

Answer 2

您链接到的页面将启动：

7.4合约:一个完整的示例

本节为一个相同的示例开发了几种不同风格的合约:球拍的argmax函数。

最后的味道是最彻底的(“纠结”)。

你似乎认为这个页面试图说服你，合同是一种“必需品”。我可没看出来。我看到它解释了合同的可能性--如果/当/当你认为收益超过成本时。如果你认为永远不会，那也没关系。

值得一提的是，我已经阅读了相当多的球拍代码，我很少看到如此复杂的合同。此外，Racketeers很清楚合同有运行时成本；人们通常只在重要的“边界”使用它们。

最后，如果你喜欢静态类型，你可能更喜欢类型化的球拍。请注意，您可以混合使用动态和静态类型的球拍模块。为了确保静态类型不变，边界由...合同。