3 ms·

Your description of the assistant reminds me of a Clojure talk I watched recently[1] where the speaker outlines how a central pool of knowledge about invariant

• chriswarbo 10y ago
  Not watched the talk yet, but sounds very similar to my own thinking. For example, I think the "pipeline" approach of compilation (preprocess -> lex -> parse -> desugar -> inference -> check -> optimise -> code generation) is very restrictive, as it precludes many other activities (e.g. static analysis), forcing custom lexers, parsers, etc. to be created in parallel, which may-or-may-not work with existing code, etc. I think a more data-based approach would be preferable, for example we might think of "source text", "preprocessed", "lexed", etc. as being tables in a relational database, and the phases of the pipeline as views/projections which populate one table from another. Optimisation would just be a one:many relation, with a single source text corresponding to multiple possible expressions. This data could be stored, collated, mined, augmented, etc. by various other processes, which allows more approaches to be taken than just compiling. Of course, this is just one idea; and the relational part would only need to be an interface to the data, it could be computed lazily, and wouldn't necessarily be implemented with an actual RDBMS storing all of the intermediate bits.
• chriswarbo 10y ago
  Just watched the talk. The technique the author's discovered is called "supercompilation" (note: this is distinct from "superoptimisation", mentioned in sibling comments). The idea is to use an evaluation strategy which works at compile time, reducing statically-known expressions whilst shuffling around unknown values symbolically to preserve the semantics. The result ends up folding constants, inlining, unrolling, etc. automatically, just like the examples in the talk. Whilst supercompilation can be slow, the main criticism is that resulting code is quite large, due to the amount of inlining. The main difference between supercompilers and the technique discussed in the talk is that supercompilation is provably correct: it doesn't rely on testing or placing exhaustiveness requirements on the user. I don't think it's necessary to sacrifice correctness; the speaker mentioned the use of guards in JITs, and how he avoids them for speed, but I think that since we're performing such extensive rewriting of the code anyway, many redundant guards can be supercompiled-away, and those remaining can be shunted to the start of the program, so that no branches appear in the hot path. The allusions to the scientific method seem to be about properties/invariants, and potential counterexamples to them. I'm all for finding and sharing properties of programs, both conjectured and proven, although I don't like the idea of assuming the conjectures are true. I've looked into this in Haskell, and found some great work, including: - QuickSpec (v1 https://hackage.haskell.org/package/quickspec https://hackage.haskell.org/package/quickspec and v2 https://github.com/nick8325/quickspec https://github.com/nick8325/quickspec ) which conjectures equations about functions by testing them on random inputs. - HipSpec ( https://github.com/danr/hipspec https://github.com/danr/hipspec ) which does the same as QuickSpec, but automatically proves the equations so they're guaranteed to hold. - The GHC compiler's rewrite rule system ( https://wiki.haskell.org/GHC/Using_rules https://wiki.haskell.org/GHC/Using_rules ) which allows programs to be optimised by replacing regular definitions with optimised versions in particular cases. This is how "fusion" and "deforestation" optimisations are implemented, e.g. https://donsbot.wordpress.com/2010/02/26/fusion-makes-functional-programming-fun https://donsbot.wordpress.com/2010/02/26/fusion-makes-functi... I think there's definitely some low-hanging fruit there, for finding equivalent expressions, comparing their performance, and generating a list of rewrite rules which the programmer may want to consider adding to their code. A slightly more ambitious project would use equations/properties about the program to generate a specialised supercompiler (maybe using something like a variant of knuth-bendix completion, ordered such that the normal forms are the higher-performing variants).