Le vendredi 5 mai 2017 16:36:49 UTC+2, Matthias Felleisen a écrit : > I think that developers should write contracts and use them during testing > and deployment in the same way. I did this decades ago for embedded realtime > software and we’d be all better off if we did so.
I agree that I always feel uneasy about turning off contracts. But sometimes performance is a problem. How would you therefore recommend checking the invariant that the recursive function's output is a list of integers, then (as a simple example)? 1. (define/contract (foo input) (-> blah (listof integer?)) …) This has a O(n²) cost. I'd consider this bad programming. It's not about small speed improvements, it's about making an application unusable altogether (the SMS app on my phone has a O(n²) somewhere, with n the number of texts sent. After a few thousands, it takes 30s to send a text, so it is effectively unusable). 2. (provide (contract-out [foo (-> blah (listof integer?))])) + regular define This has a O(n) cost, but does not perform any check during recursive calls. If the function is a case-lambda with many cases (which happens often in one form or another in macro implementations), it's then hard to guess which case is the culprit. One then has to resort to printf-debugging and throw-away sanity checks inserted during the debugging session and removed afterwards. 3. (define/contract (foo input) (-> blah (or/c (cons/c integer? any/c) null?)) …) This has a O(n) cost, and checks recursive calls, but it relies on the fact that the implementation of foo prepends elements to the result one at a time. If the implementation is changed so that at one point is prepends two elements, the contract fails to properly check the result. Ideally, there would be a way to attach to a value a witness that a given contract was checked against it: 4. (define/contract (foo input) (-> blah (listof integer?)) …) where the contract check stops when it encounters an already-checked value. In my current academic project (a typed variant of Nanopass), I'm using a hybrid approach: types enforce "simple" invariants. More complex structural invariants (acyclicity, well-scopedness, backward "parent" pointers in the AST which indeed point to the correct parent, and so on) are checked at run-time, since they cannot be expressed using Typed Racket's type system alone. Once such an invariant is checked, a phantom type is used on the value's type to indicate that the value was safely checked against a given invariant. This allows compile-time verification that a call to a transformation pass gives a value which was properly checked, and also reduces the need for performing the same checks against the AST too often (passing the same AST to two or more analysis passes needs only one check). I'm unaware of mechanisms which would allow annotating list elements or syntax objects in Racket, which would allow solution 4 to work. If it was possible to have chaperone contracts on pairs, it would be possible to wrap the checked output values with a no-op "witness" chaperone, and check for the presence of the chaperone. Alternatively, the contract system could maintain a cache of recently-checked values (like equal? does) e.g. using a weak hash table. Of course, the best solution is to use types, but until Typed Racket becomes versatile enough to write macro implementations, and until Typed Racket gains dependent types, so that a wide range of expressive properties can be encoded, what would you recommend? -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
