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

[Dupéron Georges]

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 the contract 
can be specified separately from the function, and the function itself knows 
the default argument's value. In the general case, extracting the default 
argument's value (without running the default expression multiple times) might 
be tricky.

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

This does look like a real (pun intended) problem.

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

With the code below, the post-condition only gets called once:

#lang racket

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

(real-sqrt 1)

With this code, however, the contract does get called twice:

#lang racket

(define/contract (real-sqrt x)
  (->i ([x real?])
   #:pre (x)
   (>= x 0)
   [result (λ (result) (displayln result) (>= result 0))]
   #:post (result) #t)
  (sqrt x))

(real-sqrt 1)

See this very interesting thread on the mailing list for a detailed discussion 
about this 
https://groups.google.com/forum/#!searchin/racket-users/contract$20twice%7Csort:relevance/racket-users/SUzcozdPh6Q/bjgEjTyQEAAJ
 .

Short story: if one of the arguments is a function, and a dependent #:pre, 
#:post, argument or result contract calls that function, you want it to be 
protected. The contract therefore needs to be applied to the argument before it 
is passed to the other dependent clause, and is applied again when actually 
calling the function.

> Finally, some timings.

Thanks for taking the time to test this out :) .

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

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

[In Eiffel I'd need to use a check condition in my loop. Below I explore
the moral equivalent of raising an error in Racket, which seems to work
well enough.]


I've removed the offending post-condition and redone the timings. (Code at
end)


*No contracts*
cpu time: 13 real time: 13 gc time: 0

*Outer contract only*
cpu time: 48 real time: 48 gc time: 0

*Outer contract + inner exception check*
cpu time: 63 real time: 73 gc time: 15

*Outer + tight inner contract*
cpu time: 1251 real time: 1268 gc time: 27



The virtue of the inner contract is that it catches non-terminating cases
during development.

