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.
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.
That reminds me of Joe Armstrong's talk—the best place to introduce new technology is in a company which is already experiencing technology failure. At that point, the pain is clear and options to resolve it command power and premium.
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.
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.
>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 :)
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.
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:
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.
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.
> 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.
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.
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.
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.
> 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.
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.
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.
