[racket-dev] [plt] Push #27446: master branch updated

FWIW, this is something that's been studied in small calculi in the
literature. Nothing that will have to get thru all of the little details
that you have to get right to make it work in a real language design like
TR, but maybe you'll find some useful ways to look at the problem. (Mostly
the papers I'm thinking of have Jeremy Siek as a co-author but there are
others, including our own Sam.)

Robby


On Mon, Sep 9, 2013 at 7:14 PM, Eric Dobson <eric.n.dobson at gmail.com> wrote:

> I have ideas to remove about the contracts from TR code, but currently
> that is only prototyped.
>
> Example:
>
> #lang typed/racket
> (provide f)
> (: f (Number -> Number))
> (define (f x) x)
>
> Currently f is exported with the contract (number? . -> . number?),
> but this can be safely reduced to (number . -> . any). This is because
> the return value contract is checking things we have already ensured
> statically. IIRC checking return values of functions is much more
> expensive than just arguments, so this should reduce the cost of TR
> boundary cost, but I don't have any numbers.
>
> On Mon, Sep 9, 2013 at 10:57 AM, Sam Tobin-Hochstadt
> <samth at cs.indiana.edu> wrote:
> > On Mon, Sep 9, 2013 at 11:35 AM, Neil Toronto <neil.toronto at gmail.com>
> wrote:
> >> Nice, and thanks for the explanation. Just to make sure I get it: does
> this
> >> mean fully expanded TR modules are smaller?
> >
> > Yes.
> >
> >> Does it reduce the number of generated contracts?
> >
> > No.
> >
> >>
> >>
> >> On 09/08/2013 12:24 PM, Sam Tobin-Hochstadt wrote:
> >>>
> >>> Typed Racket has to expand into code that registers the type of each
> >>> module-top-level identifier in the global environment so that other
> >>> modules can find the types to typecheck with.  For example, this
> >>> program:
> >>>
> >>> #lang typed/racket
> >>> (provide x)
> >>> (define: x : Integer 1)
> >>>
> >>> expands into (greatly simplified):
> >>>
> >>> #lang ...
> >>> (#%provide x)
> >>> (begin-for-syntax
> >>>    (declare #'x Integer-rep))
> >>> (define-values (x) 1)
> >>>
> >>> but what is `Integer-rep`?  It needs to be an expression that
> >>> _constructs_ the internal Typed Racket representation of the `Integer`
> >>> type. Previously, that looked something like this:
> >>>
> >>>      (make-Union (sort (list Negative-Fixnum-rep Positive-Fixnum-rep
> >>> ...)))
> >>>
> >>> and so on and so forth for the components, all the way down to base
> >>> types.  You can imagine how this gets quite large, especially for
> >>> large types.
> >>>
> >>> However, this is wasteful, because every Typed Racket program, at type
> >>> checking time, defines a constant that's the representation of the
> >>> `Integer` type, right here [1]. So instead of serializing an
> >>> expression that constructs the same thing as `-Int`, we can just
> >>> *reference* `-Int` in the expanded code.  To make that possible, Typed
> >>> Racket now builds a hash table [2] mapping types (really, their
> >>> representations) to identifiers that denote those types. Then the
> >>> serializer just consults this table [3].
> >>>
> >>> It turns out that base types (but no others) already used basically
> >>> this mechanism, by storing the identifier *in* the type
> >>> representation.  But that's now obsolete, and thus was removed in my
> >>> subsequent commit.
> >>>
> >>> As a result, the type serialization is much smaller.
> >>>
> >>> [1]
> >>>
> https://github.com/plt/racket/blob/master/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/numeric-tower.rkt#L107
> >>> [2]
> >>>
> https://github.com/plt/racket/blob/master/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt#L23
> >>> [3]
> >>>
> https://github.com/plt/racket/blob/master/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt#L51
> >>>
> >>> On Sat, Sep 7, 2013 at 3:20 PM, Neil Toronto <neil.toronto at gmail.com>
> >>> wrote:
> >>>>
> >>>> On 09/06/2013 04:14 PM, samth at racket-lang.org wrote:
> >>>>>
> >>>>>
> >>>>> 56b372c Sam Tobin-Hochstadt <samth at racket-lang.org> 2013-09-06 14:22
> >>>>> :
> >>>>> | Remember types that are defined, and use them in serialization.
> >>>>> |
> >>>>> | This extends a facility already available for base types,
> >>>>> | making that facility no longer strictly needed.
> >>>>> |
> >>>>> | Shrinks the zo size for the `math` package by almost 1MB.
> >>>>> :
> >>>>>     M .../typed-racket/env/init-envs.rkt                |   1 +
> >>>>>     M .../typed-racket/typecheck/def-export.rkt         |   7 +-
> >>>>>     M .../typed-racket/typecheck/tc-toplevel.rkt        |  31 +++---
> >>>>>     M .../typed-racket/types/abbrev.rkt                 |  36 +++----
> >>>>>     M .../typed-racket/types/base-abbrev.rkt            |  12 ++-
> >>>>>     M .../typed-racket/types/numeric-tower.rkt          | 108
> >>>>> +++++++++----------
> >>>>
> >>>>
> >>>>
> >>>> Would you mind explaining this a little more? It sounds interesting,
> and
> >>>> the
> >>>> commit almost has my name in it. :)
> >>>>
> >>>> Neil ⊥
> >>>>
> >>
> >
> > _________________________
> >   Racket Developers list:
> >   http://lists.racket-lang.org/dev
>
> _________________________
>   Racket Developers list:
>   http://lists.racket-lang.org/dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20130909/61dedd84/attachment.html>