畳んだラケット契約の目的は何ですか？

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))]))))])) 

私はこれを賭けますこの契約は実際に実装の詳細を明らかにしていませんが、契約は必要な実際の実装よりもずっと複雑になりました。何が私をさらに悩ませているのは、契約がカリー・ハワードの同型性による型システムを介したプロパティの証明のようなコンパイル時のコンポーネントでもないことです。したがって、認定されたプログラミングアプローチではなく、ランタイム効果が欠点です。この複雑さのレベルでは、単純なデータ型チェックというよりも、契約をすることの利点がありません。これについては、私はそれについてもっと知ることができます。 ？

私は契約書のような種類の必要性について、行方不明ですどこが指摘でしたR

Answer 1

これはドキュメントです。文書化のポイントは、契約システムの機能の可能な限り多くをカバーすることです。

ウェディングケーキを焼くとします。あなたの結婚式のケーキにはどんな種類のものがあるのか​​を見せてもらいたいので、作る可能性のあるすべての装飾が施されたケーキを作り、それを簡単なベースに置いてください。あなたはこのケーキを見て、それがあまりにも派手であると不平を言うでしょうか？いいえ、ポイントは機能のメニューです。このドキュメンテーションを読んだ後で、さまざまな部分が何をするのかを理解できるはずです。

Answer 2

あなたが開始リンクするページ：

7.4契約：徹底した例

このセクションでは、1と 同じ例えば契約のいくつかの異なる味の開発：ラケットのARGMAX機能を。

最終的なフレーバーは、最も徹底的に（「畳み込まれた」）です。

あなたは契約書が「必要性」であるとあなたを説得しようとしていると思うようです。私はそれを見ない。私はそれがが可能であることを説明することを参照してください。は、契約と関係があります。あなたが決してないと思うなら、それは大丈夫です。

ラケットコードはかなり価値があると思いますが、そのような複雑な契約はめったにありません。また、Racketeersは、契約にはランタイムコストがあることをよく認識しています。多くの場合、人々は重要な「境界」でのみそれらを使用します。

最後に、静的型を好む場合は、型付きラケットが好きかもしれません。動的に型定義されたRacketモジュールを混在させることができます。静的型不変量を保証するために、境界は...契約によって保護されています。