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

[Daniel Prager]

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 result)
   (equal? result (< (sqr y) x)))

  (> x (sqr y)))

(greater-than-square? 10)


sqr: contract violation
  expected: number?
  given: #


*2. contract-exercise seems to miss explicit #pre-conditions ...*

(contract-exercise sqrt2) finds no counter-examples (correct)
(contract-exercise sqrt3) finds bogus counter-examples (incorrect),
typically -inf.0 and -1


(define/contract (real-sqrt2 x)
  (-> (>=/c 0) (>=/c 0))
  (sqrt x))


(define/contract (real-sqrt3 x)
  (->i ([x real?])
   #:pre (x)
   (>= x 0)
   [result (>=/c 0)])
  (sqrt x))



*3. post-conditions appear to be called twice ...*

Is there a double boundary crossing on post-conditions?

Output from instrumenting of (real-sqrt 100), Newton's method for
calculating the sqrt loaded with contracts (source code at end of e-mail)
...


> (real-sqrt 100 1e-14)


(10.0 0.0)
(10.0 0.0)
(10.0139897 2.7979396577393345e-11)
(10.0139897 2.7979396577393345e-11)
(10.52895642693 1.0579156517920296e-05)
(10.52895642693 1.0579156517920296e-05)
(10.032578510960604 0.0065263157858850285)
(10.032578510960604 0.0065263157858850285)
(10.840434673026925 0.17515023900164373)
(10.840434673026925 0.17515023900164373)
(15.025530119986813 1.257665553866309)
(15.025530119986813 1.257665553866309)
(26.24009900990099 5.88542796049407)
(26.24009900990099 5.88542796049407)
(50.5 24.5025)
10.0


Note: The reverse order is because of the nature of the recursion — to be
useful in catching errors in runaway computations the check should be moved
to the pre-condition.

* * *

Finally, some timings.

Stripping out the contracts to get a fast implementation for comparison:

