34 ms·

Morte: an intermediate language for super-optimizing functional programs

79 points by mercurial 12y ago

mercurial 12y 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 12y ago
  Morte means "death" in Latin and also in my native language (Portuguese).
  - glibgil 12y 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.
    - mercurial 12y ago
      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.
      - Gabriel439 12y ago
        I agree. Planescape: Torment was the best RPG ever. I still get chills thinking about it.
    - JadeNB 12y ago
      > 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 http://www.etymonline.com/index.php?term=mortgage.
  - ionforce 12y ago
    De onde você é? Português ou brasileiro? Estuda latim? Where are you from? Are you Portuguese or Brazilian? Did you study Latin?
rrradical 12y ago
I love the work this guy does. He consistently and often develops really interesting Haskell libraries. Does anyone know his background?
- deleted 12y ago
  [deleted]
- Gabriel439 12y 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 12y ago
    What sort of work are you doing at Twitter? Does Twitter use Haskell?
    - Gabriel439 12y ago
      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.
      - tel 12y ago
JadeNB 12y 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.
- silentvoice 12y 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 http://en.wikipedia.org/wiki/Calculus_of_constructions (What morte is based on) and http://en.wikipedia.org/wiki/Normalization_property_(abstract_rewriting)#Typed_lambda_calculus http://en.wikipedia.org/wiki/Normalization_property_(abstrac... answers the point on Turing completeness.
  - JadeNB 12y 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 http://lambda-the-ultimate.org/node/4290), but Ross Angle points out at http://lambda-the-ultimate.org/node/5045#comment-82340 http://lambda-the-ultimate.org/node/5045#comment-82340 that that's only when they are mixed, which is apparently not the case here.
    - silentvoice 12y ago
      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.
gamegoblin 12y 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.
- JadeNB 12y ago
  You can do this, at the cost of some heavy lifting to express it: http://www.haskell.org/haskellwiki/Type_arithmetic 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-expressions-not-evaluated-at-compile-time-in-haskell http://stackoverflow.com/questions/19259114/why-are-constant....
- chongli 12y 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.
- deleted 12y ago
  [deleted]

79 points by mercurial 12y 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 12y ago
Morte means "death" in Latin and also in my native language (Portuguese).
- glibgil 12y 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.
  - mercurial 12y ago
    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.
    - Gabriel439 12y ago
      I agree. Planescape: Torment was the best RPG ever. I still get chills thinking about it.
  - JadeNB 12y ago
    > 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 http://www.etymonline.com/index.php?term=mortgage.
- ionforce 12y ago
  De onde você é? Português ou brasileiro? Estuda latim? Where are you from? Are you Portuguese or Brazilian? Did you study Latin?

rrradical 12y ago

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

deleted 12y ago
[deleted]
Gabriel439 12y 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 12y ago
  What sort of work are you doing at Twitter? Does Twitter use Haskell?
  - Gabriel439 12y ago
    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.
    - tel 12y ago

JadeNB 12y 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.

silentvoice 12y 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 http://en.wikipedia.org/wiki/Calculus_of_constructions (What morte is based on) and http://en.wikipedia.org/wiki/Normalization_property_(abstract_rewriting)#Typed_lambda_calculus http://en.wikipedia.org/wiki/Normalization_property_(abstrac... answers the point on Turing completeness.
- JadeNB 12y 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 http://lambda-the-ultimate.org/node/4290), but Ross Angle points out at http://lambda-the-ultimate.org/node/5045#comment-82340 http://lambda-the-ultimate.org/node/5045#comment-82340 that that's only when they are mixed, which is apparently not the case here.
  - silentvoice 12y ago
    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.

gamegoblin 12y 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.

JadeNB 12y ago
You can do this, at the cost of some heavy lifting to express it: http://www.haskell.org/haskellwiki/Type_arithmetic 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-expressions-not-evaluated-at-compile-time-in-haskell http://stackoverflow.com/questions/19259114/why-are-constant....
chongli 12y 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.
deleted 12y ago
[deleted]