Morte: an intermediate language for super-optimizing functional programs

http://www.haskellforall.com/2014/09/morte-intermediate-language-for-super.html

by mercurial • 12 years ago

79 31 12 years ago

mercurial2• 12 years ago

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.

TelmoMenezes• 12 years ago

Morte means "death" in Latin and also in my native language (Portuguese).

glibgil• 12 years ago

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.

ionforce• 12 years ago

De onde você é? Português ou brasileiro? Estuda latim?

Where are you from? Are you Portuguese or Brazilian? Did you study Latin?

rrradical2• 12 years ago

I love the work this guy does. He consistently and often develops really interesting Haskell libraries. Does anyone know his background?

Gabriel4393• 12 years ago

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.

cstrahan• 12 years ago

What sort of work are you doing at Twitter? Does Twitter use Haskell?

rrradical2• 12 years ago

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!

JadeNB6• 12 years ago

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.

jeremiep• 12 years ago

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

JadeNB6• 12 years ago

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.

freyrs3• 12 years ago

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.

wyager• 12 years ago

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 :)

tel4• 12 years ago

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.

hawkice• 12 years ago

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.

silentvoice2• 12 years ago

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.

JadeNB6• 12 years ago

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.

JadeNB6• 12 years ago

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

tel4• 12 years ago

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.

bigcojosh• 12 years ago

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?

gamegoblin• 12 years ago

I have always wondered why I couldn't do something in Haskell like:

    {#- COMPILECOMPUTE #-}
    factorial 0 = 1
    factorial n = n * factorial (n - 1)

And have the compiler transform something like "factorial 5" into "120" at compile time, since factorial is a pure function, it seems like that would be doable? Of course you'd have to use your pragmas very judiciously to avoid crazy compile times.

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.

JadeNB6• 12 years ago

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

chongli• 12 years ago

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.

Morte: an intermediate language for super-optimizing functional programs

Related Stories