<div dir="ltr">Oh, I see. Yes, even better.<div> </div><div>Robby</div><div> </div></div><div class="gmail_extra"> <div class="gmail_quote">On Sun, Jan 6, 2013 at 4:36 PM, Sam Tobin-Hochstadt <<a href="mailto:samth@ccs.neu.edu" target="_blank">samth@ccs.neu.edu</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Right -- if we (the typed code) are picking the instantiation, then we have to check structurally, to make sure that it's really got integers everywhere. But if it's a plain type parameter, then the untyped side gets to pick it, and WLOG they could pick `Any`, meaning that there's no wrong values they could supply. That means that as long as they supply a `kons`, it must meet the contract of `(Kons A)`. So I think the contract can be much cheaper in this one specific case, which fortunately is the case that Neil cares about, I think. Sam On Sun, Jan 6, 2013 at 5:28 PM, Robby Findler <div class="HOEnZb"><div class="h5"><<a href="mailto:robby@eecs.northwestern.edu">robby@eecs.northwestern.edu</a>> wrote: > Oh-- I think you're right that the type parameter can matter (it could go > over to R as an Integer list and come back as a Boolean list or something). > > Robby > > > On Sun, Jan 6, 2013 at 4:08 PM, Sam Tobin-Hochstadt <<a href="mailto:samth@ccs.neu.edu">samth@ccs.neu.edu</a>> > wrote: >> >> Sorry, that was very silly of me. That isn't what's happening at all, >> because type soundness means we don't need to enforce the >> parametricity at all. >> >> The actual relevant program is: >> >> (module m racket >> (struct kons (a d)) >> (struct mt ()) >> (define MT (mt)) >> (define (FST v) >> (when (eq? MT v) (error 'empty)) >> (kons-a v)) >> (define (RST v) >> (when (eq? MT v) (error 'empty)) >> (kons-d v)) >> (define (LST . x) >> (if (empty? x) >> MT >> (kons (first x) (apply LST (rest x))))) >> (define (LST/C elem/c) >> (define C (recursive-contract >> (or/c (λ (v) (eq? v MT)) >> (struct/dc kons [a elem/c] [d C])))) >> C) >> (provide/contract >> [LST (->* () #:rest any/c (LST/C any/c))] >> [FST (-> (LST/C any/c) any/c)] >> [RST (-> (LST/C any/c) (LST/C any/c))]) >> ) >> >> However, thinking about this more, it's an invariant that `kons` >> structures are always correctly constructed, and we can rely on them >> to have *some* instantiation that typechecks -- that's why the `any/c` >> is ok. That suggests to me that contract generation for a struct type >> applied to simple type variables can always be just the predicate for >> that type, which would make Neil very happy. I want to think about >> this more before I'm sure, though. >> >> Thanks for being patient while I get this wrong in various ways ... >> Sam >> >> On Sun, Jan 6, 2013 at 4:13 PM, Robby Findler >> <<a href="mailto:robby@eecs.northwestern.edu">robby@eecs.northwestern.edu</a>> wrote: >> > This has a non-chaperone contract being used in a struct/c, I think? >> > >> > (FST (LST 1 2 3)) => struct/dc: expected chaperone contracts, but field >> > a >> > has #<barrier-contract> >> > >> > Robby >> > >> > >> > On Sun, Jan 6, 2013 at 2:40 PM, Sam Tobin-Hochstadt <<a href="mailto:samth@ccs.neu.edu">samth@ccs.neu.edu</a>> >> > wrote: >> >> >> >> On Sun, Jan 6, 2013 at 3:23 PM, Robby Findler >> >> <<a href="mailto:robby@eecs.northwestern.edu">robby@eecs.northwestern.edu</a>> wrote: >> >> > On Sun, Jan 6, 2013 at 2:18 PM, Sam Tobin-Hochstadt >> >> > <<a href="mailto:samth@ccs.neu.edu">samth@ccs.neu.edu</a>> >> >> > wrote: >> >> >> >> >> >> > The boundaries have the information; that's how the contracts got >> >> >> > inserted >> >> >> > in the first place. >> >> >> >> >> >> No, the contracts are parametric contracts using `parametric->/c`, >> >> >> and >> >> >> thus don't have any information about the types used at all. >> >> > >> >> > >> >> > I don't see why you can't tag them when something at a boundary and >> >> > then >> >> > check that something at another boundary instead of doing some deep >> >> > check. >> >> >> >> The problem is that I don't know what to tag them *with*. >> >> >> >> Consider the following program: >> >> >> >> #lang racket >> >> >> >> (struct kons (a d)) >> >> (struct mt ()) >> >> (define MT (mt)) >> >> (define (FST v) >> >> (when (eq? MT v) (error 'empty)) >> >> (kons-a v)) >> >> (define (RST v) >> >> (when (eq? MT v) (error 'empty)) >> >> (kons-d v)) >> >> (define (LST . x) >> >> (if (empty? x) >> >> MT >> >> (kons (first x) (apply LST (rest x))))) >> >> (define (LST/C elem/c) >> >> (define C (recursive-contract >> >> (or/c (λ (v) (eq? v MT)) >> >> (struct/c kons elem/c C)))) >> >> C) >> >> (provide/contract >> >> [LST (parametric->/c (A) (->* () #:rest A (LST/C A)))] >> >> [FST (parametric->/c (A) (-> (LST/C A) A))] >> >> [RST (parametric->/c (A) (-> (LST/C A) (LST/C A)))]) >> >> >> >> This is the essence of Neil's polymorphic list program, as implemented >> >> by Typed Racket. I don't know how to change those contracts to not be >> >> really expensive, because I can't pick the instantiation of A at >> >> runtime to tag the structure instances with. >> >> >> >> Sam >> > >> > > > </div></div></blockquote></div> </div>