> On May 5, 2017, at 11:30 AM, Dupéron Georges <jahvascriptman...@gmail.com> > wrote: > > 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 assume input is also a list. Then Racket’s define/contract is NOT O(n²) because the recursion of foo is considered INSIDE the boundary. You have to jump through hoops to get define/contract to check recursive calls. (If it does so now, it’s a bug.) > I'd consider this bad programming. It's not about small speed improvements, > it's about making an application unusable altogether Absolutely. Which is why I assumed you had written an alternative to get the recursion checked. > > 4. (define/contract (foo input) (-> blah (listof integer?)) …) > where the contract check stops when it encounters an already-checked value. [What’s the diff to 1?] > > 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? Have you considered using nano-pass specific types? Leif and I did for a brief time, but we moved on to other things. (We had a private exchange on that one.) -- 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.
