Hacker News Reader

Comment by dustingetz | Hacker News Reader

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-lang...

https://en.wikipedia.org/wiki/Superoptimization

View on HN

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.

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.

Morte isn't Turing complete.

Morte by itself also doesn't support arithmetics.

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.

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

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.

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

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

Reply on news.ycombinator.com