(define (real-sqrt-fast x [eps 1e-14])
  (define (sqrt-error estimate)
(abs (- 1 (/ (sqr estimate) x

  (define (S estimate)
(if (< (sqrt-error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))

  (if (zero? x)
  0
  (S x)))

More moderate choice of contracts:

(define/contract (real-sqrt-moderate x [eps 1e-14])
  (->* ((>=/c 0)) ((>/c 0)) (>=/c 0))
  (define (sqrt-error estimate)
(abs (- 1 (/ (sqr estimate) x

  (define/tight (S estimate)
(-> (and (>/c 0) (<=/c (max 1 x))) (>/c 0))
(if (< (sqrt-error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))

  (if (zero? x)
  0
  (S x)))

The fully contract-loaded code is at the end of this email (just comment
out the displayln).


Timing code:


(time
 (for/last ([i (in-range 1000)])
   (real-sqrt 1000 1e-14)))

(time
 (for/last ([i (in-range 1000)])
   (real-sqrt-moderate 1000)))

(time
 (for/last ([i (in-range 1000)])
   (real-sqrt-fast 1000)))



*All the contracts*
cpu time: 840 real time: 1048 gc time: 288
31.622776601683793

*Moderate (but still some "tight") use of contracts *
cpu time: 404 real time: 443 gc time: 163
31.622776601683793

*No contracts*
cpu time: 3 real time: 3 gc time: 0
31.622776601683793

So a 280x speed-up / slow-down for heavy-duty use of "tight" contracts. ;-)
Only a factor of 2x difference between the contract variations.

Dan


Contracts for real-sqrt

#lang racket

(define-syntax-rule (define/tight (fn args ...)
  ctc
  body ...)
  (begin
(define (fn args ...) (fn/impl args ...))
(with-contract fn
  ([fn/impl ctc])
  #:freevar fn ctc
  (define (fn/impl args ...)
body ...

(define-syntax-rule (implies a b)
  (or (not a) b))

(define (sqrt-error x estimate)
  (-> (>/c 0) (>/c 0) (>=/c 0))
  (abs (- 1 (/ (sqr estimate) x

(define/contract (real-sqrt x eps)
  (->i ([x (>=/c 0)]
[eps (>/c 0)])
   [result (>=/c 0)]
   #:post (x result)
   (implies (= x 0) (= result 0))
   #:post (x eps result)
   (implies (> x 0) (< (sqrt-error x result) eps)))

  (define/tight (S estimate)
(->i ([estimate (and (>/c 0) (<=/c (max 1 x)))])
 [result (>/c 0)]
 #:post/name (estimate result)
 "Unless it is practically zero, the error should decrease with
every iteration"
 (let ([dr (sqrt-error x result)])
   (displayln (list estimate (sqrt-error x estimate)))
   (or (< dr eps)
   (< dr (sqrt-error x estimate)

(if (< (sqrt-error x estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))

  (if (zero? x)
  0
  (S (* 0.5 (+ 1 x)


(define (real-sqrt-fast x [eps 1e-14])
  (define (error estimate)
(abs (- 1 (/ (sqr estimate) x

  (define (S estimate)
(if (< (error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))

  (if (zero? x)
  0
  (S x)))

-- 
You received 

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

[Matthias Felleisen]

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. An example of use would be very helpful in the 
>> docs!
> 
> This gives "blaming: (region unsafe-factorial)" instead of "blaming: 
> (function unsafe-factorial)". Aside from this slight leak, the messages are 
> identical. Supposing this code is correct (I never used with-contract 
> before), if you clean it up a bit and add an example to the docs, I'm sure a 
> PR would be welcome :) .
> 
> #lang racket
> (define-syntax-rule (define/tight (fn args ...)
>  ctc
>  body ...)
>  (begin
>(define (fn args ...) (fn/impl args ...))
>(with-contract fn
>   ([fn/impl ctc])
>   #:freevar fn ctc
>   (define (fn/impl args ...)
> body ...
> 
> (define/tight [unsafe-factorial n]
>  (-> (and/c integer? (>=/c 0)) (and/c integer? (>=/c 0)))
>  (if (zero? n) 
>  1
>  (* n (unsafe-factorial (- n 10)
> (unsafe-factorial 5)

-- 
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.

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

[Dupéron Georges]

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 "blaming: (function 
unsafe-factorial)". Aside from this slight leak, the messages are identical. 
Supposing this code is correct (I never used with-contract before), if you 
clean it up a bit and add an example to the docs, I'm sure a PR would be 
welcome :) .

#lang racket
(define-syntax-rule (define/tight (fn args ...)
  ctc
  body ...)
  (begin
(define (fn args ...) (fn/impl args ...))
(with-contract fn
   ([fn/impl ctc])
   #:freevar fn ctc
   (define (fn/impl args ...)
 body ...

(define/tight [unsafe-factorial n]
  (-> (and/c integer? (>=/c 0)) (and/c integer? (>=/c 0)))
  (if (zero? n) 
  1
  (* n (unsafe-factorial (- n 10)
(unsafe-factorial 5)

-- 
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.

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

[Matthias Felleisen]

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 uses the contract region machinery (or something like 
your syntax rule) and thus blames the (seemingly) wrong party: 

> unsafe-factorial: contract violation
>   expected: (and/c real? (not/c negative?))
>   given: -5
>   in: an and/c case of
>   the 1st argument of
>   (->
>(and/c
> integer?
> (and/c real? (not/c negative?)))
>(and/c
> integer?
> (and/c real? (not/c negative?
>   contract from: anonymous-module
>   blaming: anonymous-module
>(assuming the contract is correct)
>   at: unsaved-editor:21.3






> On May 6, 2017, at 6:27 PM, Daniel Prager  wrote:
> 
> 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, 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-factorial: contract violation
> > ...
> >   blaming: (function unsafe-factorial)
> > ...
> >   at: unsaved-editor:13.15
> >
> >
> > i.e. it's leaking an auxillary introduced by the macro (fn/impl) into the
> > message & Dr Racket. It seems that the line-number refers to the line that
> > defines unsafe-factorial, though, which looks right.
> 
> Perhaps with-contract's `blame-id` can help?
> 
> http://docs.racket-lang.org/reference/attaching-contracts-to-values.html#%28form._%28%28lib._racket%2Fcontract%2Fregion..rkt%29._with-contract%29%29
>  
> 

-- 
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.

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

[Daniel Prager]

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, 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-factorial: contract violation
> > ...
> >   blaming: (function unsafe-factorial)
> > ...
> >   at: unsaved-editor:13.15
> >
> >
> > i.e. it's leaking an auxillary introduced by the macro (fn/impl) into the
> > message & Dr Racket. It seems that the line-number refers to the line
> that
> > defines unsafe-factorial, though, which looks right.
>
> Perhaps with-contract's `blame-id` can help?
>
> http://docs.racket-lang.org/reference/attaching-contracts-
> to-values.html#%28form._%28%28lib._racket%2Fcontract%
> 2Fregion..rkt%29._with-contract%29%29

-- 
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.

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

[Dupéron Georges]

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-factorial: contract violation
> ...
>   blaming: (function unsafe-factorial)
> ...
>   at: unsaved-editor:13.15
>
>
> i.e. it's leaking an auxillary introduced by the macro (fn/impl) into the
> message & Dr Racket. It seems that the line-number refers to the line that
> defines unsafe-factorial, though, which looks right.

Perhaps with-contract's `blame-id` can help?

http://docs.racket-lang.org/reference/attaching-contracts-to-values.html#%28form._%28%28lib._racket%2Fcontract%2Fregion..rkt%29._with-contract%29%29

-- 
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.

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

[Daniel Prager]

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: unsaved-editor:13.15


i.e. it's leaking an auxillary introduced by the macro (fn/impl) into the
message & Dr Racket. It seems that the line-number refers to the line that
defines unsafe-factorial, though, which looks right.

I could ameliorate this by having my macro give a more suggestive name e.g.
"unsafe-factorial/impl", but perhaps there's a better approach.

* * *

Matthias wrote
> The only thing that leaks is that >/c is actually an and/c contract — and
I will say I am rather surprised by that.

Me too!

I ended up switching my contract to (and/c integer? (not not/c negative?))
to remove the inconsistency, but it does seem to point to another leak.

Dan


On Sun, May 7, 2017 at 12:25 AM, Matthias Felleisen 
wrote:

>
> 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 ...)
>   ctc
>   body ...)
>   (begin
> (define (fn args ...) (fn/impl args ...))
> (define/contract (fn/impl args ...)
>   ctc
>   #:freevar fn ctc; Directs blame to "fn/impl" rather than the
> enclosing module
>   body ...)))
>
>
>
> I am not sure what you mean by ‘leaky’. When I run this,
>
> (define/tight [unsafe-factorial n]
>   (-> (and/c integer? (>=/c 0)) (and/c integer? (>=/c 0)))
>   (if (zero? n)
>   1
>   (* n (unsafe-factorial (- n 10)
> (unsafe-factorial 5) ; Does not terminate
>
> I get
>
> unsafe-factorial: contract violation
>   expected: (and/c real? (not/c negative?))
>   given: -5
>   in: an and/c case of
>   the 1st argument of
>   (->
>(and/c
> integer?
> (and/c real? (not/c negative?)))
>(and/c
> integer?
> (and/c real? (not/c negative?
>   contract from: anonymous-module
>   blaming: (function fn/impl)
>(assuming the contract is correct)
>   at: unsaved-editor:13.15
>
>
>
> The only thing that leaks is that >/c is actually an and/c contract — and
> I will say I am rather surprised by that.
>
>

-- 
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.

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

[Matthias Felleisen]

> 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 ...)
>   ctc
>   body ...)
>   (begin
> (define (fn args ...) (fn/impl args ...))
> (define/contract (fn/impl args ...)
>   ctc
>   #:freevar fn ctc; Directs blame to "fn/impl" rather than the 
> enclosing module
>   body ...)))
> 


I am not sure what you mean by ‘leaky’. When I run this, 

(define/tight [unsafe-factorial n]
  (-> (and/c integer? (>=/c 0)) (and/c integer? (>=/c 0)))
  (if (zero? n) 
  1
  (* n (unsafe-factorial (- n 10)
(unsafe-factorial 5) ; Does not terminate

I get 

> unsafe-factorial: contract violation
>   expected: (and/c real? (not/c negative?))
>   given: -5
>   in: an and/c case of
>   the 1st argument of
>   (->
>(and/c
> integer?
> (and/c real? (not/c negative?)))
>(and/c
> integer?
> (and/c real? (not/c negative?
>   contract from: anonymous-module
>   blaming: (function fn/impl)
>(assuming the contract is correct)
>   at: unsaved-editor:13.15


The only thing that leaks is that >/c is actually an and/c contract — and I 
will say I am rather surprised by that. 

-- 
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.