[racket-dev] Motivation for polymorphic opaque types

Oh, I see. Yes, even better.

Robby



On Sun, Jan 6, 2013 at 4:36 PM, Sam Tobin-Hochstadt <samth at 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
> <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
> >> >
> >> >
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20130106/c4770805/attachment.html>