->i applies contract projections multiple times?

[Alexis King]

This question comes from someone else on Stack Overflow, which they
asked here: http://stackoverflow.com/q/41144374/465378

I think it’s likely that the people who can answer this are probably
only on the mailing list, though, so I figured I’d ask it here.

Basically, the ->i contract applies contract projections more than
once, despite the fact that it seems unnecessary. Here’s the example
provided in the question:

(define/contract (foo x y z)
(->i ([x (λ (x) (begin (displayln 0) #t))]
[y (x) (λ (y) (begin (displayln 1) #t))]
[z (x y) (λ (z) (begin (displayln 2) #t))])
any)
#t)

(foo 1 2 3)

The above example prints the following when run:

0
0
1
1
2
#t

This indicates that values used dependently for determining other
contracts cause their contracts to be applied more than once. The
above example only uses flat contracts, but I tested with a
side-effectful impersonator contract and got the same result.

After some very simple pondering, I couldn’t come up with a situation
in which applying the contracts more than once would be necessary,
and this could obviously have a performance penalty given that ->i
is already a fairly slow contract. Is this a bug in ->i, or is it
necessary or intentional behavior? If the latter, why is it necessary?

Alexis

[Robby Findler]

I think it could be possible to avoid those printfs but only because
the contracts used here are flat, but the implementation of ->i
doesn't do that specialization. In the general case, the contract on
each of the depended on arguments (x and y in this case) have to be
applied twice, once to catch errors in the contract itself and once to
catch errors in the body of the function. (So if you'd used
impersonator contracts, we'd have to see multiple printouts.)

The fact that this code prints "y" twice is related, but more
obviously a bug to be fixed.

#lang racket
(define/contract f
(->i ([x any/c]
[y (x) (begin (printf "y\n") any/c)]
[z (x y) (begin (printf "z\n") any/c)])
any)
(λ args 0))
(f 1 2 3)

Robby

> --
> 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...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Scott Moore]

Robby beat me to it. For a longer discussion, see Christos, Robby, Cormac and Matthias’ paper: http://www.ccs.neu.edu/racket/pubs/popl11-dfff.pdf on the difference between dependent (->d) and indy-dependent contracts (->i).

A contrived example of why this is better is:

(define/contract (foo x y)

  (->d ([x (λ (x) (y ‘evil) #t)]

        [y (-> integer? integer?)])

       [result any/c])

  void)

(foo 0 (λ (x) (+ x 1)))

> +: contract violation   !!! Whoops, but I promised to only call y with integers!

  expected: number?

  given: 'evil

  argument position: 1st

  other arguments…:

vs:

(define/contract (foo x y)

  (->i ([x (y) (λ (x) (y 'evil) #t)]

        [y (-> integer? integer?)])

       [result any/c])

  void)

(foo 0 (λ (x) (+ x 1)))

foo: broke its own contract  !!! Much better :)

  promised: integer?

  produced: 'evil

  in: the 1st argument of

      the y argument of

      (->i

       ((x (y) (λ (x) (y 'evil) #t))

        (y (-> integer? integer?)))

       (result any/c))

  contract from: anonymous-module

  blaming: anonymous-module

   (assuming the contract is correct)

  at: unsaved-editor:3.18

['John Clements' via users-redirect]

Nice example. Just the right size to read and understand. Many thanks!

John

[Robby Findler]

I've pushed a fix for this and the related bug that I mentioned in
this thread. No important performance improvements, however (I believe
most of the time in ->i microbenchmarks is spent in just piping things
around, not doing the actual contract checking).

Robby


On Wed, Dec 14, 2016 at 5:33 PM, Alexis King <lexi....@gmail.com> wrote:

[Alexis King]

Many thanks to both of you for the explanation and examples. I admit
I’ve seen that paper before, but I haven’t really taken the time
to understand it. I haven’t spent the effort to understand all the
notation being used, so much of the paper is pretty opaque to me.
Maybe once I get some time I’ll sift through it more carefully, but
in the meantime, Scott’s example helps a lot to demonstrate what
indy dependent contracts actually do.

However, from a practical implementation perspective, I’m still a
little confused about why the contract needs to be applied twice.
Given that Racket uses the +indy semantics, it seems like the blame
provided is identical for both cases, so it seems like the contracts
should only need to be applied once. For Scott’s example, the
contract for the y argument needs to be applied such that if it is
misused within the function body, then it blames foo, and if it is
misused within the contract itself, it also blames foo.

If ->i used the indy or -indy semantics (though admittedly I don’t
get why the -indy semantics would ever be useful), I would understand
why the contract would need to be applied twice, since the blame
would be different. Given the way Racket handles things, though, I
don’t really understand what I’m missing.

[Ben Greenman]

There are 3 parties that could be blamed:

1. the context that calls `foo`

2. the function `foo`

3. the contract on `foo`

--
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+unsubscribe@googlegroups.com.

[Robby Findler]

Perhaps the contract implementation could notice that the indy blame
parties and the normal blame parties are the same and thus avoid the
second contract. Given today's experience I'm not sure it is worth
bothering, at least until other things improve in the contract
implementation.

But if you want to know more about how they could be different, you
might want to consider this example from section 1 of the paper. It
will (randomly) assign blame to any of the three submodules.

#lang racket
(module m1 racket
(provide
(contract-out
[deriv-contract
contract?]))

(define n 100)
(define δ 0.01)

(define deriv-contract
(->i ([f (-> real? real?)][ε real?])
(fp (-> real? real?))
#:post (f ε fp)
(for/and ([i (in-range 0 n)])
(define x (random-number))
(define slope
(/ (- (f (- x ε)) (f (+ x ε)))
(* 2 ε)))
(<= (abs (- slope (fp x))) δ))))

(define (random-number)
(case (random 10)
[(0) 1+1i]
[(1) 100]
[else (random)])))

(module m2 racket
(require (submod ".." m1))
(provide (contract-out [deriv deriv-contract]))
(define (deriv f ε)
(λ (x)
(if (> x 1)
(f #f)
(f x)))))

(module m3 racket
(require (submod ".." m2))
(deriv (λ (x) (if (<= x 1) x #f)) 0.))

(require 'm3)


Robby

[Alexis King]

> On Dec 15, 2016, at 3:16 PM, Robby Findler <ro...@eecs.northwestern.edu> wrote:
>
> But if you want to know more about how they could be different, you
> might want to consider this example from section 1 of the paper. It
> will (randomly) assign blame to any of the three submodules.

Hmm. That example is helpful to see, but I’m still a little confused.
How is its behavior any different from a picky dependent contract?
It seems to me like that behavior would be the same, but I can’t
know for sure, since Racket does not provide a picky dependent
contract combinator.

[Robby Findler]

On Fri, Dec 16, 2016 at 11:49 AM, Alexis King <lexi....@gmail.com> wrote:
>> On Dec 15, 2016, at 3:16 PM, Robby Findler <ro...@eecs.northwestern.edu> wrote:
>>
>> But if you want to know more about how they could be different, you
>> might want to consider this example from section 1 of the paper. It
>> will (randomly) assign blame to any of the three submodules.
>
> Hmm. That example is helpful to see, but I’m still a little confused.
> How is its behavior any different from a picky dependent contract?

Picky would never assign blame to m1. The places where m1 would be
blamed would instead fall on, I think, m2.

> It seems to me like that behavior would be the same, but I can’t
> know for sure, since Racket does not provide a picky dependent
> contract combinator.

It wouldn't be too difficult to break the current ->i to get something
that behaves like picky if you want to experiment, but really the
difference is that indy brings in the third party. That third party
replaces the negative party for uses of the values that are depended
on (so, in the example, the two blame parties for the uses `f` and
`fp` in m1 are m1 and m3, but the two parties for uses of `f` in m2
are m2 and m3 -- picky just always uses m2/m3).

Robby

[Alexis King]

> On Dec 16, 2016, at 9:53 AM, Robby Findler <ro...@eecs.northwestern.edu> wrote:
>
> Picky would never assign blame to m1. The places where m1 would be
> blamed would instead fall on, I think, m2.

Ahh, I see. I was confused because I wasn’t paying enough attention
to the blame information in the error message, only at the beginning
of the message which varied between “contract violation” and “broke
its own contract”. When m1 is blamed, I would have expected some
other message, but I guess it makes sense based on the semantics
being used.

Thank you for your patience and your explanation; I think I understand
what’s going on now, at least at a high level.

Alexis

[Robby Findler]

On Fri, Dec 16, 2016 at 12:20 PM, Alexis King <lexi....@gmail.com> wrote:
>> On Dec 16, 2016, at 9:53 AM, Robby Findler <ro...@eecs.northwestern.edu> wrote:
>>
>> Picky would never assign blame to m1. The places where m1 would be
>> blamed would instead fall on, I think, m2.
>
> Ahh, I see. I was confused because I wasn’t paying enough attention
> to the blame information in the error message, only at the beginning
> of the message which varied between “contract violation” and “broke
> its own contract”. When m1 is blamed, I would have expected some
> other message, but I guess it makes sense based on the semantics
> being used.

The error messages could certainly be improved. If you want to have a
hack at it, the relevant code is here (unless there is information
that needs to make its way there):

https://github.com/racket/racket/blob/master/racket/collects/racket/contract/private/blame.rkt#L159

One thing we decided a while back was to put the " (blaming ...)"
near the end, but the blame information is taken into account in that
first line. Perhaps there should be a more refined piece of code that
computes that first line in this case, tho?

> Thank you for your patience and your explanation; I think I understand
> what’s going on now, at least at a high level.

:)

Robby

[Matthias Felleisen]

> One thing we decided a while back was to put the " (blaming ...)"
> near the end, but the blame information is taken into account in that
> first line. Perhaps there should be a more refined piece of code that
> computes that first line in this case, tho?

On Thursday, NWU-Max gave a bb talk at NEU on blame in the TR/R case.
It was more or less a categorical analysis of the Wadler-Findler paper that
says “we should always blame both parties involved, plus the spec”, which
would mean contract here. (His analysis points out an asymmetry in WF,
which is — in his framework — a symptom of a mistake.)

It was of course music in my ears to hear this. Christos pointed out that
Max’s suggested fix could be generalized so that a contracted value
keeps track of all crossed boundaries and the error system could report
those crossings to help the developer even more. After all if A is blamed,
fixing A may just move the bug to B and then to C and then to D.

The cost is high (wrapped information goes). But if we could validate
the conjecture practically, it would neat generalize this error message
and finally wrap up the first NSF on contracts :)

— Matthias