Re: [racket-dev] [plt] Push #28817: master branch updated
Let me spell out my cryptic comment. 1. I said that a bunch of optimizations are simple context-free rewrite rules. 2. I also said that what we really need to keep track of contexts. If you think of Γ ⊢ e ~ e' if Γ ⊨ e ~ e' as the general form of optimizing rewrites, then the key generalization over 2 is the context Γ. 3. Matthew calls this 'type inference' because that's where Γs like the above are most common. But Γ could also contain statements such as 'f = \x.e, f \not∈ AV(P)' which then gives rise to inlining. [Optimizations really are about the logic of the program, if you want sound ones.] 4. In general optimizers gather a lot of knowledge about contexts that they exploit, and front-ends do so mostly for type checking reasons. That's why the two are often conflated. But you really do want more than type info in the context. 5. Our current major problem is that the type checker does not communicate the type checking information from the front end to the optimizer. The general formulation is that #lang-languages have only a few hooks to tell the compiler what they figured out. 6. Now in this context, my Perhaps remark means two distinct things: -- it would be wonderful if we could centralize rewriting rules in one place through one mechanism, and syntax-* looks promising That does not mean that these things are part of the program. I could see using some syntax-* used to generate code for the current optimizer. [I know that this is a stretch.] -- it would be even wonderfuller if (a) this centralized mechanism came with a mechanism for collecting context information and (b) if #lang languages had a mechanism to communicate the contextual information they have gathered to this central rewriter. This would avoid leakage [citation to Julia omitted] Does this make sense? Okay I understand that I am laying out a research agenda to improve our infrastructure. Don't bother to tell me, I know. It's my job. Now I have to look for someone who wishes to write this very real dissertation. -- Matthias On May 28, 2014, at 10:50 PM, Eric Dobson eric.n.dob...@gmail.com wrote: Cases like this make me think that we need something stronger than context free rewrite rules over the ast/bytecode. On May 29, 2014, at 1:19 AM, Matthew Flatt mfl...@cs.utah.edu wrote: Ok, I see. I'll revise my comment to this would be better done with a more general form of type inference, leaving out the claim of where that inference should live. I don't currently know how to do it other than building inference into the complier. Matthias's plug-in rules sounds like a point that we hope to eventually reach through macros as a compiler API. On Sam's general question, I agree that there's no simple answer. Some languages/libraries will provide particular optimizations that are made possible by syntactic constraints. A type system is a particularly fancy syntactic constraint, and it can offer particularly fancy optimizations (such as splitting complex numbers). Syntactic constraints are the reason to have multiple languages and a choice, instead of just one language and compiler. I suppose a single compiler could try several languages and find the one that a program matches syntactically, but often the constraints are complex enough that programs won't fit without careful attention. In that case, a programmer knows (and can declare, and would really prefer to declare and get feedback on) the restricted form that they intend to use for a program. Meanwhile, we have a lot of code in plain Racket. Optimizing by hand is so painful that even writing more C code (for the current optimizer) seems like a better trade-off than hand-optimization. I imagine that the PR was provoked by actual code somewhere. When the compiler is finally itself implemented in Racket, the balance should shift even further toward optimizations for plain Racket, whether or not we find better a macro API for optimizations. At Wed, 28 May 2014 19:50:50 -0700, Eric Dobson wrote: I don't think that TR should provide the majority of the optimizations in its current form because it has to run before inlining, and this limits what it can do. Here is an example program: #lang typed/racket (: my-sequence-map (All (A B) (case- ((A - B) (Vectorof A) - (Vectorof B)) ((A - B) (Listof A) - (Listof B) (define (my-sequence-map f s) (if (vector? s) (vector-map f s) (map f s))) (my-sequence-map add1 (vector 1 2 3)) (my-sequence-map add1 (list 1 2 3)) I would like this to be optimized to: (vector-map add1 (vector 1 2 3)) (map add1 (list 1 2 3)) I think this case of code will be very common if we move to a world where we work over generic sequences/datastructures, and specializing the call sites will be a big win. TR cannot do this optimization
Re: [racket-dev] [plt] Push #28817: master branch updated
I think that there was a miscomunication over the word context and other than that we are in agreement. The context in context-free has not the same as the logical context, and the context free rewrite rules you are proposing have the logical context as part of them. My claim was that without the logical context (just over the ast/bytecode) we would be very limited, and that we absolutely need it. On Thu, May 29, 2014 at 7:40 AM, Matthias Felleisen matth...@ccs.neu.edu wrote: Let me spell out my cryptic comment. 1. I said that a bunch of optimizations are simple context-free rewrite rules. 2. I also said that what we really need to keep track of contexts. If you think of Γ ⊢ e ~ e' if Γ ⊨ e ~ e' as the general form of optimizing rewrites, then the key generalization over 2 is the context Γ. 3. Matthew calls this 'type inference' because that's where Γs like the above are most common. But Γ could also contain statements such as 'f = \x.e, f \not∈ AV(P)' which then gives rise to inlining. [Optimizations really are about the logic of the program, if you want sound ones.] 4. In general optimizers gather a lot of knowledge about contexts that they exploit, and front-ends do so mostly for type checking reasons. That's why the two are often conflated. But you really do want more than type info in the context. 5. Our current major problem is that the type checker does not communicate the type checking information from the front end to the optimizer. The general formulation is that #lang-languages have only a few hooks to tell the compiler what they figured out. 6. Now in this context, my Perhaps remark means two distinct things: -- it would be wonderful if we could centralize rewriting rules in one place through one mechanism, and syntax-* looks promising That does not mean that these things are part of the program. I could see using some syntax-* used to generate code for the current optimizer. [I know that this is a stretch.] -- it would be even wonderfuller if (a) this centralized mechanism came with a mechanism for collecting context information and (b) if #lang languages had a mechanism to communicate the contextual information they have gathered to this central rewriter. This would avoid leakage [citation to Julia omitted] Does this make sense? Okay I understand that I am laying out a research agenda to improve our infrastructure. Don't bother to tell me, I know. It's my job. Now I have to look for someone who wishes to write this very real dissertation. -- Matthias On May 28, 2014, at 10:50 PM, Eric Dobson eric.n.dob...@gmail.com wrote: Cases like this make me think that we need something stronger than context free rewrite rules over the ast/bytecode. On May 29, 2014, at 1:19 AM, Matthew Flatt mfl...@cs.utah.edu wrote: Ok, I see. I'll revise my comment to this would be better done with a more general form of type inference, leaving out the claim of where that inference should live. I don't currently know how to do it other than building inference into the complier. Matthias's plug-in rules sounds like a point that we hope to eventually reach through macros as a compiler API. On Sam's general question, I agree that there's no simple answer. Some languages/libraries will provide particular optimizations that are made possible by syntactic constraints. A type system is a particularly fancy syntactic constraint, and it can offer particularly fancy optimizations (such as splitting complex numbers). Syntactic constraints are the reason to have multiple languages and a choice, instead of just one language and compiler. I suppose a single compiler could try several languages and find the one that a program matches syntactically, but often the constraints are complex enough that programs won't fit without careful attention. In that case, a programmer knows (and can declare, and would really prefer to declare and get feedback on) the restricted form that they intend to use for a program. Meanwhile, we have a lot of code in plain Racket. Optimizing by hand is so painful that even writing more C code (for the current optimizer) seems like a better trade-off than hand-optimization. I imagine that the PR was provoked by actual code somewhere. When the compiler is finally itself implemented in Racket, the balance should shift even further toward optimizations for plain Racket, whether or not we find better a macro API for optimizations. At Wed, 28 May 2014 19:50:50 -0700, Eric Dobson wrote: I don't think that TR should provide the majority of the optimizations in its current form because it has to run before inlining, and this limits what it can do. Here is an example program: #lang typed/racket (: my-sequence-map (All (A B) (case- ((A - B) (Vectorof A) - (Vectorof B)) ((A - B) (Listof A) -
