[racket-dev] Motivation for polymorphic opaque types

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
<robby at 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 <samth at 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
>> <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
>> >
>> >
>
>