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 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Reply via email to