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] break-thread + thread-wait can't be handled

[Ryan Culpepper]

On 5/3/17 10:41 PM, Eric Griffis wrote:

Hello,

I'm having trouble catching "terminate break" exceptions when combining 
break-thread with thread-wait.

MWE 1:

  (with-handlers ([exn:break:terminate? writeln])
(let ([t (thread (lambda () (thread-wait (current-thread])
  (break-thread t 'terminate)
  (thread-wait t)))


Threads do not inherit exception handlers. You need to move the 
`with-handlers` to the new thread:


  (let ([t (thread (lambda ()
 (with-handlers ([exn:break:terminate? writeln])
   (thread-wait (current-thread)])
(break-thread t 'terminate)
(thread-wait t))

Except that isn't quite right either, because , the main thread might 
(very likely) send the break to `t` before `t` is ready to catch it. So 
we need some additional synchronization:


  (define t-ready (make-semaphore 0))
  (let ([t (thread (lambda ()
 (with-handlers ([exn:break:terminate? writeln])
   (semaphore-post t-ready)
   (thread-wait (current-thread)])
(semaphore-wait t-ready)
(break-thread t 'terminate)
(thread-wait t))

That version should reliably print out the break exception.

Ryan

--
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] break-thread + thread-wait can't be handled

[Eric Griffis]

Hello,

I'm having trouble catching "terminate break" exceptions when combining 
break-thread with thread-wait.

MWE 1:

  (with-handlers ([exn:break:terminate? writeln])
(let ([t (thread (lambda () (thread-wait (current-thread])
  (break-thread t 'terminate)
  (thread-wait t)))

MWE 2:

  (with-handlers ([exn:break:terminate? writeln])
(let ([t (thread (lambda () (thread-receive)))])
  (break-thread t 'terminate)
  (thread-wait t)))

Expected:

  #(struct:exn:break:terminate "terminate break" # 
#)

Actual:

  terminate break

FWIW, the following snippet works as expected:

  (with-handlers ([exn:break:terminate? writeln])
(break-thread (current-thread) 'terminate))

Am I missing something? Any help is appreciated.

Eric

-- 
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] Webserver HTTP 2

[Jay McCarthy]

I am very confident that it will eventually support it. ;)

However, I have no current plans to go implement it. It's on my long
list of things to eventually get to, but is not blocking me on any
other things. If someone else were passionate about it, I'd be happy
to help them get started, etc.

Jay

On Wed, May 3, 2017 at 4:42 AM, Sean Kemplay  wrote:
> Hello,
>
> Does anyone know if the Racket webserver will support http2 at any stage?
>
> Kind regards,
> Sean
>
> --
> 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.



-- 
-=[ Jay McCarthy   http://jeapostrophe.github.io]=-
-=[ Associate ProfessorPLT @ CS @ UMass Lowell ]=-
-=[ Moses 1:33: And worlds without number have I created; ]=-

-- 
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] How to improve compile times?

[Daniel Brunner]

Am 28.04.2017 um 08:07 schrieb Alex Harsanyi:

> 
> In the end, the start up time does not bother me too much, as it is a GUI 
> application and I spend a lot of time using it after starting it up, so the 7 
> second wait is acceptable. I have other, more interesting, application 
> features to work on anyway :-)
> 

As one of the users of ActivityLog2 I do not mind the startup time either.

Best wishes,
Daniel

-- 
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] Webserver HTTP 2

[Sean Kemplay]

Hello,

Does anyone know if the Racket webserver will support http2 at any stage?

Kind regards,
Sean

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