Re: ->i applies contract projections multiple times?

> On Dec 14, 2016, at 3:56 PM, Scott Moore <[email protected]> wrote:
> 
> 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

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

John



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