Re: [racket-users] Apropos contracts: simple predicates and switching on and off

On Mon, May 8, 2017 at 3:05 AM, Matthias Felleisen wrote: > > Measure with outer contract and remove the inner define/tight. If you > wrote this algorithm with a loop in Eiffel, instead of a tail-recursive > function, you wouldn’t check the invariant for every loop

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Thanks Georges, Matthias, and Philip for the further pointers: Helped by your comments I inferred that I could construct a legitimate unsupplied-arg case using case-lambda. I think that this is the kind of illustration would be helpful in the docs: #lang racket (module server racket

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

I was also surprised by the-unsupplied-arg ( http://docs.racket-lang.org/reference/function-contracts.html#%28def._%28%28lib._racket%2Fcontract%2Fbase..rkt%29._the-unsupplied-arg%29%29) when I first encountered it: perhaps it should not be the very last thing in the documentation for ->i? If

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Le dimanche 7 mai 2017 23:14:17 UTC+2, Daniel Prager a écrit : > Thanks for the explanation on 2. Pragmatically, it's just another contributor > to the cost of contract checking. I suppose you meant point 3, instead of point 2? The thread I linked to indicates that with ->d, the double-checking

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

> On May 7, 2017, at 1:26 AM, Daniel Prager wrote: > > Putting this new set-up through its paces I think I've found a few issues: > > 1. Default argument goes missing from post-condition, leading to an > unexpected error … (define (default-y x) 0) (define/contract

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Hi Georges Thanks for the explanation on 2. Pragmatically, it's just another contributor to the cost of contract checking. On 1, I'm (naïvely) baffled as to why the contract should regard an optional argument as unsupplied when it comes from the default rather than an explicit passing. GIven

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Le dimanche 7 mai 2017 07:27:08 UTC+2, Daniel Prager a écrit : > 1. Default argument goes missing from post-condition, leading to an > unexpected error ... You should use unsupplied-arg? . But I couldn't find a way to get the default value from the contract. I would guess that the problem is

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Putting this new set-up through its paces I think I've found a few issues: *1. Default argument goes missing from post-condition, leading to an unexpected error ...* (define/contract (greater-than-square? x [y 0]) (->i ([x real?]) ([y real?]) [result boolean?] #:post (x y

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

I did #1681. The region one is arguably correct. > On May 6, 2017, at 6:36 PM, Dupéron Georges > wrote: > > Le dimanche 7 mai 2017 00:27:36 UTC+2, Daniel Prager a écrit : >> Thanks Georges >> >> It looks suggestive, but I'm struggling to follow the details

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Le dimanche 7 mai 2017 00:27:36 UTC+2, Daniel Prager a écrit : > Thanks Georges > > It looks suggestive, but I'm struggling to follow the details of > with-contract / blame-id. An example of use would be very helpful in the docs! This gives "blaming: (region unsafe-factorial)" instead of

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Those who look shall be rewarded: (define unsafe-factorial (invariant-assertion (-> (and/c integer? (>=/c 0)) (and/c integer? (>=/c 0))) (lambda (n) (if (zero? n) 1 (* n (unsafe-factorial (- n 10))) (unsafe-factorial 5) BUT @robby the invariant-assertion

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Thanks Georges It looks suggestive, but I'm struggling to follow the details of with-contract / blame-id. An example of use would be very helpful in the docs! Have you used this construct? Dan On Sun, May 7, 2017 at 7:44 AM, Dupéron Georges wrote: > Le samedi

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Le samedi 6 mai 2017 23:38:29 UTC+2, Daniel Prager a écrit : > Although I understand why my macro does this > > unsafe-factorial: contract violation > ... > blaming: (function fn/impl) > ... > at: unsaved-editor:13.15 > > > Ideally I would prefer one which blames unsafe-factorial > >

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Although I understand why my macro does this unsafe-factorial: contract violation ... blaming: (function fn/impl) ... at: unsaved-editor:13.15 Ideally I would prefer one which blames unsafe-factorial unsafe-factorial: contract violation ... blaming: (function unsafe-factorial) ... at:

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

> On May 5, 2017, at 11:30 PM, Daniel Prager wrote: > > Thank-you Matthias > > That's neat! > > And yes, I can write a basic macro. By introducing #:freevar I was able to > improve the blame situation, but the abstraction is a bit leaky ... > > (define-syntax-rule

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Thank-you Matthias That's neat! And yes, I can write a basic macro. By introducing #:freevar I was able to improve the blame situation, but the abstraction is a bit leaky ... (define-syntax-rule (define/tight (fn args ...) ctc body ...) (begin

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Sure: #lang racket (define/contract [unsafe-factorial n] (-> (and/c integer? (>=/c 0)) (and/c integer? (>=/c 0))) (if (zero? n) 1 (* n (factorial (- n 10) (define (factorial n) (unsafe-factorial n)) ;; cross the boundary and go right back in (unsafe-factorial 5) ; Does

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Hi Matthias Thanks for the pointer to Robby's 2014 keynote. Here's the link for those interested — it's really good: https://www.youtube.com/watch?v=gXTbMPVFP1M * * * In regard to Racket's use of boundaries, am I right in thinking that it's difficult to pull the boundaries in really *tight*?

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

> On May 5, 2017, at 1:21 PM, Dupéron Georges > wrote: > >> >> [What’s the diff to 1?] > > The difference would be that a partial check would be performed at each > recursion step, stopping when data which has already been validated by the > same contract is

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

> On May 5, 2017, at 11:30 AM, Dupéron Georges > 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

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

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

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

> On May 5, 2017, at 10:05 AM, Dupéron Georges > wrote: > > Le vendredi 5 mai 2017 15:24:40 UTC+2, Matthias Felleisen a écrit : >> See >> https://docs.racket-lang.org/style/Units_of_Code.html#%28part._.Modules_and_their_.Interfaces%29 > > That's a very

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Le vendredi 5 mai 2017 15:24:40 UTC+2, Matthias Felleisen a écrit : > See > https://docs.racket-lang.org/style/Units_of_Code.html#%28part._.Modules_and_their_.Interfaces%29 That's a very interesting document, thanks for the reference. Would you suggest that, in this spirit, types for functions

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

> On May 4, 2017, at 8:40 PM, Dupéron Georges > wrote: > > Le vendredi 5 mai 2017 02:30:50 UTC+2, Ben Greenman a écrit : >> With a `define/contract-out` macro? >> >> But I'd rather not have a macro like this in the contract library. >> I prefer reading code

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Le vendredi 5 mai 2017 02:30:50 UTC+2, Ben Greenman a écrit : > With a `define/contract-out` macro? > > But I'd rather not have a macro like this in the contract library. > I prefer reading code with all the "provide" statements at the top of the > file. Since provide transformers are executed

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

On Thu, May 4, 2017 at 8:23 PM, Dupéron Georges wrote: > In these cases, instead of turning off the contract checks altogether, it > would be nice to have a way to disable the define/contract and turn it into > a contract-out, using a single parameter (perhaps a

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Le jeudi 4 mai 2017 03:00:10 UTC+2, Daniel Prager a écrit : > On the subject of turning down contracts for performance and then being > bitten, believe me, I hear you: my preference is to have the maximum checking > I can afford. But when I'm really writing stringent post-conditions (or >

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Please read The Contract Guide at https://docs.racket-lang.org/guide/contracts.html?q=contracts It has many examples and gradually builds intuition. The ideal PR would be to specific chapters there. > On May 4, 2017, at 12:38 AM, Daniel Prager wrote: > >

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Using Ben's left-pad example as a model I get the following re-write of the real-sqrt contract (([x real?]) #:pre/name (x) "non-negative argument expected" (>= x 0) . ->i . [result (x) real?] #:post/name (x result) "the sqrt of zero is zero" (implies (= x 0) (= result

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

> On May 3, 2017, at 10:01 PM, Daniel Prager wrote: > > Do you bet on the Formula I driver whose team includes the most safety > features? ;-) Yes. He’s more like to survive and get across the goal line :)) > From a technical perspective I'm happy to not mention

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Hi Matthias (and everyone) Matthias wrote: > As Tony Hoare said, what do you think of a boater who practices on land with his swim vest on and then goes to sea and takes the swim vest off? I think the only way to reply to these sorts of arguments is to wrestle back the framing! Do you bet on

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Thanks Ben The left-pad example is most helpful. Perhaps it could be included in the docs, given that usefully illustrates features of ->i for which no example is given. I may well have a shot at re-implementing it once I have sufficient machinery set up to support multiple and optional

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Hi Philip Thank-you for sharing your version: each example and variation is helping me understand the machinery better. I agree that clarity in error reporting is also vital, and it's been made clear to me that it is feasible to hook into the contract system and take advantage of its facilities,

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

You have gotten plenty of good answers so let me focus on some of the high-level points and some details that people didn’t respond to: > On May 2, 2017, at 6:01 PM, Daniel Prager wrote: > > More concise and clear expression of contracts > • The implies

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

On Tue, May 2, 2017 at 11:43 PM, Daniel Prager wrote: > I kind of expected that it would be possible to do what I wanted with > "indy" contracts, but struggled with the heavy use of combinators in the > examples. Two offhand thoughts: 1. To practice with dependent

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Here's the "quick" way I'd write the real-sqrt in Racket, combined with an illustration of one of the advantages of using the established contract combinators: here they gracefully report a kind of error that in the original would have caused an error in the error-checking code. (define/contract

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

Thanks Matthew That's very helpful. I definitely want to hook into the existing contract system if possible, and you've given some good pointers to how this might be done. I kind of expected that it would be possible to do what I wanted with "indy" contracts, but struggled with the heavy use of

Re: [racket-users] Apropos contracts: simple predicates and switching on and off

> On May 2, 2017, at 4:33 PM, Daniel Prager wrote: > > (define/pre-post (real-sqrt x) > #:pre ([(real? x) "real argument expected"] > [(>= x 0) "non-negative argument expected"]) > > #:implementation (sqrt x) > > #:post ([(implies (= x 0) (= result