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