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

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

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

[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

[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

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

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.

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

[Daniel Prager]

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

Dan


On Sat, May 6, 2017 at 11:15 AM, Matthias Felleisen 
wrote:

>
> 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 not terminate
>
>
> I suspect you can implement this with a macro now.
>

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

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


I suspect you can implement this with a macro now. 



> On May 5, 2017, at 5:48 PM, Daniel Prager  wrote:
> 
> 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*?
> 
> For instance, the following example does not terminate and cannot help with 
> the necessary debugging because the contract is only checked on the call 
> through the module boundary, with recursive calls incorrectly and implicitly 
> trusted:
> 
> 
> #lang racket
> 
> (module server racket
>   (provide (contract-out
> [unsafe-factorial (-> (and/c integer? (>=/c 0))
>   (and/c integer? (>=/c 0)))]))
>
>   (define (unsafe-factorial n)
> (if (zero? n) ; Naïvely relying on the 
> contract to rule out -ve n's
> 1
> (* n (unsafe-factorial (- n 10))  ; Bug
> 
> 
> (require 'server)
> 
> (unsafe-factorial 5) ; Does not terminate
> 
> 
> My best idea at the moment is to add some extra checking, e.g. (just 
> duplicating the pre-conditions) ...
> 
>   (define (safe-factorial n)
> (unless (integer? n)
>   (raise-argument-error 'safe-factorial "n must be an integer" n))
> (unless (>= n 0)
>   (raise-argument-error 'safe-factorial "n must be >= 0" n))
> (if (zero? n)
> 1
> (* n (safe-factorial (- n 10))
> 
> ... but this is verbose, no good for higher-oder conditions, and redundant: 
> once it has been debugged the contract at the module-boundary suffices.
> 
> What do others do / suggest?
> 
> 
> 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.

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

[Daniel Prager]

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

For instance, the following example does not terminate and cannot help with
the necessary debugging because the contract is only checked on the call
through the module boundary, with recursive calls incorrectly and
implicitly trusted:


#lang racket

(module server racket
  (provide (contract-out
[unsafe-factorial (-> (and/c integer? (>=/c 0))
  (and/c integer? (>=/c 0)))]))

  (define (unsafe-factorial n)
(if (zero? n) ; Naïvely relying on the
contract to rule out -ve n's
1
(* n (unsafe-factorial (- n 10))  ; Bug


(require 'server)

(unsafe-factorial 5) ; Does not terminate


My best idea at the moment is to add some extra checking, e.g. (just
duplicating the pre-conditions) ...

  (define (safe-factorial n)
(unless (integer? n)
  (raise-argument-error 'safe-factorial "n must be an integer" n))
(unless (>= n 0)
  (raise-argument-error 'safe-factorial "n must be >= 0" n))
(if (zero? n)
1
(* n (safe-factorial (- n 10))

... but this is verbose, no good for higher-oder conditions, and redundant:
once it has been debugged the contract at the module-boundary suffices.

What do others do / suggest?


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.

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

[Matthias Felleisen]

> 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 thinking for now.


Mike Sperber’s language (DieMachtDerAbstraktion) in the DrRacket menu comes 
with a contract system that does this. It checks recursive calls and memoizes 
so that your algorithm has a large constant degradation but is in the correct 
complexity class. The language itself is kind of like the teaching languages 
for HtDP so impoverished. 

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

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

[Dupéron Georges]

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'd consider this bad programming. It's not about 
small speed improvements, it's about making an application unusable altogether 
(the SMS app on my phone has a O(n²) somewhere, with n the number of texts 
sent. After a few thousands, it takes 30s to send a text, so it is effectively 
unusable).

2. (provide (contract-out [foo (-> blah (listof integer?))])) + regular define

  This has a O(n) cost, but does not perform any check during recursive calls. 
If the function is a case-lambda with many cases (which happens often in one 
form or another in macro implementations), it's then hard to guess which case 
is the culprit. One then has to resort to printf-debugging and throw-away 
sanity checks inserted during the debugging session and removed afterwards.

3. (define/contract (foo input) (-> blah (or/c (cons/c integer? any/c) null?)) 
…)

  This has a O(n) cost, and checks recursive calls, but it relies on the fact 
that the implementation of foo prepends elements to the result one at a time. 
If the implementation is changed so that at one point is prepends two elements, 
the contract fails to properly check the result.

Ideally, there would be a way to attach to a value a witness that a given 
contract was checked against it:

4. (define/contract (foo input) (-> blah (listof integer?)) …)
  where the contract check stops when it encounters an already-checked value.

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?

-- 
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 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 reference. Would you 
> suggest that, in this spirit, types for functions are moved to the top of the 
> file with the provide forms, instead of being specified alongside each 
> function?

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
Yes. There is a broken form of type-out that supports some of this already. I 
am hoping Sam will get to fixing this eventually. @samth 
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - 


> 
>>> On this topic, I have sometimes written recursive functions with expensive 
>>> contracts (when recursing down a list, a contract on the whole list will 
>>> have a total cost of O(n²)).
>> 
>> 2. I consider this a horrible idea and I made sure define/contract does not 
>> do so. If you feel that unsure about recursive functions, I recommend using 
>> types. They help you avoid typos at that level. 
> 
> I'm using types wherever possible. Unfortunately, TR does not (yet) mix well 
> with contracts (but I'm aware that there is a pending PR for this).


- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
Yes. I am hoping Sam will get to fixing and approving this eventually. @samth 
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - 


> More importantly, Typed Racket cannot be used to write macro implementations, 
> for several reasons:


I guess I underestimated what kind of code you’re writing. Your concerns are 
real. 


> I'm genuinely unsure which aspect of this idea you find horrible?
> 
> * Is it because the contract is specified along the function, with 
> define/contract-out, instead of being written alongside the provide forms? If 
> so, separating the contract from the function definition, using a form 
> similar to TR's (: name type), would allow the contract to be specified next 
> to the provide form, but still have it applied to recursive function calls 
> during debugging.
> 
> * Is it because turning off the contract for recursive calls would lower the 
> safety (i.e. the swim vest analogy)? In my case, the contract on the result 
> was strong enough to catch the error anyway, and the goal was only to catch 
> incorrect results as soon as possible, instead of waiting until they cross 
> the module boundary and are returned to the original caller, so that it is 
> easier to locate the exact source of the error.
> 
> * Is it because of something else that I missed?
> 
> In conclusion, I do agree that types are a much better option, and I do use 
> them wherever possible. Unfortunately, there are some cases where types 
> cannot be used (yet), and in those cases I'd like to get as much help as I 
> can from contracts when debugging, without imposing a horrendous cost during 
> normal development (which does not mean tossing all safety aside, but rather 
> allow errors to be caught at module boundaries instead of detecting them 
> nearly immediately). These goals do not seem insane to me, and I'm 100% open 
> to suggestions on how to achieve this :) .


The cost and the false sense of security implied by a contract you ran on 
recursive calls and that you then turned off. 

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. 

— 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

[Dupéron Georges]

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 are moved to the top of the file with 
the provide forms, instead of being specified alongside each function?

> > On this topic, I have sometimes written recursive functions with expensive 
> > contracts (when recursing down a list, a contract on the whole list will 
> > have a total cost of O(n²)).
> 
> 2. I consider this a horrible idea and I made sure define/contract does not 
> do so. If you feel that unsure about recursive functions, I recommend using 
> types. They help you avoid typos at that level. 

I'm using types wherever possible. Unfortunately, TR does not (yet) mix well 
with contracts (but I'm aware that there is a pending PR for this). More 
importantly, Typed Racket cannot be used to write macro implementations, for 
several reasons:

* Lack of immutable values at the type level (this means that values with type 
Syntax can in principle contain mutable values, which break occurrence typing)

* syntax/parse (and possibly syntax/case) have not been ported to Typed Racket.

I did in the past a couple of experiments to use Typed Racket to implement 
macros, but the results were unsatisfactory. My best attempt so far, 
tr-immutable/typed-syntax (still unstable and undocumented) requires "unsafe" 
mutable syntax values to be converted to a "safe" representation, and converted 
back after executing the macro.

When writing complex compile-time transformations, I felt the need to check the 
input and output of every recursion step, to catch the exact point at which an 
error occurs.

I'm genuinely unsure which aspect of this idea you find horrible?

* Is it because the contract is specified along the function, with 
define/contract-out, instead of being written alongside the provide forms? If 
so, separating the contract from the function definition, using a form similar 
to TR's (: name type), would allow the contract to be specified next to the 
provide form, but still have it applied to recursive function calls during 
debugging.

* Is it because turning off the contract for recursive calls would lower the 
safety (i.e. the swim vest analogy)? In my case, the contract on the result was 
strong enough to catch the error anyway, and the goal was only to catch 
incorrect results as soon as possible, instead of waiting until they cross the 
module boundary and are returned to the original caller, so that it is easier 
to locate the exact source of the error.

* Is it because of something else that I missed?

In conclusion, I do agree that types are a much better option, and I do use 
them wherever possible. Unfortunately, there are some cases where types cannot 
be used (yet), and in those cases I'd like to get as much help as I can from 
contracts when debugging, without imposing a horrendous cost during normal 
development (which does not mean tossing all safety aside, but rather allow 
errors to be caught at module boundaries instead of detecting them nearly 
immediately). These goals do not seem insane to me, and I'm 100% open to 
suggestions on how to achieve this :) .

-- 
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 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 at the top of the 
>> file.
> 
> Since provide transformers are executed in two passes (the second one being 
> after the expansion of the rest of the file, IIRC), I thought about writing 
> define/contract-out so that it saves the contract, but does not implicitly 
> provide the identifier.


See 
https://docs.racket-lang.org/style/Units_of_Code.html#%28part._.Modules_and_their_.Interfaces%29


[[ In a world where the IDE teases out all possible provides and can show a 
beautifully formatted interface for a module, we might not want to follow 
linguistics. ]] 



> On this topic, I have sometimes written recursive functions with expensive 
> contracts (when recursing down a list, a contract on the whole list will have 
> a total cost of O(n²)).


1. It’s “recurring” not “recursing”. The latter means curse and curse and curse 
and curse . . . 

2. I consider this a horrible idea and I made sure define/contract does not do 
so. If you feel that unsure about recursive functions, I recommend using types. 
They help you avoid typos at that level. 

— 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

[Dupéron Georges]

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 in two passes (the second one being 
after the expansion of the rest of the file, IIRC), I thought about writing 
define/contract-out so that it saves the contract, but does not implicitly 
provide the identifier.

That way, if the identifier is provided, the "saved" contract is attached to it.

Types in Typed Racket work a bit like this: the type is defined or inferred 
alongside the function definition, but is also provided. The implementation 
mechanism is a bit more complex though (it relies on a submodule to store the 
types).

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

[Ben Greenman]

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?).
>
> I'm not sure what would be the best syntax and implementation strategy for
> this, though.
>

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.

-- 
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 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 
> invariants) they can get *really* expensive, negatively impacting on user 
> experience, which takes us into the land of pragmatic trade-offs. 
> 
> If I don't have a way to turn them off I'm either not going to write them at 
> all or comment them out, and then regret not using them on smaller test 
> scenarios.

On this topic, I have sometimes written recursive functions with expensive 
contracts (when recursing down a list, a contract on the whole list will have a 
total cost of O(n²)).

Using (provide (contract-out …)) is of course the right solution for the final 
version, but during debugging, the extra checks at each recursion step can help 
pinpoint bugs more easily.

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

I'm not sure what would be the best syntax and implementation strategy for 
this, though.

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

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 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))
>#:post/name (x result)
>"the sqrt of a positive number is positive"
>(implies (> x 0) (> result 0))
>#:post/name (x result)
>"result * result = x (to within error)"
>(implies (> x 0) (<= (abs (- x (* result result))) 0.0001)))
> 
> Other than a bit of repetition — multiple uses of #:post/name — this is 
> pretty darn close to what I was after.
> 
> Like most people, when faced with something complex and a bit daunting — in 
> this case the ->i contract combinator — I benefit from concrete examples. 
> 
> If enough people encourage me to "make a pull request" once I'm more familiar 
> I'll propose some more examples myself.
> 
> * * *
> 
> My off-hand proposal would be to permit a variation on #:pre/name, 
> #:post/name and friends to allow multiple clauses. For example:
> 
>  #:post/name (x result)
>["sqrt of zero is zero" (implies (= x 0) (= result 0))]
>["sqrt of a positive number is positive" (implies (> x 0) (> result 0))]
>["result * result = x (to within error)" 
> (implies (> x 0) (<= (abs (- x (* result result))) 0.0001))]
> 
> 
> Next stop ... boundaries.
> 
> 
> Thanks again
> 
> Dan
> 
> 
> On Wed, May 3, 2017 at 1:57 PM, Ben Greenman  
> wrote:
> 
> 1. To practice with dependent contracts, I made a "full" spec for the 
> JavaScript left-pad function.
> https://www.npmjs.com/package/left-pad
> 
> The exercise was fun, I learned a lot, and I think my solution is "as 
> readable as possible" :) .
> https://github.com/bennn/racket-left-pad
> 
> 
> -- 
> 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

[Daniel Prager]

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))
   #:post/name (x result)
   "the sqrt of a positive number is positive"
   (implies (> x 0) (> result 0))
   #:post/name (x result)
   "result * result = x (to within error)"
   (implies (> x 0) (<= (abs (- x (* result result))) 0.0001)))

Other than a bit of repetition — multiple uses of #:post/name — this is
pretty darn close to what I was after.

Like most people, when faced with something complex and a bit daunting — in
this case the ->i contract combinator — I benefit from concrete examples.

If enough people encourage me to "make a pull request" once I'm more
familiar I'll propose some more examples myself.

* * *

My off-hand proposal would be to permit a variation on #:pre/name,
#:post/name and friends to allow multiple clauses. For example:

 #:post/name (x result)
   ["sqrt of zero is zero" (implies (= x 0) (= result 0))]
   ["sqrt of a positive number is positive" (implies (> x 0) (> result 0))]
   ["result * result = x (to within error)"
(implies (> x 0) (<= (abs (- x (* result result))) 0.0001))]


Next stop ... boundaries.


Thanks again

Dan


On Wed, May 3, 2017 at 1:57 PM, Ben Greenman 
wrote:

1. To practice with dependent contracts, I made a "full" spec for the
> JavaScript left-pad function.
> https://www.npmjs.com/package/left-pad
>
> The exercise was fun, I learned a lot, and I think my solution is "as
> readable as possible" :) .
> https://github.com/bennn/racket-left-pad
>
>

-- 
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 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 again for now: they don't seem very relevant in the main Racket 
> use cases


You need to wrap your head around boundaries. Google for Robby’s keynote at 
ICFP in Goteburg and try to scan this paper: 

   http://www.ccs.neu.edu/racket/pubs/#icfp16-dnff 




-- 
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 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 Formula I driver whose team includes the most safety
features? ;-)

> We want you to take responsibility for taking the swim vest off.

I love this comment!

* * *

On the Eiffel in contrast to Racket stuff, I appreciate that significant
advances have been made, serious issues addressed, and changes too in your
group's work on Contracts.

For me, as a practitioner, Eiffel did some things very well within its
limitations, and I wasn't affected by the shortcomings too badly.

In moving over to Racket I appreciate the breadth and depth of all the
additional stuff one can do, which — along with the terrific community — is
why I'm here.

>From a technical perspective I'm happy to not mention invariants or
covariance again for now: they don't seem very relevant in the main Racket
use cases.


Thanks again!

Dan


On Thu, May 4, 2017 at 1:51 AM, Matthias Felleisen 
wrote:

>
> 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 we would accept a pull request on that one.
>
>
> >   • Proper support for invariant-checking
>
>
> Well. It’s kind of there (see appended code at end) but not exactly.
> Eiffel has re-entry problems with invariants and Spec# cleaned this up a
> bit. We have a ‘boundary philosophy’ (see beginning of Contract Guide and
> what I wrote there) and that is much cleaner but distinct from Eiffel for
> sure.
>
>
> >   • Proper support for covariant inheritance
>
>
> That’s unsound so we did not want to go there.
>
>
> >   • Tools for automatically generating documentation
>
> Good idea. We have bits and pieces for that. Nothing too useful.
>
>
> >   • Better tools for turning off contracts by configuration
>
>
> 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?
>
>
> > My questions are:
> >   • Is it feasible to get similar behaviour from the official
> contract system?, or
> >   • Do these considerations call for building up an alternative
> system?
>
>
> Yes you can. Racket’s contract system is far more expressive than
> Eiffel’s. It also repairs obvious short-comings (a polite way of saying
> problems) with Eiffel’s.
>
> What you are missing is what you can do with macros.
>
>
> >
> > Restating my goals:
> >   • Specify pre-conditions and post-conditions as simple predicates
> (boolean expressions)
> >   • Selectively turn off contracts (mainly post-conditions) for
> performance in well-tested code.
>
> See Hoare above. See Macro above. See the Literature pointer in Ben’s
> message. We want you to take responsibility for taking the swim vest off.
>
>
> #lang racket
>
> (module server racket
>   (provide
>(contract-out
> (c% (class/c (field [x positive?]) (setter (->m number? number?))
>
>   (define c%
> (class object%
>   (super-new)
>   (field [x -1])
>   (define/public (setter x*) (begin0 x (set! x x*))
>
> (module client racket
>   (require (submod ".." server))
>
>   (define c (new c%))
>   (displayln `(the initial value does not have to live up to the field
> contract ,(send c setter 2)))
>   (with-handlers ([exn:fail:contract? (lambda (xn) (displayln `(you can't
> get away with bad sets)))])
> (send c setter 0)))
>
> (require 'client)

-- 
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 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 in the kind of
style I favor for expressing contracts. Then it will be interesting to see
how the readability compares.

Thanks also for pointing me to the paper on contracts — time for a re-read!

Dan

On Wed, May 3, 2017 at 1:57 PM, Ben Greenman 
wrote:

>
> 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" spec for the
> JavaScript left-pad function.
> https://www.npmjs.com/package/left-pad
>
> The exercise was fun, I learned a lot, and I think my solution is "as
> readable as possible" :) .
> https://github.com/bennn/racket-left-pad
>
>
> 2. "Oh Lord, Don't Let Contracts be Misunderstood" implements a little DSL
> on top of ->i contracts: http://www.ccs.neu.edu/racket/
> pubs/icfp16-dnff.pdf
>
>
>

-- 
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 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, which is great.

Once I've made another pass I'll include the error messages for critical
discussion.

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 invariants) they can get *really* expensive, negatively
impacting on user experience, which takes us into the land of pragmatic
trade-offs.

If I don't have a way to turn them off I'm either not going to write them
at all or comment them out, and then regret not using them on smaller test
scenarios.

Dan





On Wed, May 3, 2017 at 1:51 PM, Philip McGrath 
wrote:

> 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 (real-sqrt x)
>   (->i ([x (>=/c 0)])
>[rslt (x)
> (if (= 0 x)
> (=/c 0)
> (and/c (>=/c 0)
>(λ (rslt) (<= (abs (- x (* rslt rslt))) error])
>   "not even a number")
>
>
> The part of what you describe that has the least support in the Racket
> system is controlling the level of safety through a mechanism
> like pre-conditions-on/post-conditions-on. It would be easy enough to
> create a contract that is always satisfied if e.g. pre-conditions-on (which
> might be most Rackety to right as a parameter) is non-false, but I would
> suspect, at least in a case like this, you would already have paid most of
> the cost by getting into the contract system in the first place.
>
> The most typical solution, as Matthew illustrates, is to attach the
> contract at a module boundary with contract-out rather than a function
> boundary with define/contract, perhaps ultimately to attach it only to the
> public API of your library rather than for internals, and to leave off
> checks on the domains of functions (with the "any" contract) once you know
> they behave properly. Personally, though, having been annoyed once too
> often in tracking down an error that turned out to result from having
> changed the number of values a function returned, I'm happy to pay the
> price for good errors and trust the wonderful Racket implementers to keep
> the price as cheap as possible.
>
> Interestingly I had some trouble getting the nicely specific error
> messages you had in your example: I'll post about that separately.
>
> -Philip
>

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

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 we would accept a pull request on that one. 


>   • Proper support for invariant-checking


Well. It’s kind of there (see appended code at end) but not exactly. Eiffel has 
re-entry problems with invariants and Spec# cleaned this up a bit. We have a 
‘boundary philosophy’ (see beginning of Contract Guide and what I wrote there) 
and that is much cleaner but distinct from Eiffel for sure. 


>   • Proper support for covariant inheritance


That’s unsound so we did not want to go there. 


>   • Tools for automatically generating documentation

Good idea. We have bits and pieces for that. Nothing too useful. 


>   • Better tools for turning off contracts by configuration


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? 


> My questions are: 
>   • Is it feasible to get similar behaviour from the official contract 
> system?, or
>   • Do these considerations call for building up an alternative system?


Yes you can. Racket’s contract system is far more expressive than Eiffel’s. It 
also repairs obvious short-comings (a polite way of saying problems) with 
Eiffel’s. 

What you are missing is what you can do with macros. 


> 
> Restating my goals:
>   • Specify pre-conditions and post-conditions as simple predicates 
> (boolean expressions)
>   • Selectively turn off contracts (mainly post-conditions) for 
> performance in well-tested code.

See Hoare above. See Macro above. See the Literature pointer in Ben’s message. 
We want you to take responsibility for taking the swim vest off. 


#lang racket

(module server racket
  (provide
   (contract-out 
(c% (class/c (field [x positive?]) (setter (->m number? number?))

  (define c%
(class object%
  (super-new)
  (field [x -1])
  (define/public (setter x*) (begin0 x (set! x x*))

(module client racket
  (require (submod ".." server))
  
  (define c (new c%))
  (displayln `(the initial value does not have to live up to the field contract 
,(send c setter 2)))
  (with-handlers ([exn:fail:contract? (lambda (xn) (displayln `(you can't get 
away with bad sets)))])
(send c setter 0)))

(require 'client)

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

[Ben Greenman]

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" spec for the
JavaScript left-pad function.
https://www.npmjs.com/package/left-pad

The exercise was fun, I learned a lot, and I think my solution is "as
readable as possible" :) .
https://github.com/bennn/racket-left-pad


2. "Oh Lord, Don't Let Contracts be Misunderstood" implements a little DSL
on top of ->i contracts: http://www.ccs.neu.edu/racket/pubs/icfp16-dnff.pdf

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

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 (real-sqrt x)
  (->i ([x (>=/c 0)])
   [rslt (x)
(if (= 0 x)
(=/c 0)
(and/c (>=/c 0)
   (λ (rslt) (<= (abs (- x (* rslt rslt))) error])
  "not even a number")


The part of what you describe that has the least support in the Racket
system is controlling the level of safety through a mechanism
like pre-conditions-on/post-conditions-on. It would be easy enough to
create a contract that is always satisfied if e.g. pre-conditions-on (which
might be most Rackety to right as a parameter) is non-false, but I would
suspect, at least in a case like this, you would already have paid most of
the cost by getting into the contract system in the first place.

The most typical solution, as Matthew illustrates, is to attach the
contract at a module boundary with contract-out rather than a function
boundary with define/contract, perhaps ultimately to attach it only to the
public API of your library rather than for internals, and to leave off
checks on the domains of functions (with the "any" contract) once you know
they behave properly. Personally, though, having been annoyed once too
often in tracking down an error that turned out to result from having
changed the number of values a function returned, I'm happy to pay the
price for good errors and trust the wonderful Racket implementers to keep
the price as cheap as possible.

Interestingly I had some trouble getting the nicely specific error messages
you had in your example: I'll post about that separately.

-Philip

On Tue, May 2, 2017 at 9:22 PM, Matthew Butterick  wrote:

>
> 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 be
> zero"]
>   [(implies (> x 0) (> result 0)) "Positive numbers have positive
> square-roots"]
>   [(implies (> x 0) (<= (abs (- x (* result result))) 0.001))
>"result * result = x (to within error)"]))
>
>
>
> It sounds like you want alternate notation for stuff the contract system
> can already do.
>
> AFAICT the function below is equivalent to your function above. One could
> create a macro to go from one to the other:
>
>
> (define/contract (real-sqrt x)
>   (([x (and/c
> (or/c (λ (x) (real? x))
>   (curry raise-argument-error 'real-sqrt "real argument
> expected"))
> (or/c (λ (x) (>= x 0))
>   (curry raise-argument-error 'real-sqrt "non-negative
> argument expected")))])
>. ->i .
>[result (x)
>(cond
>  [(= x 0) (or/c (λ (result) (= result 0))
> (curry raise-result-error 'real-sqrt "sqrt of
> zero should be zero"))]
>  [(> x 0) (and/c
>  (or/c (λ (result) (> result 0))
>(curry raise-result-error 'real-sqrt
> "sqrt of positive number should be positive"))
>  (or/c (λ (result) (<= (abs (- x (* result
> result))) 0.0001))
>  (curry raise-result-error 'real-sqrt
> "result * result = x (to within error)")))])])
>   (sqrt x))
>
>
> Thinking more about the functional context, a macro — say (define/pre-post
> ...) that cleanly defined the following functions would be pretty sweet
> (continuing with the real-sqrt example):
>
>- real-sqrt-unsafe
>- real-sqrt-with-pre-conditions
>- real-sqrt-with-pre-and-post-conditions
>- real-sqrt (make-parameter one-of-the above)
>
>
> Rather than mint new identifiers, one could also export the function via
> multiple submodules, each of which has a different level of contracting.
> The advantage is that the "safety level" 1) can be adjusted by the caller,
> 2) without having to change the name of the identifier in the code. Again,
> this could all be automated through a macro:
>
> (begin
>   (define (real-sqrt x)
>  ;; no contract)
>   (provide real-sqrt)
>
>   (module+ precheck
> (provide (contract-out [real-sqrt precheck-contract ···])))
>
>   (module+ allchecks
> (provide (contract-out [real-sqrt allcheck-contract ···])))
> )
>
> And so on.
>
>
>
> --
> 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 

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

[Daniel Prager]

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 combinators in the
examples.

Your example is illuminating: I'll have a play with it and see if I can
figure out a suitable macro to reduce the boilerplate.

The use of module+ approach is good motivation to get more familiar with
the module system: back to Beautiful Racket for a refresher!

* * *

Thinking more about it, it also makes sense to reify contracts to allow
them to clip onto alternative implementations.

I'll come back later with some more code (unless someone beats me to it ;-).

* * *

I'm also interested in whether more people would use contracts routinely if
they were made a bit more accessible in terms of ease-of-use and making it
easy to turn them on and off.

When I used and advocated them first in the late 90s my colleagues thought
it was all too "bondage and discipline" so I went it alone.

When I was tech lead in naughties I corralled one team into using them to
good effect, but it required a degree of leadership and personal support.

Now, with the more widespread acceptance of unit tests and TDD, I wonder
whether they might be an easier "sell".


Dan



On Wed, May 3, 2017 at 12:22 PM, Matthew Butterick  wrote:

>
> 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 be
> zero"]
>   [(implies (> x 0) (> result 0)) "Positive numbers have positive
> square-roots"]
>   [(implies (> x 0) (<= (abs (- x (* result result))) 0.001))
>"result * result = x (to within error)"]))
>
>
>
> It sounds like you want alternate notation for stuff the contract system
> can already do.
>
> AFAICT the function below is equivalent to your function above. One could
> create a macro to go from one to the other:
>
>
> (define/contract (real-sqrt x)
>   (([x (and/c
> (or/c (λ (x) (real? x))
>   (curry raise-argument-error 'real-sqrt "real argument
> expected"))
> (or/c (λ (x) (>= x 0))
>   (curry raise-argument-error 'real-sqrt "non-negative
> argument expected")))])
>. ->i .
>[result (x)
>(cond
>  [(= x 0) (or/c (λ (result) (= result 0))
> (curry raise-result-error 'real-sqrt "sqrt of
> zero should be zero"))]
>  [(> x 0) (and/c
>  (or/c (λ (result) (> result 0))
>(curry raise-result-error 'real-sqrt
> "sqrt of positive number should be positive"))
>  (or/c (λ (result) (<= (abs (- x (* result
> result))) 0.0001))
>  (curry raise-result-error 'real-sqrt
> "result * result = x (to within error)")))])])
>   (sqrt x))
>
>
> Thinking more about the functional context, a macro — say (define/pre-post
> ...) that cleanly defined the following functions would be pretty sweet
> (continuing with the real-sqrt example):
>
>- real-sqrt-unsafe
>- real-sqrt-with-pre-conditions
>- real-sqrt-with-pre-and-post-conditions
>- real-sqrt (make-parameter one-of-the above)
>
>
> Rather than mint new identifiers, one could also export the function via
> multiple submodules, each of which has a different level of contracting.
> The advantage is that the "safety level" 1) can be adjusted by the caller,
> 2) without having to change the name of the identifier in the code. Again,
> this could all be automated through a macro:
>
> (begin
>   (define (real-sqrt x)
>  ;; no contract)
>   (provide real-sqrt)
>
>   (module+ precheck
> (provide (contract-out [real-sqrt precheck-contract ···])))
>
>   (module+ allchecks
> (provide (contract-out [real-sqrt allcheck-contract ···])))
> )
>
> And so on.
>
>

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

[Matthew Butterick]

> 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 be zero"]
>   [(implies (> x 0) (> result 0)) "Positive numbers have positive 
> square-roots"]
>   [(implies (> x 0) (<= (abs (- x (* result result))) 0.001))
>"result * result = x (to within error)"]))


It sounds like you want alternate notation for stuff the contract system can 
already do. 

AFAICT the function below is equivalent to your function above. One could 
create a macro to go from one to the other:


(define/contract (real-sqrt x)
  (([x (and/c
(or/c (λ (x) (real? x))
  (curry raise-argument-error 'real-sqrt "real argument expected"))
(or/c (λ (x) (>= x 0))
  (curry raise-argument-error 'real-sqrt "non-negative argument 
expected")))])
   . ->i .
   [result (x)
   (cond
 [(= x 0) (or/c (λ (result) (= result 0))
(curry raise-result-error 'real-sqrt "sqrt of zero 
should be zero"))]
 [(> x 0) (and/c
 (or/c (λ (result) (> result 0))
   (curry raise-result-error 'real-sqrt "sqrt 
of positive number should be positive"))
 (or/c (λ (result) (<= (abs (- x (* result 
result))) 0.0001))
 (curry raise-result-error 'real-sqrt 
"result * result = x (to within error)")))])])
  (sqrt x))


> Thinking more about the functional context, a macro — say (define/pre-post 
> ...) that cleanly defined the following functions would be pretty sweet 
> (continuing with the real-sqrt example):
> real-sqrt-unsafe
> real-sqrt-with-pre-conditions
> real-sqrt-with-pre-and-post-conditions
> real-sqrt (make-parameter one-of-the above)

Rather than mint new identifiers, one could also export the function via 
multiple submodules, each of which has a different level of contracting. The 
advantage is that the "safety level" 1) can be adjusted by the caller, 2) 
without having to change the name of the identifier in the code. Again, this 
could all be automated through a macro:

(begin
  (define (real-sqrt x)
 ;; no contract)
  (provide real-sqrt)

  (module+ precheck
(provide (contract-out [real-sqrt precheck-contract ···])))

  (module+ allchecks
(provide (contract-out [real-sqrt allcheck-contract ···])))
)

And so on.



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

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

[Daniel Prager]

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-conditions as simple
   predicates
   2. Being able to selectively turn off contracts (typically
   post-conditions) in well-tested code for performance.

With very simple hand-rolled assertions (plus some design discipline) I
reckon I achieved 80% pf the promise of contracts, with my debugging time
plunging by a factor of 10, and much cleaner designs.

When I finally programmed in Eiffel there were several added benefits of
language support that I appreciated:

   - More concise and clear expression of contracts
   - The implies operator
   - Proper support for invariant-checking
   - Proper support for covariant inheritance
   - Tools for automatically generating documentation
   - Better tools for turning off contracts by configuration

But I was only able to get to use Eiffel in one organisational setting —
quite a big negative!

* * *

Coming across to Racket I was thrilled to see that contracts are a big part
of the system, but they are certainly a bit different to what I was used to!

I'd like to share a sketch of how I would start to hand-roll the kind of
contracts I was used to in Racket.

My questions are:

   - Is it feasible to get similar behaviour from the official contract
   system?, or
   - Do these considerations call for building up an alternative system?


Restating my goals:

   1. Specify pre-conditions and post-conditions as simple predicates
   (boolean expressions)
   2. Selectively turn off contracts (mainly post-conditions) for
   performance in well-tested code.

Example: real square root function, and sketch of support below.

Now, I appreciate that the Racket contract system provides all sorts of
support for higher-level functional programming, but it concerns me that as
a big fan of contracts I've been reluctant to use them consistently in
Racket.

I hope to change that in my second decade of Racket (formerly PLT Scheme)
use, but may need some support and guidance!

Dan



#lang racket

(define pre-conditions-on #t)
(define post-conditions-on #t)

(define (implies a b)
  (or (not a) b))

(define-syntax-rule (pre [test? msg] ...)
  (unless (not pre-conditions-on)
(unless test?
  (error (~a "Pre-condition violation: " msg))) ...))

(define-syntax-rule (post [test? msg] ...)
  (unless (not post-conditions-on)
(unless test?
  (error (~a "Post-condition violation: " msg))) ...))

(define (real-sqrt x)
  (pre [(real? x) "real argument expected"]
   [(>= x 0) "non-negative argument expected"])

  (define result (sqrt x))
  ; Change the implementation to 1, 0, (- x) to trigger various
post-condition errors

  (post [(implies (= x 0) (= result 0)) "The sqrt of zero should be zero"]
[(implies (> x 0) (> result 0)) "Positive numbers have positive
square-roots"]
[(implies (> x 0) (<= (abs (- x (* result result))) 0.001))
 "result * result = x (to within error)"])
  result)


(real-sqrt 0)
(real-sqrt 9)
(real-sqrt -9) ; Pre-condition error

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