Re: ->i applies contract projections multiple times?

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


On Thu, Dec 15, 2016 at 4:05 PM, Alexis King <[email protected]> wrote:
> 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.
>
> --
> 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-/JYPxA39Uh5TLH3MbocFF+G/[email protected]
> 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+unsubscribe-/JYPxA39Uh5TLH3MbocFF+G/[email protected]
For more options, visit https://groups.google.com/d/optout.