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

Reply via email to