4 ms·

See also Morte: an intermediate language for super-optimizing functional programs "Now suppose there were a hypothetical language with a stronger guarantee: if

See also Morte: an intermediate language for super-optimizing functional programs "Now suppose there were a hypothetical language with a stronger guarantee: if two programs are equal then they generate identical executables. Such a language would be immune to abstraction: no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected. Here I will introduce such an intermediate language named Morte that obeys this stronger guarantee." http://www.haskellforall.com/2014/09/morte-intermediate-language-for-super.html http://www.haskellforall.com/2014/09/morte-intermediate-lang... https://en.wikipedia.org/wiki/Superoptimization https://en.wikipedia.org/wiki/Superoptimization

amelius 9y ago
So then the task is to transpile the source functions into Morte, compile them, and see if the executables are equal; and somehow we have solved an undecidable problem (?) There must be a catch somewhere.
- cousin_it 9y ago
  Morte isn't Turing complete.
- kccqzy 9y ago
  Morte by itself also doesn't support arithmetics.
  - jerf 9y ago
    I am reliably informed by many Internet commenters... and can there be any higher authority than that?... that programming doesn't actually involve "math" very often at all, so I'm sure languages that don't support that ivory tower "arithmetic" stuff will be suitable for a wide variety of useful every day tasks, such as scraping web APIs and re-implementing Reddit in a weekend.
  - dustingetz 9y ago
    Urbit does this cool trick where you use pure lambda calculus arithmetic (church encoding), use this theoretically correct impl as a basis of your proofs and reasoning, and then at runtime provide a polyfill that uses hardware arithmetic operators. The runtime impl is thus not equal since it can for example overflow, but in practice that doesn't inhibit our ability to make useful programs. https://en.wikipedia.org/wiki/Church_encoding https://en.wikipedia.org/wiki/Church_encoding Facebook does this also with GraphQL - GraphQL queries are theoretically dynamic and defined by the client, but you can bake them when you ship, and then provide optimized implementations of the query that also have knowledge of the UI and database that they aren't supposed to otherwise have.
chriswarbo 9y ago
Morte isn't actually a superoptimiser, it's a supercompiler. A supercompiler performs as much evaluation as it can at compile-time; it can be thought of as inlining every function call, and constant folding every literal. A superoptimiser is a search procedure which generates programs, e.g. starting with individual machine instructions, then pairs of machine instructions, and so on, and checks whether any of them behave the same as the given program; if so, they're used as the output. Supercompilation is 'top down': we refine the given program again and again until there's nothing more to do. Superoptimisation is 'bottom up': we build up from nothing until we have a binary which implements the given program.
Kutta 9y ago
Unfortunately, beta-eta reduction on Church-coded terms (as in Morte) is much weaker than what is commonly understood as supercompilation, and it is false that "no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected". This kind of statement can only theoretically hold for something like simple type theory with strong finite products and coproducts, for which (quasi) normalization has been recently shown in https://arxiv.org/abs/1610.01213 https://arxiv.org/abs/1610.01213
- dustingetz 9y ago
  It was my understanding that you just had to provide a safe language without infinite loops (so no ⊥) - is this not true? https://en.wikipedia.org/wiki/Bottom_type https://en.wikipedia.org/wiki/Bottom_type

amelius 9y ago

So then the task is to transpile the source functions into Morte, compile them, and see if the executables are equal; and somehow we have solved an undecidable problem (?) There must be a catch somewhere.

cousin_it 9y ago
Morte isn't Turing complete.
kccqzy 9y ago
Morte by itself also doesn't support arithmetics.
- jerf 9y ago
  I am reliably informed by many Internet commenters... and can there be any higher authority than that?... that programming doesn't actually involve "math" very often at all, so I'm sure languages that don't support that ivory tower "arithmetic" stuff will be suitable for a wide variety of useful every day tasks, such as scraping web APIs and re-implementing Reddit in a weekend.
- dustingetz 9y ago
  Urbit does this cool trick where you use pure lambda calculus arithmetic (church encoding), use this theoretically correct impl as a basis of your proofs and reasoning, and then at runtime provide a polyfill that uses hardware arithmetic operators. The runtime impl is thus not equal since it can for example overflow, but in practice that doesn't inhibit our ability to make useful programs. https://en.wikipedia.org/wiki/Church_encoding https://en.wikipedia.org/wiki/Church_encoding Facebook does this also with GraphQL - GraphQL queries are theoretically dynamic and defined by the client, but you can bake them when you ship, and then provide optimized implementations of the query that also have knowledge of the UI and database that they aren't supposed to otherwise have.

chriswarbo 9y ago

Morte isn't actually a superoptimiser, it's a supercompiler. A supercompiler performs as much evaluation as it can at compile-time; it can be thought of as inlining every function call, and constant folding every literal. A superoptimiser is a search procedure which generates programs, e.g. starting with individual machine instructions, then pairs of machine instructions, and so on, and checks whether any of them behave the same as the given program; if so, they're used as the output. Supercompilation is 'top down': we refine the given program again and again until there's nothing more to do. Superoptimisation is 'bottom up': we build up from nothing until we have a binary which implements the given program.

Kutta 9y ago

Unfortunately, beta-eta reduction on Church-coded terms (as in Morte) is much weaker than what is commonly understood as supercompilation, and it is false that "no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected". This kind of statement can only theoretically hold for something like simple type theory with strong finite products and coproducts, for which (quasi) normalization has been recently shown in https://arxiv.org/abs/1610.01213 https://arxiv.org/abs/1610.01213

dustingetz 9y ago
It was my understanding that you just had to provide a safe language without infinite loops (so no ⊥) - is this not true? https://en.wikipedia.org/wiki/Bottom_type https://en.wikipedia.org/wiki/Bottom_type