<div dir="ltr">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.)<div> </div><div>Robby</div></div><div class="gmail_extra"> <div class="gmail_quote">On Mon, Sep 9, 2013 at 7:14 PM, Eric Dobson <<a href="mailto:eric.n.dobson@gmail.com" target="_blank">eric.n.dobson@gmail.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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. <div class="HOEnZb"><div class="h5"> On Mon, Sep 9, 2013 at 10:57 AM, Sam Tobin-Hochstadt <<a href="mailto:samth@cs.indiana.edu">samth@cs.indiana.edu</a>> wrote: > On Mon, Sep 9, 2013 at 11:35 AM, Neil Toronto <<a href="mailto:neil.toronto@gmail.com">neil.toronto@gmail.com</a>> 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] >>> <a href="https://github.com/plt/racket/blob/master/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/numeric-tower.rkt#L107" target="_blank">https://github.com/plt/racket/blob/master/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/numeric-tower.rkt#L107</a> >>> [2] >>> <a href="https://github.com/plt/racket/blob/master/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt#L23" target="_blank">https://github.com/plt/racket/blob/master/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt#L23</a> >>> [3] >>> <a href="https://github.com/plt/racket/blob/master/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt#L51" target="_blank">https://github.com/plt/racket/blob/master/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt#L51</a> >>> >>> On Sat, Sep 7, 2013 at 3:20 PM, Neil Toronto <<a href="mailto:neil.toronto@gmail.com">neil.toronto@gmail.com</a>> >>> wrote: >>>> >>>> On 09/06/2013 04:14 PM, <a href="mailto:samth@racket-lang.org">samth@racket-lang.org</a> wrote: >>>>> >>>>> >>>>> 56b372c Sam Tobin-Hochstadt <<a href="mailto:samth@racket-lang.org">samth@racket-lang.org</a>> 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: > <a href="http://lists.racket-lang.org/dev" target="_blank">http://lists.racket-lang.org/dev</a> _________________________ Racket Developers list: <a href="http://lists.racket-lang.org/dev" target="_blank">http://lists.racket-lang.org/dev</a> </div></div></blockquote></div> </div>