# [racket-users] Error reporting with (flat?) contracts

```While trying to express in the contract system Daniel Prager's check that a
possibly-buggy square root function actually returns the square root of its
argument (and in particular the nice error messages, I ran into a few
things that weren't quite as I expected.```
```
My first attempt, using flat-contract-with-explanation, looks like this:

(define/contract (squares-to/within/c x error)
(-> (>=/c 0) (>=/c 0) flat-contract?)
(flat-contract-with-explanation
(λ (rslt)
(cond
[(not (real? rslt))
(λ (blame)
(raise-blame-error
blame rslt
'(expected: "real?" given: "~e")
rslt))]
[(<= (abs (- x (* rslt rslt)))
error)
#t]
[else
(λ (blame)
(raise-blame-error
blame rslt
'(expected:
"a number that squares to ~e ± ~e"
given: "~e"
"\n  " given " squared:  ~e")
x error rslt (* rslt rslt)))]))))

(define/contract (buggy-sqrt x)
(->i ([x (>=/c 0)])
[rslt (x)
(if (= 0 x)
(=/c 0)
(and/c (>/c 0)
(squares-to/within/c x 0.0000001)))])
1)

(Aside: I noticed that despite this thread, flat-contract-with-explanation
still does not accept a #:name argument, or at least not in 6.9.)

Given the above, (buggy-sqrt 4) produces this fairly unhelpful error
message, including none of the nice reporting:

buggy-sqrt: broke its own contract
promised: (and/c (and/c real? positive?) anonymous-flat-contract)
produced: 1
in: the rslt result of
(->i
((x (and/c real? (not/c negative?))))
(rslt
(x)
(if (= 0 x)
(=/c 0)
(and/c
(>/c 0)
(squares-to/within/c x 1e-07)))))
contract from: (function buggy-sqrt)
blaming: (function buggy-sqrt)
(assuming the contract is correct)
at: unsaved-editor:26.18

I then tried dropping down to make-flat-contract like this:

(define/contract (squares-to/within/c-v2 x error)
(-> (>=/c 0) (>=/c 0) flat-contract?)
(make-flat-contract
#:name `(squares-to/within/c-v2 ,x ,error)
#:first-order (λ (rslt)
(and (real? rslt)
(<= (abs (- x (* rslt rslt)))
error)))
#:late-neg-projection
(λ (blame)
(λ (rslt neg-party)
(cond
[(not (real? rslt))
(raise-blame-error
blame rslt #:missing-party neg-party
'(expected: "real?" given: "~e")
rslt)]
[(<= (abs (- x (* rslt rslt)))
error)
rslt]
[else
(raise-blame-error
blame rslt #:missing-party neg-party
'(expected:
"a number that squares to ~e ± ~e"
given: "~e"
"\n  " given " squared:  ~e")
x error rslt (* rslt rslt))])))))

(define/contract (buggy-sqrt-v2 x)
(->i ([x (>=/c 0)])
[rslt (x)
(if (= 0 x)
(=/c 0)
(and/c (>/c 0)
(squares-to/within/c-v2 x 0.0000001)))])
1)

but (buggy-sqrt-v2 4) gives this error:

buggy-sqrt-v2: broke its own contract
promised: (and/c (and/c real? positive?) (squares-to/within/c-v2 4 1e-07))
produced: 1
in: the rslt result of
(->i
((x (and/c real? (not/c negative?))))
(rslt
(x)
(if (= 0 x)
(=/c 0)
(and/c
(>/c 0)
(squares-to/within/c-v2 x 1e-07)))))
contract from: (function buggy-sqrt-v2)
blaming: (function buggy-sqrt-v2)
(assuming the contract is correct)
at: unsaved-editor:67.18

which is improved only in that it includes a name: it still doesn't use the
nice error message I programed in, and it doesn't even tell me which case
of the and/c failed (though that is fairly obvious in this case).

Just for completeness, I also tried a struct, like so:

(struct squares-to/within-contract (x error)
#:property prop:custom-write contract-custom-write-property-proc
#:property prop:flat-contract
(build-flat-contract-property
#:name
(match-lambda
[(squares-to/within-contract x error)
`(squares-to/within/c-v3 ,x ,error)])
#:first-order
(match-lambda
[(squares-to/within-contract x error)
(λ (rslt)
(and (real? rslt)
(<= (abs (- x (* rslt rslt)))
error)))])
#:late-neg-projection
(match-lambda
[(squares-to/within-contract x error)
(λ (blame)
(λ (rslt neg-party)
(cond
[(not (real? rslt))
(raise-blame-error
blame rslt #:missing-party neg-party
'(expected: "real?" given: "~e")
rslt)]
[(<= (abs (- x (* rslt rslt)))
error)
rslt]
[else
(raise-blame-error
blame rslt #:missing-party neg-party
'(expected:
"a number that squares to ~e ± ~e"
given: "~e"
"\n  " given " squared:  ~e")
x error rslt (* rslt rslt))])))])))

(define/contract (squares-to/within/c-v3 x error)
(-> (>=/c 0) (>=/c 0) flat-contract?)
(squares-to/within-contract x error))

(define/contract (buggy-sqrt-v3 x)
(->i ([x (>=/c 0)])
[rslt (x)
(if (= 0 x)
(=/c 0)
(and/c (>/c 0)
(squares-to/within/c-v3 x 0.0000001)))])
1)

but (buggy-sqrt-v3 4) was like (buggy-sqrt-v2 4) except for the version
number.

I would also note that using the contract in e.g.

(define/contract buggy
(and/c number? (squares-to/within/c-v3 4 0.0000001))
1)

gives the nice error I wanted:

../../Applications/Racket v6.9/collects/racket/private/kw.rkt:1170:47:
buggy: broke its own contract
promised: a number that squares to 4 ± 1e-07
produced: 1
produced squared:  1
in: an and/c case of
(and/c
number?
(squares-to/within/c-v3 4 1e-07))
contract from: (definition buggy)
blaming: (definition buggy)
(assuming the contract is correct)
at: unsaved-editor:131.17

The error message just seems to be lost with some subset of combinators,
evidently including ->i.

-Philip

---------- Forwarded message ----------
From: Daniel Prager <daniel.a.pra...@gmail.com>
Date: Tue, May 2, 2017 at 5:01 PM
Subject: [racket-users] Apropos contracts: simple predicates and switching
on and off

#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.0000001))
"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