What's the purpose of convoluted racket contract?

Question

I am walking through the racket guide and just finished this page:

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

And the resulting contract is so convoluted that I couldn't believe my eyes:

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

I bet this contract has reached much higher complexity than the needed actual implementation, though this contract doesn't in fact reveal any implementation details. What baffles me more is that the contract is not even a compile time component, like a proof of properties via type system by Curry-Howard isomorphism, so it's not in any sense certified programming approach and defintiely comes with a runtime effect. With this level of complexity, I see no benefit of doing contract more than, say some simple data type checking, which I can see more sense about it.

Could you point out where I am missing about the necessity of such kind of contract?r

Answer 1

This is documentation; the point of the documentation is to cover as many as possible of the features of the contract system.

Suppose I bake wedding cakes. I want to show you what kinds of things you can have on your wedding cake, so I make a cake with every possible decoration you might make, and put it on a simple base—maybe even a piece of cardboard. Would you look at this cake and complain that it's too garish? No. The point is that this is a menu of features; after reading this documentation, you should be able to understand what all of the different pieces do.

Answer 2

The page to which you link starts:

7.4 Contracts: A Thorough Example

This section develops several different flavors of contracts for one and the same example: Racket’s argmax function.

The final flavor is the most thorough ("convoluted").

You seem to think the page is attempting to convince you that contracts are a "necessity". I don't see that. I see it explaining what is possible to do with contracts -- if/as/when you think the benefits exceed the costs. If you deem never, that's fine.

For what it's worth, I've read a fair amount of Racket code, and I've rarely seen such a complicated contract. Also, Racketeers are well aware that contracts have a runtime cost; often people use them only at important "boundaries".

Finally, if you prefer static types, you might prefer Typed Racket. Note that you can mix dynamically and statically typed Racket modules. To ensure the static type invariants, the boundary is protected by... contracts.