Oh, I see. Yes, even better. Robby
On Sun, Jan 6, 2013 at 4:36 PM, Sam Tobin-Hochstadt <sa...@ccs.neu.edu>wrote: > 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 > <ro...@eecs.northwestern.edu> 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 <sa...@ccs.neu.edu> > > 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 > >> <ro...@eecs.northwestern.edu> 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 < > sa...@ccs.neu.edu> > >> > wrote: > >> >> > >> >> On Sun, Jan 6, 2013 at 3:23 PM, Robby Findler > >> >> <ro...@eecs.northwestern.edu> wrote: > >> >> > On Sun, Jan 6, 2013 at 2:18 PM, Sam Tobin-Hochstadt > >> >> > <sa...@ccs.neu.edu> > >> >> > 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 > >> > > >> > > > > > >
_________________________ Racket Developers list: http://lists.racket-lang.org/dev