[racket-dev] Motivation for polymorphic opaque types

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
<robby at 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 <samth at ccs.neu.edu>
> wrote:
>>
>> On Sun, Jan 6, 2013 at 3:23 PM, Robby Findler
>> <robby at eecs.northwestern.edu> wrote:
>> > On Sun, Jan 6, 2013 at 2:18 PM, Sam Tobin-Hochstadt <samth at 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
>
>