Best way to use contracts -- define/contract, contract-out, ...?

I make heavy use of define-contract in my code, since I like having the system do the work of catching when I pass the wrong thing from another function.

I've seen other modules and documentation that leave the contracts off inside the module but use contract-out when providing them. I'm guessing the value here is that the functions run faster inside the module because the arguments aren't being checked once they're inside? I get it, but for most of my code I'm happy to trade some speed for a lot of security.

How do other people use the contract system, if you do? What are your thoughts on the best way to do it?

NB: I thought of this question after reading the "Best Practices for Contracts" question, which is really more about defining and documenting than using, and I wanted to close the gap. Best practices for contracts

3 Likes

In addition to possible performance improvements for calls from within the library, the error messages for contract violations can often be clearer with contract-out. That's because there is no way to get at the internals of a function via an import of a module except going via require and provide (and so you can make sure you've got all the necessary contracts).

3 Likes

I'm not quite following that. Could you expand on it for me?

When you use define/contract, the function you define might use another function in the same module. This use of the other function is "implicit" in the sense that you might not have explicitly put a contract on the other function. With contracts at modules, this implicit use is impossible; all exports have to explicitly be provided and then you can put the contracts you want them to have.

There is also a more complex issue at work here that is probably not worth going in to, but the way it manifests itself is people getting confused with error messages from contracts that originate with define/contract. But using modules completely avoids this other, complex issue too.

3 Likes

I think you're saying that this is problematic:

(define/contract (get-number)
  (-> number?)
  (waste-time)
  7)

(define (waste-time)
  'do-nothing)

(provide get-number)  

waste-time is not provided to outside functions but there's in implicit export in the sense that it's called from inside get-number. I'm still not getting it. Sorry for being slow, but this seems like pretty bog-standard interface exposure, where public functions are exported and private functions are not. What is the issue? Outside consumers can't get at waste-time, surely?

There is also a more complex issue at work here that is probably not worth going in to, but the way it manifests itself is people getting confused with error messages from contracts that originate with define/contract . But using modules completely avoids this other, complex issue too.

I don't want to take up too much of your time but is there anywhere I can read about that issue? Given my heavy use of define/contract I'd like to be aware of any potential landmines.

For the former, that's not the kind of thing I meant. I just meant that you can write define on some definitions, define-contract on others and thus (accidentally) fail to notice that you should have added a contract somewhere, which might get confusing. With modules, you cannot forget in this sense.

Here's an example of the second for you to consider:

#lang racket

(define/contract (f x)
  (-> natural? integer?)
  (- 1 x))

(define/contract (g x)
  (-> integer? integer?)
  (f -1))

(g 5)

which produces this error message:

f: contract violation
  expected: natural?
  given: -1
  in: the 1st argument of
      (-> natural? integer?)
  contract from: (function f)
  blaming: /Users/robby/tmp.rkt
   (assuming the contract is correct)

One might argue that the blaming line is wrong and it should have blamed g instead with a line like this one:

  blaming: (function g)

the reason it doesn't is subtle and tricky and can be defended from a language-design/calculus point of view. The difference with modules is that this kind of pathological situation is not possible because you cannot get from f to g without an explicit connection via require and provide.

There was a long, deep discussion on the racket mailing list about this topic in, I think, fall of 2018? I'm not completely sure of the dates, but Matthias and Alexis and probably some others (maybe Christos Dimoulas) were involved in it. You may find more value rereading that, than continuing here, as it was a very thoughtful discussion.

1 Like

Ah, I see. That makes sense. Thanks!

I'll dig around on the mailing list and see if I can find the convo.

I poked around too and didn't find it. Maybe I imagined it :cry:. But let me know if you want to continue discussing!

1 Like

Oh, I'm definitely interested! Racket is one of these deep languages where there's always more to learn, and I love that. I simply didn't want to bother you if you were done with the subject. Please do continue.

1 Like

As always, apologies if what I'm about to say is flawed or just wrong....

I think that the primary innovation of the racket contract system is that it recognizes that in the world of higher-order functions, "blame" is not obvious. That is: if we agree that you give me a function from numbers to numbers and I give you back a number, and I then take that function from numbers to numbers and pass it to another function that wants a function from positive numbers to positive numbers, whose fault is it when the function gets called with a negative number? This kind of blame tracking and assignment is (in my mind) the key problem that's solved by Racket's contract system.

However, I believe that the blame system depends fundamentally on the notion of "parties"; that is, code (or coders) that represent the two sides of the agreement. I believe that when we use define/contract internally, the blame correctness statement can't be guaranteed, and maybe doesn't even make sense.

For that reason, my sense is that when I use define/contract internally, it can be useful, but I'm sort of "doing it wrong", in the sense that I'm failing to set up the blame component correctly.

Again, just my ramblings, apologies if I'm all wet.

2 Likes

Huh. How would Racket assess the blame on that, because it seems to me like it could be assigned to multiple parties. I've seen the terms 'positive blame' and 'negative blame' in the docs but I don't understand them.

How is define/contract different from contract/out in this case?

Actually, my example is simpler than I'd imagined, because if the third party accepts a function from positive numbers to anything and calls it with a negative number, that third party has definitely broken its contract with the second party. A better example occurs when the second party accepts a function from positive numbers to positive numbers and passes it to a function that expects a num->num.

Honestly, rather than trying to construct examples, I should just point you the guide, which actually has some nice examples:

https://docs.racket-lang.org/guide/contract-boundaries.html

(NB: this is the guide, not the reference)

3 Likes

Most of my stuff is for personal use, but I prefer define-contract with a macro to turn the contracts all on/off for development. I find it very helpful to define contracts for every function when trying to find out where some bug is occurring, though I prefer not to leave these on when doing any performance sensitive stuff outside of debugging.

However, if you can afford the performance overhead, I think you should use define-contract for anything with non-trivial constraints on the return value. If the only significant checks are basic type checks on the input, I think contract-out can be appropriate since your module should know what it is doing.

One final style worth mentioning is having your code split up into many submodules such that each "kernel" of work is its own module and therefore contract-out makes sense. Even if only a single function, this might make sense if you are writing a recursive function (I don't often use recursion since I'm fond of for/ style loops).