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 <m...@mbtype.com> wrote:
>
> 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 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.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:
>
> (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 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.
