As far as I understand Racket best practices, the reason ->i is preferred over ->d (to the point of calling ->d broken) is because ->i guards uses of the variables bound within the contract.
But define/contract doesn’t guard recursive calls, and contract-out guards even less. Between the two of these, contract-out is preferred, and this lack of checking is considered positive for performance.
Why doesn’t that apply to the use of ->d, too? (Or does it? Maybe these best practices I’m trying to reconcile aren’t even opinions held by the same people.) It seems like if I’m making performance-conscious use of lean contracts that only guard the external API of my code, then I won’t want them to spend extra time checking that I wrote the contracts correctly. Contracts can show up in documentation and in particularly cautious client code, too, so does that have something to do with it?
Perhaps this is a question for @robby?
The problem with ->d is that it doesn’t fully protect the function wrt the boundary you specify. It’s not a question of more checks vs less.
@robby has joined the channel
What distinction are you making between “doesn’t fully protect the function” and fewer checks?
I looked through that paper but basically came away knowing more words for the same question. It looks like a lot of attention is paid not to doing more checks but to properly assigning blame for the same ones, but that seems to mainly have to do with ruling out a third semantics, picky, that does just as many checks as ->i but blames the contract-internal ones on the contracted function.
This was originally part of my question:
> Contracts can show up in documentation and in particularly cautious client code, too, so does that have something to do with it? > The answers I’m seeking might be behind this. Even in simple contract-out situations where all the blamed components are entire modules, a function contract may originate from a different module than the function does, because it may be part of the contract of a higher-order function. I don’t know quite what to conclude from this yet.
The example in the ->d docs is:
> For example, using this contract > (->d ([f (-> integer? integer?)])
#:pre
(zero? (f #f))
any) > will allow f to be called with #f, trigger whatever bad behavior the author of f was trying to prohibit by insisting that f’s contract accept only integers. > But it wasn’t the author of f who insisted on this. It was the author of this (->d <...>) contract, unless we take such a fine-grained view as to acknowledge that different subexpressions of a contract expression could have been written by different authors.
If this author (I’ll assume just one) had wanted their own (-> integer? integer?) contract to prevent them from calling f with #f, they could have written (define/contract protected-f <...> f) inside the precondition and called protected-f instead.
And if they really were both making a mistake and forgetting to guard against it, then how is it different than if they had made any other uncaught mistake in writing the contract? It gets me thinking, “Pray, Mr. Babbage, if you put into the machine wrong contracts, will correct blame come out?”
In terms of the examples in the paper…
> Sadly, blame correctness cannot differentiate between lax and indy. Since lax may trigger crashes in the presence of precise specifications, it is clearly not correct. > The example being referenced here (which I’ve omitted) is a buggy specification in its own right. Sometimes it fails with its own errors, which can be attributed to a specific part of its code (the use of random-number). This isn’t “clearly” a “precise specification.”
Handling part of the error-reporting responsibility in the design of ->d itself (by recommending ->i) seems generally helpful, but not for a reason like ->d itself being erroneous. And the reason I find it helpful (more thorough internal checking) is the opposite of the reason I find contract-out helpful, hence my sense that there are mixed messages here.
The example in “4.2 Neither Lax Nor Picky Is a Complete Monitor” is much longer, but it looks like the point is still that there’s a function call within the contract itself that may cause a contract error but doesn’t have a well-defined party to blame for it.
The point of the example in section 4.2 is that a value flows from one side of the contract boundary to the other without being protected by a contract. Obviously avoiding that requires having enough checks, but it’s about a particular notion of boundaries, which is also what determines the checks imposed by the other forms you mention.
The paper also discusses picky, as you say, which has enough checks but the wrong blame
The whole point of the paper is to give a precise framework for determining what side of the boundary different values come from
In the example you show, the function comes from one side of the boundary and is applied to a value from the other side without a contract check
The example with (f #f)? The value #f comes from the contract itself, right? (Just orienting myself with regard to this “the other side” terminology, which I would have thought meant from the client/negative side to the server/positive side or vice versa…)
If I’m understanding right, then I’m basically at:
Yes, it gets bound to f within the contract without being projected through the contract (-> integer? integer?). If I’m in the mood to cut down on checks, that sounds like a feature.
If I’m in the mood to be formally precise about things crossing boundaries, I might still want to accommodate this use case. Given the motivations that led to ->i (or at least the ones I think we’re on the same page on), we might agree it’s useful to talk about a contract boundary having three sides: The server/positive side, the client/negative side, and the contract side itself. The typical logic of a contract has to do with projecting a value from the server/positive side to the client/negative side. The (-> integer? integer?) contract here is in negative position, where it’s repurposed to project a value from the client/negative side to the server/positive side. Either way, that’s not the same direction the f binding is going! We need it to project a value from the client/negative side to both the contract side and the server/positive side. Let’s say projecting from anywhere to the contract side is “projecting inward,” while the usual directions are “projecting across.”
The ->d combinator assumes no contract ever imposes any checks on a value that’s projected inward; the (-> integer? integer?) contract is only in negative position and not in some kind of combination negative and negatively inward position. The ->i combinator assumes that for every contract, projecting inward is the same as projecting across.
I think whether either one of these assumptions is correct is moot. The ->d and ->i operations are themselves a part of the contract specification, and even if individual contracts had an innate notion of “projecting inward,” either or both of these operations could be designed in a way that explicitly overrode that innate behavior.
This has been on my mind since I learned about ->d and ->i, but for a long time I just assumed I should make all my contract boundaries as tight and strict as possible and that that’s why ->i was preferred. Being reminded tonight that define/contract put a boundary around a whole definition form, rather than making a stricter boundary around a variable binding, made me wonder why it wasn’t considered buggy for an analogous reason. Between then and now, I caught on to the fact contract-out was often preferred to define/contract and usually gave me better blame messages, so most of my code uses contract-out, and the assumption that initially let me embrace ->i no longer seems as clear.