Morte: an intermediate language for super-optimizing functional programs(haskellforall.com)
haskellforall.com
Morte: an intermediate language for super-optimizing functional programs
http://www.haskellforall.com/2014/09/morte-intermediate-language-for-super.html
4 comments
I love the work this guy does. He consistently and often develops really interesting Haskell libraries. Does anyone know his background?
I was a PhD student in biochemistry, but most of my PhD work was structural bioinformatics because I worked in a protein design research lab. Working on my PhD project is how I got exposed to (and addicted to) Haskell and programming in general, so I decided to change career paths to software engineering so I could feed my programming habit and now I work at Twitter.
Wow, interesting journey.
Anyway, I'm a fan. I'm working on a game engine now with an eye toward it being usable with mvc.
Keep making neat things!
Anyway, I'm a fan. I'm working on a game engine now with an eye toward it being usable with mvc.
Keep making neat things!
What sort of work are you doing at Twitter? Does Twitter use Haskell?
I work on an internal analytics framework at Twitter.
Twitter doesn't use Haskell. The most Haskell I've done there is to write an internal tool in Haskell (A shell-based interface to HDFS). Everybody here knows that it's my mission to introduce Haskell more at Twitter and I have two long plays to do so (Morte is part of one of them).
You would think that it would be easier to introduce Haskell at a Scala-based company because of the strong similarities between the functional half of Scala and Haskell, but it's actually quite the opposite: the marginal benefit of switching to Haskell is smaller so it's harder to make the case to adopt Haskell. This is why you see Haskell take hold more easily in companies programming primarily in languages far-removed from Haskell (like PHP or Python) because then the marginal benefit of switching is much higher.
Twitter doesn't use Haskell. The most Haskell I've done there is to write an internal tool in Haskell (A shell-based interface to HDFS). Everybody here knows that it's my mission to introduce Haskell more at Twitter and I have two long plays to do so (Morte is part of one of them).
You would think that it would be easier to introduce Haskell at a Scala-based company because of the strong similarities between the functional half of Scala and Haskell, but it's actually quite the opposite: the marginal benefit of switching to Haskell is smaller so it's harder to make the case to adopt Haskell. This is why you see Haskell take hold more easily in companies programming primarily in languages far-removed from Haskell (like PHP or Python) because then the marginal benefit of switching is much higher.
[deleted]
I'm confused by this. It seems to be promising a normal form for all expressions in a Turing-complete language—but that's equivalent to guaranteeing termination, isn't it? Moreover, it promises to produce equal results for equivalent programs, which would allow a solution of the halting problem, wouldn't it?
I suspect that I've got some bad conceptual misunderstanding here; but, on the other hand, I also have a hard time believing that, if beta- and eta-reduction alone were sufficient to express such powerful optimisations, it would have taken this long to discover that.
I suspect that I've got some bad conceptual misunderstanding here; but, on the other hand, I also have a hard time believing that, if beta- and eta-reduction alone were sufficient to express such powerful optimisations, it would have taken this long to discover that.
Did the author claim Morte was Turing-complete? I don't think I saw that claim, but I'm a newcomer to all this computer science theory stuff. I think these Wikipedia links answer your question:
http://en.wikipedia.org/wiki/Calculus_of_constructions (What morte is based on)
and
http://en.wikipedia.org/wiki/Normalization_property_(abstrac...
answers the point on Turing completeness.
http://en.wikipedia.org/wiki/Calculus_of_constructions (What morte is based on)
and
http://en.wikipedia.org/wiki/Normalization_property_(abstrac...
answers the point on Turing completeness.
I had assumed that it must be Turing complete because otherwise its utility as an intermediate language seems dramatically reduced (despite its power, no one is compiling to Coq!); but, now that you point it out, I agree that there is no such claim. I originally thought that general recursion followed from folds and unfolds (http://lambda-the-ultimate.org/node/4290), but Ross Angle points out at http://lambda-the-ultimate.org/node/5045#comment-82340 that that's only when they are mixed, which is apparently not the case here.
I don't know how useful it will be in the end. The idea of targeting a powerful (proper) subset of turing completeness to produce fast executables makes a lot of sense to me, and furthermore for reasons that you have already brought up this is the only way it is possible if we truly desire a mechanized solution to this problem.
My concern on the practicality point is that the superoptimizer here really isn't "superoptimizing" so much as super-simplifying. There's a reason modern compilers don't aggressively inline every single function called if they have access to the source code, and for the same reasons they don't aggressively unroll every loop they come across if the loop bounds are known compile time.The tradeoffs of such optimizations are very complicated and hard to reason about because processors are very complicated and hard to reason about.
My concern on the practicality point is that the superoptimizer here really isn't "superoptimizing" so much as super-simplifying. There's a reason modern compilers don't aggressively inline every single function called if they have access to the source code, and for the same reasons they don't aggressively unroll every loop they come across if the loop bounds are known compile time.The tradeoffs of such optimizations are very complicated and hard to reason about because processors are very complicated and hard to reason about.
In a reddit discussion, the author indicates that, indeed, it is explicitly not Turing complete: http://www.reddit.com/r/haskell/comments/2g6wsx/haskell_for_....
I don't think this will allow solving the halting problem, its been mathematically proved to be impossible to solve [1].
Nothing prevents a turing complete program from entering an infinite loop. A GUI program for example is terminated only when the user decides to, which is impossible to predict.
1. http://en.wikipedia.org/wiki/Rice%27s_theorem
Nothing prevents a turing complete program from entering an infinite loop. A GUI program for example is terminated only when the user decides to, which is impossible to predict.
1. http://en.wikipedia.org/wiki/Rice%27s_theorem
> I don't think this will allow solving the halting problem, its been mathematically proved to be impossible to solve [1].
Yes, this is my point: the proposed super-optimiser would, it seems to me, en passant be solving the halting problem, which means that it can't actually exist (or, at least, can't actually satisfy the stated guarantee).
> Nothing prevents a turing complete program from entering an infinite loop. A GUI program for example is terminated only when the user decides to, which is impossible to predict.
On the level of the lambda-calculus, this is reflected in the corresponding term's having no normal form, in which case the algorithm described (which relies on reducing everything to a normal form) cannot do anything with it.
Yes, this is my point: the proposed super-optimiser would, it seems to me, en passant be solving the halting problem, which means that it can't actually exist (or, at least, can't actually satisfy the stated guarantee).
> Nothing prevents a turing complete program from entering an infinite loop. A GUI program for example is terminated only when the user decides to, which is impossible to predict.
On the level of the lambda-calculus, this is reflected in the corresponding term's having no normal form, in which case the algorithm described (which relies on reducing everything to a normal form) cannot do anything with it.
The halting problem forbids the existence of oracles which can decide with certainty in some finite time that an arbitrary program will halt. Loosen any of these qualifiers and the problem is not necessarily undecidable. Loosening the "arbitrary program" restriction, the problem of analyzing the termination of a subset of programs which doesn't encode looping or recursion constructs ( i.e. simply typed lambda calculus ) is trivially decidable. A totality checker like in Agda can decide whether some programs halt given a set of restrictions on the program.
>Moreover, it promises to produce equal results for equivalent programs, which would allow a solution of the halting problem, wouldn't it?
I believe this is the case. So the article's promise (as I read it) can not hold true in the general case.
On a similar note, just write a program that runs the collatz conjecture and prints the result and a program that prints 1. Run them through Morte. If they compile to the same code, then boom, you've solved the Collatz conjecture :)
I believe this is the case. So the article's promise (as I read it) can not hold true in the general case.
On a similar note, just write a program that runs the collatz conjecture and prints the result and a program that prints 1. Run them through Morte. If they compile to the same code, then boom, you've solved the Collatz conjecture :)
You can't encode the Collatz Conjecture (in that way) in Morte. It would require an infinite amount of computation and infinite loops have been disallowed. You would have to get a little bit more creative with the dependently typed parts of CIC and then finding a program which matches the needed type is as of today an unsolved task.
Equivalent in the sense he's talking about means "I can take any declaration a = b and replace a with b in the scope of that definition". This is substantially weaker than "if the two programs produce the same output", which would obviously violate Rice's Theorem.
Simple—it's not Turing complete. The whole premise is to eliminate recursive structure. Replacing them are measured folds and unfolds of data and codata respectively. These allow you to get as close to infinity as needed on both sides without going over (for some moderate syntactic and semantic penalties).
Within a language like the Calculus of Coinductive Constructions like Morte appears to implement it's not such a strange idea to have normalization.
So, no infinite loops means no Halting Problem means no completeness.
The upside is a larger set of easy-to-perform optimizations, much greater mathematical elegance. The downside is that you cannot directly write an interpreter for a complete language. Though you could write one which halts every N steps and requires user input to continue. In practice, that isn't the worst idea for a repl anyway.
Within a language like the Calculus of Coinductive Constructions like Morte appears to implement it's not such a strange idea to have normalization.
So, no infinite loops means no Halting Problem means no completeness.
The upside is a larger set of easy-to-perform optimizations, much greater mathematical elegance. The downside is that you cannot directly write an interpreter for a complete language. Though you could write one which halts every N steps and requires user input to continue. In practice, that isn't the worst idea for a repl anyway.
How will be Morte used to do "real work"? Would it always have to be called from a larger language that can do effectful things like IO?
I have no idea what Gabriel is intending here; I'm just talking from general knowledge about consistent languages like the CIC.
There are a number of general examples, though.
1. You can leave termination guarantees in foreign code up to the programmer using an "unsafe" marker.
2. You can model effects using a monad
3. You can model the whole program as codata which is "driven" by the runtime
4. You can write a compiler of an embedded language in CIC and execute complete programs in, say, C
There are a number of general examples, though.
1. You can leave termination guarantees in foreign code up to the programmer using an "unsafe" marker.
2. You can model effects using a monad
3. You can model the whole program as codata which is "driven" by the runtime
4. You can write a compiler of an embedded language in CIC and execute complete programs in, say, C
I have always wondered why I couldn't do something in Haskell like:
But there are some instances where, for code readability, I'd want to say "f 123" rather than whatever "f" evaluates to at 123, since "f 123" shows where the value comes from, but at compile time I'd like that to be optimized out.
{#- COMPILECOMPUTE #-}
factorial 0 = 1
factorial n = n * factorial (n - 1)
But there are some instances where, for code readability, I'd want to say "f 123" rather than whatever "f" evaluates to at 123, since "f 123" shows where the value comes from, but at compile time I'd like that to be optimized out.
You can do this, at the cost of some heavy lifting to express it: http://www.haskell.org/haskellwiki/Type_arithmetic.
P.S. This type of inlining was also discussed at http://stackoverflow.com/questions/19259114/why-are-constant....
P.S. This type of inlining was also discussed at http://stackoverflow.com/questions/19259114/why-are-constant....
Haskell already does something almost like this. Expressions such as "factorial 5" may be lifted to the top level as a Constant Applicative Form (CAF). This allows the result to be computed once the first time they are needed and then subsequently shared, even across function invocations.
The advantage of this approach over doing it at compile time is that you don't risk blowing up your compilation time.
The advantage of this approach over doing it at compile time is that you don't risk blowing up your compilation time.
[deleted]
> Also, if you're wondering, the name Morte is a tribute to a talking skull from the game Planescape: Torment, since the Morte library is a "bare-bones" calculus of constructions.
Clearly a mark of good taste.
Clearly a mark of good taste.
Morte means "death" in Latin and also in my native language (Portuguese).
Almost every native English speaker knows the meaning of morte. We have a words like mortician which is a person who cares for the dead, mortgage which is a plan to kill you debt, rigor mortis which is the stiffness of death and mortal which means subject to death. Yes, we almost all know what morte means. That is why it was the name given to a talking skull in a game. Just like love and hate, however, we often use native words in English for our most basic concepts. Death is one of those.
> mortgage which is a plan to kill you debt
I thought that this must be a joke, but it looks like it's not far off: http://www.etymonline.com/index.php?term=mortgage.
I thought that this must be a joke, but it looks like it's not far off: http://www.etymonline.com/index.php?term=mortgage.
You also have Mallory's "Le Morte d'Arthur" (no talking skull involved in this one). That said, it was just a small nod to Gabriel's appreciation of the game, which after so many years I still consider the best RPG ever made.
I agree. Planescape: Torment was the best RPG ever. I still get chills thinking about it.
De onde você é? Português ou brasileiro? Estuda latim?
Where are you from? Are you Portuguese or Brazilian? Did you study Latin?
Where are you from? Are you Portuguese or Brazilian? Did you study Latin?