E.g. In the recursive call (S (* 0.5 (+ estimate (/ x estimate if we
replace / with * the "tight" contract catches it by imposing a bounds
check.

*Note*: I haven't reintroduced the more stringent requirement that the
error reduces with every iteration (monotonic convergence).


*Take-away*

The timings suggest that applying the contract system is a particularly
expensive way to achieve this level of safety. The outer contract + inner
exception check is a much more affordable alternative.

This example isn't enough to really explore the question of whether it
makes sense to later turn off the inner checks, once confidence has been
achieved. Personally, I'd say "it depends" on how slow we're going and
whether it makes a difference and what cheaper checks are available.

YMMV

Dan



#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 (default-eps) 1e-14)

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

(define/contract (real-sqrt x [eps (default-eps)])
  (->i ([x (>=/c 0)])
   ([eps (>/c 0)])
   [result (>=/c 0)]
   #:post (x result)
   (implies (= x 0) (= result 0))
   #:post (x eps result)
   (let ([EPS (if (unsupplied-arg? eps)
  (default-eps)
  eps)])
 (implies (> x 0) (< (sqrt-error x result) EPS

  (define/tight (S estimate)
(->i ([estimate (and (>/c 0) (<=/c (max 1 x)))])
 [result (>/c 0)])

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

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


(define/contract (real-sqrt-moderate x [eps (default-eps)])
  (->i ([x (>=/c 0)])
   ([eps (>/c 0)])
   [result (>=/c 0)]
   #:post (x result)
   (implies (= x 0) (= result 0))
   #:post (x eps result)
   (let ([EPS (if (unsupplied-arg? eps)
  (default-eps)
  eps)])
 (implies (> x 0) (< (sqrt-error x result) EPS

  (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 (* 0.5 (+ 1 x)

(define/contract (real-sqrt-modified x [eps (default-eps)])
  (->i ([x (>=/c 0)])
   ([eps (>/c 0)])
   [result (>=/c 0)]
   #:post (x result)
   (implies (= x 0) (= result 0))
   #:post (x eps result)
   (let ([EPS (if (unsupplied-arg? eps)
  (default-eps)
  eps)])
 (implies (> x 0) (< (sqrt-error x result) EPS

  (define (sqrt-error estimate)
(abs (- 1 (/ (sqr estimate) x

  (define (S estimate)
(unless (<= 0 estimate (max 1 x))
  (raise-arguments-error 'real-sqrt-modified "Broken bounds"
"estimate" estimate
"x" x))
(if (< (sqrt-error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))

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


(define (real-sqrt-fast x [eps (default-eps)])
  (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 (* 0.5 (+ 1 x)


(displayln "No contracts")
(time
 (for ([i (in-range 5000)])
   (real-sqrt-fast i)))

(newline)
(displayln "Outer contract only")
(time
 (for ([i (in-range 5000)])
   (real-sqrt-moderate i)))

(newline)
(displayln "Outer contract + inner exception check")
(time
 (for ([i (in-range 5000)])
   (real-sqrt-modified i)))

(newline)
(displayln "Outer 

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

[Dupéron Georges]

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 does not occur. Although the docs 
mention ->d is left only for backward compatibility, it is still available.

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

#lang racket
(define my-contract
  (->i () ([x (>=/c 1)]) [result real?]
   #:post (x result) (>= result (sqr x

(define (my-sqr [y 10]) (* y y))
(define (my-cub [z 20]) (* z z z))

(define/contract my-sqr-contracted my-contract my-sqr)
(define/contract my-cub-contracted my-contract my-cub)

Contracts are values. In the example above, the default value for the first 
optional argument (named x in the contract) is not the same for the first and 
second functions (10 and 20 respectively).

To emphasise the separation between the contract and the functions, I used 
different variable names in the contract (x) and the functions (y and z, 
respectively). I also defined the functions separately, so that when the 
contract is attached, the function's source is not syntactically within 
define/contract (the functions could even be defined in another module).

I'm not sure it is even possible to access the default value for an argument 
once the function is created. If it is possible (but I doubt it), then the 
contract could extract the default expression (which could refer to a global 
mutable value) when a check occurs. It would be nice indeed if this magic 
occurred, but it seems non-trivial to implement.

Furthermore, an poorly designed contract could incorrectly pre-compute the 
default expression, and pass it to the function (e.g. pass 11 instead of 10, 
due to a bug in the contract implementation). The simple fact that this is 
technically possible to make it impossible for the contract generated by ->i to 
be a chaperone, instead it would have to be an impersonator.

You can easily enough define a leaky abstraction with a macro which copies the 
default expression in the contract and in the function signature (but this 
would cause multiple evaluations). I tired to think about caching the value, 
but can't find a way to do so without breaking the blame mechanism (e.g. by 
wrapping the function, the inner one with the contract + mandatory arguments, 
and the outer one with optional arguments + no contract).

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

[Philip McGrath]

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 are optional arguments that are not supplied, then the
> corresponding variables will be bound to a special value called
> the-unsupplied-arg value. For example, in this contract:
> (->i ([x (y) (if (unsupplied-arg? y)
>  real?
>  (>=/c y))])
>  ([y real?])
>  any)
> the contract on x depends on y, but y might not be supplied at the call
> site. In that case, the value of y in the contract on x is
> the-unsupplied-arg and the ->i contract must check for it and tailor the
> contract on x to account for y not being supplied.
> When the contract expressions for unsupplied arguments are dependent, and
> the argument is not supplied at the call site, the contract expressions are
> not evaluated at all. For example, in this contract, y’s contract
> expression is evaluated only when y is supplied:
> (->i ()
>  ([x real?]
>   [y (x) (>=/c x)])
>  any)
> In contrast, x’s expression is always evaluated (indeed, it is evaluated
> when the ->i expression is evaluated because it does not have any
> dependencies).


Aside from Dupéron's point that "the contract can be specified separately
from the function, and the function itself knows the default argument's
value", I have found cases when it's actually useful to know explicitly
whether an argument was supplied or not. For example, make-id-cookie

uses a single ->i contract to check that it was called with either three
by-position arguments or two by-position arguments and a #:key argument
(but not three by-position arguments and a #:key argument). Then the actual
implementation can use a default value of #f (which wouldn't satisfy any of
the relevant contracts) for these supposedly-optional arguments, and
normalizing the arguments becomes just a matter of using or.


-Philip

On Sun, May 7, 2017 at 4:13 PM, Daniel Prager 
wrote:

> 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 that Racket obliges you to supply a default when declaring an
> optional argument, in what sort of situations does the unsupplied case
> arise?
>
> Dan
>
>
>
> On Sun, May 7, 2017 at 10:36 PM, Dupéron Georges <
> jahvascriptman...@gmail.com> wrote:
>
>> 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 the
>> contract can be specified separately from the function, and the function
>> itself knows the default argument's value. In the general case, extracting
>> the default argument's value (without running the default expression
>> multiple times) might be tricky.
>>
>> --
> 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.
>

-- 
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 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 (default-y x)])
  (->i ([x real?])
   ([y real?])
   [result boolean?]
   #:post (x y result)
   (equal? result (< (sqr (if (unsupplied-arg? y) (default-y x) y)) x)))
  (> x (sqr y)))

(greater-than-square? 10)


> 3. post-conditions appear to be called twice ...
> 
> Is there a double boundary crossing on post-conditions?


Yes! Your syntax rule says to check the post-condition twice: 

(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   now you see it checked only 
once 
   (define (fn/impl args ...)
 body ...


> Finally, some timings.

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 

— Matthias


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

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 that Racket obliges you to supply a default when declaring an
optional argument, in what sort of situations does the unsupplied case
arise?

Dan



On Sun, May 7, 2017 at 10:36 PM, Dupéron Georges <
jahvascriptman...@gmail.com> wrote:

> 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 the
> contract can be specified separately from the function, and the function
> itself knows the default argument's value. In the general case, extracting
> the default argument's value (without running the default expression
> multiple times) might be tricky.
>
>

-- 
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, 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 (contract-out
[f (->* (number?) (number?) number?)]
[g (->i ([a real?])
([b real?])
(result real?)
#:post (a b result)
(let ([B (if (unsupplied-arg? b) (default-b) b)])
  (= (* (sgn a) (sgn B)) (sgn result]))

(define (default-b) 10)

(define f (case-lambda
[(a) (+ a (default-b))]
[(a b) (+ a b)]))

(define g (case-lambda
[(a) (* a (default-b))]
[(a b) (* a b)])))



(require 'server)

(f 10)
(f 10 -5)

(g 10)
(g 10 -5)

I suppose this falls into the class of learning challenges where certain
aspects of the design of a feature are explained by the existence of
"advanced" concepts that not everyone may be yet using routinely, or even
be familiar with.

Dan

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