[racket-dev] Motivation for polymorphic opaque types

I think this "specific case" covers pretty much every abstract data type 
written in Typed Racket, including all those exported by PFDS and 
math/array. (Well, the RAList type in PFDS would have to wrap its lists 
of roots in a struct to get great performance in untyped Racket instead 
of just good performance.) In math/array, in particular, there are only 
a few instances in which the typed code instantiates the Array type, all 
having to do with conversions to and from FlArray and FCArray.

Yes, this would make me very happy. :)

Neil ⊥

On 01/06/2013 03:36 PM, Sam Tobin-Hochstadt 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
> <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
>>>>
>>>>
>>
>>