tag:blogger.com,1999:blog-1777990983847811806.post1179905794869657936..comments2021-09-16T21:12:15.659-07:00Comments on Haskell for all: Morte: an intermediate language for super-optimizing functional programsGabriella Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-1777990983847811806.post-87653540163969947412017-02-26T20:22:21.555-08:002017-02-26T20:22:21.555-08:00Yeah, super-compiler is probably the more correct ...Yeah, super-compiler is probably the more correct word for thisGabriella Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-65448300149646560942017-02-24T09:31:24.840-08:002017-02-24T09:31:24.840-08:00I really like the ideas you're following with ...I really like the ideas you're following with Morte, Annah, Dhall, etc. but stumbling on this post I'm wondering if "super-optimize" is the right phrase to use, and whether "super-compile" would be more accurate.<br /><br />As far as I'm aware, super-optimisation involves brute-force search for a program which is provably equivalent to the input, starting with small, fast programs and gradually trying longer, slower programs until a provably-equivalent one can be found. Crucially, we don't generate code by modifying the given program into some other form; instead, it's only used as a *specification* against which we check our generated code. It seems like state of the art superoptimisers can handle programs containing around 10 machine code instructions, without branches.<br /><br />On the other hand, super-compilation involves modifying the given code as much as possible, acting like constant-folding on steroids. Rather than special-case optimisations like constant folding, function inlining, loop unrolling, etc. a supercompiler will try to evaluate as many terms of the program as possible at compile time. Known functions applied to known arguments will be run to completion, abstractions will be collapsed and any remaining computation will be specialised to perform only those steps which couldn't be reduced without knowing the input (e.g. a pattern-match). That seems to be what Morte does; relying on CoC being total to ensure that performing such calls will terminate.<br /><br />Some super-compilers also extend the reduction rules of the language, to try and reduce redundancy between branches. For example, during supercompilation our code may end up containing something like 'if (x > 3) then (if (x > 0) then "hello" else "goodbye") else "world"' which we can't beta-reduce without knowing "x"; however, we can still propagate the "positive" information that "x > 3" into the "then" branch, which tells us enough about "x" that we can evaluate the inner "if" to get 'if (x > 3) then "hello" else "world"'. We can also propagate the "negative" information (in this case "not (x > 3)") into "else" branches.Warbohttps://www.blogger.com/profile/11167936627543971536noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-77127744345097009152015-05-23T23:16:39.078-07:002015-05-23T23:16:39.078-07:00There are examples of the list operations on folds...There are examples of the list operations on folds on Oleg's site.Dobeshttps://www.blogger.com/profile/09392777569321223496noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-21688510864185170722015-05-23T23:16:28.331-07:002015-05-23T23:16:28.331-07:00There are examples of the list operations on folds...There are examples of the list operations on folds on Oleg's site.Dobeshttps://www.blogger.com/profile/09392777569321223496noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-66711565582750730402015-05-19T07:06:41.836-07:002015-05-19T07:06:41.836-07:00Thanks! I fixed it.Thanks! I fixed it.Gabriella Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-2833491693345996162015-05-18T23:15:02.446-07:002015-05-18T23:15:02.446-07:00In the Haskell version of the IO example, the defi...In the Haskell version of the IO example, the definition of `main = replicateM_ ninetynine main_` is missing.Anonymoushttps://www.blogger.com/profile/11260067622636055037noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-92223856640545910072014-09-14T16:10:24.285-07:002014-09-14T16:10:24.285-07:00Yeah, in this case I mean alpha-beta-eta-equivalen...Yeah, in this case I mean alpha-beta-eta-equivalence. I think the right concept is also free theorem equivalence, but that's harder to implement, and I'm trying to see if there is an easy subset of theorems that can be implemented that is reasonably complete.<br /><br />I think if you also have free theorems you can implement the kind of equivalence you just described, but that is still a very big "if".Gabriella Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-54889586826210158882014-09-14T10:14:10.653-07:002014-09-14T10:14:10.653-07:00Very interesting post! (You had won me over by the...Very interesting post! (You had won me over by the time you said "Morte" :)<br /><br />I have a question regarding your statement that if two programs are “equal” they produce the same executable. What do you mean by equal in this context? alpha-beta-eta-equivalence? And if so, do you think that is the right concept here?<br /><br />The reason why I am asking here is the following. In classical treatments of lambda calculus, programs are just single lamba terms. There, we know that simply typed lambda calculus is strongly normalizing, and therefore (alpha)-beta-eta-equivalence is decidable by computing the normal form. However, what we are interested here is the question whether the two *programs* are the same, i.e., compute the same output on all inputs. More precisely, the question would be, given lambda terms A and B decide whether (A X) beta-eta-= (B X) for all correctly typed X. Even though simply typed lambda calculus is not Turing complete, I still cannot imagine that this problem is decidable for all A and B. <br /><br />What I am getting at is this: We have two notions of equality. i) ordinary beta-eta-equivalence and ii) beta-eta-equivalence over all X in the above sense. ii) seems to be too strong a notion of equality to be tackled with the approach you outline. On the other, hand i) seems too weak to be interesting for programs that act on many different inputs. So, is there a notion of equality that lies between i) and ii) that you are shooting for here?Felix Breuerhttps://www.blogger.com/profile/07562782118792528889noreply@blogger.com