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 iteration either
>
>
Fair comme
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
(provide
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 there
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
> 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 (greater-than-square? x [y
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 tha
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 that
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 r
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 of
>> with-contract / blame-id
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 "blamin
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 u
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 6 mai 2017 23:38:29 UTC+2, Dani
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
>
> unsafe-fac
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: u
> 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 (define/tight (fn args ...)
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
(d
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 n
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*?
> 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 encountered. But that's wishful
Le vendredi 5 mai 2017 19:10:12 UTC+2, Matthias Felleisen a écrit :
> > 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
> 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 for embedded realtime
>> soft
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 alwa
> 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 interesting document, thanks for the ref
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 a
> 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 with all the "provide" statements
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 i
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 per-file syntax
> parameter?).
>
>
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
> invari
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:
>
> Using Ben's left-pad example
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 0))
On Thu, May 4, 2017 at 12:42 PM, Matthias Felleisen
wrote:
>
> 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 :))
>
In Australia th
> 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 invariants or
> covariance
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 the
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 arguments
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,
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 operator
Missing but I am sure
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 contracts, I made a "full" sp
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 (
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 c
> 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 0)) "The sqrt of zero should b
My concept of how (simple) contracts should work was influenced by the
Bertrand Meyer / Eiffel approach and spent many years of rolling my own
contracts in lesser languages to mimic this.
The main things I found pragmatically useful were:
1. Being able to specify pre-conditions and post-condi
41 matches
Mail list logo
