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
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
For more options, visit https://groups.google.com/d/optout.