> On May 2, 2017, at 4:33 PM, Daniel Prager <daniel.a.pra...@gmail.com> 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.0000001))
>            "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 
   . ->i .
   [result (x)
             [(= 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.00000001))
                                     (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:

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

Reply via email to