[HN Gopher] High-order Virtual Machine (HVM): Massively parallel...
___________________________________________________________________
High-order Virtual Machine (HVM): Massively parallel, optimal
functional runtime
Author : Kinrany
Score : 266 points
Date : 2022-02-05 09:33 UTC (13 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| dean177 wrote:
| Readers will find HOW.md interesting too:
| https://github.com/Kindelia/HVM/blob/master/HOW.md
| anentropic wrote:
| Wow, I was looking for an ELI5 and I never expected to find one
| from the author of such a project...
|
| I actually feel like I kind of understand it now - kudos to
| @LightMachine!
| amluto wrote:
| It says:
|
| > Notice also how, in some steps, lambdas were applied to
| arguments that appeared outside of their bodies. This is all
| fine, and, in the end, the result is correct.
|
| But one of the example steps is this transformation:
| dup a b = {x0 x1} dup c d = {y0 y1} (Pair
| lx0(ly0(Pair a c)) lx1(ly1(Pair b d)))
| ------------------------------------------------ Dup-Sup
| dup c d = {y0 y1} (Pair lx0(ly0(Pair x0 c))
| lx1(ly1(Pair x1 d)))
|
| I think I'm missing a subtlety. This step substitutes the a/b
| superposition into the lambdas, but I don't see how it knows
| the the x0 goes into the first lambda and the x1 goes into the
| second one. After all, in HVM bizarro-land, lambda arguments
| have no scope, so the reverse substitution seems equally
| plausible and even syntactically valid: (Pair
| lx0(ly0(Pair x1 c)) lx1(ly1(Pair x0 d)))
|
| This substitution produces two magically entangled lambdas,
| which seems fascinating but not actually correct. How does the
| runtime (and, more generally, the computational system it
| implements) know in which direction to resolve a superposition?
| LightMachine wrote:
| `dup a b = {x0 x1}` will just substitute `a` by `x0` and `b`
| by `x1`, no matter where `a` and `b` are. So, if you apply
| that, verbatin, to: (Pair lx0(ly0(Pair a
| c)) lx1(ly1(Pair b d)))
|
| You get: (Pair lx0(ly0(Pair x0 c))
| lx1(ly1(Pair x1 d)))
|
| Does that make sense?
| cwillu wrote:
| "In other words, think of HVM as Rust, except replacing the
| borrow system by a very cheap .clone() operation that can be
| used and abused with no mercy. This is the secret sauce! Easy,
| right? Well, no. There is still a big problem to be solved: how
| do we incrementally clone a lambda? There is a beautiful answer
| to this problem that made this all possible. Let's get
| technical!"
|
| Every third paragraph feels like the autogenerated flavour text
| gibberish of a kerbal space program mission description.
| LightMachine wrote:
| I know it needs improvements, there is even a disclaimer in
| the top of HOW.md. I'll go over it and improve sentences like
| that in a future.
| throwaway17_17 wrote:
| I don't know that I would go as far as you did, but the
| writing style is a little bit to hyperbolic or maybe just to
| rhetorical/conversational for my tastes.
| mrpf1ster wrote:
| I enjoyed it, you can clearly see the author is excited about
| explaining his work.
| yewenjie wrote:
| So many new programming languages coming up with clever features
| that makes me wish I could mix and match their core features
| while using libraries from more popular languages.
|
| Up and coming Languages I am excited about -
|
| 1. Roc - https://www.youtube.com/watch?v=vzfy4EKwG_Y
|
| 2. Zig - https://ziglang.org/
|
| 3. Scopes - https://sr.ht/~duangle/scopes/
|
| 4. Gleam - https://gleam.run/
|
| 5. Odin - https://github.com/odin-lang/Odin
|
| 6. Koka - https://github.com/koka-lang/koka
|
| 7. Unison - https://github.com/unisonweb/unison
| sixbrx wrote:
| Don't forget Kind (https://github.com/Kindelia/Kind) which is
| mentioned in the "How can I Help?" section as a potential
| language for targeting HVM.
| throwaway17_17 wrote:
| I have seen talks and/or papers on all of these except Scopes
| and Gleam. Out of the list the only one that does not provide
| something I am interested in is Unison. Given that your
| feelings for interesting language features seems to be at least
| marginally close to mine I am going to check out Scopes and
| Gleam just to see what they have that interested you.
|
| Personally, from a conceptual level, I find that Koka and Roc
| provide some of the more interesting developments in PL design.
| For anyone wondering, as to Roc (which I don't think has an
| implementation or even a full description yet) I am
| particularly interested in their concept and implementation of
| the 'platform'/'application' layer idea. As to Koka, the papers
| the team has generated are almost all excellent. The paper
| describing Perseus, the GC/resource tracking system, and the
| compiler implementation review are stunning.
| joaogui1 wrote:
| There is an initial version of Roc, though the repo is
| private and you need to ask Richard Feldman for access
| laerus wrote:
| there is also maybe Dada https://dada-lang.org/welcome.html
| arc776 wrote:
| Nim - https://nim-lang.org/
|
| Lets you mix and match other libraries with their native ABI as
| it compiles to C, C++, ObjC and JS + has excellent FFI.
| afranchuk wrote:
| Really neat. I've been working on a lazy parallel language and so
| I read the "HOW" document closely to see the secret sauce. What's
| exciting to me is that, while I'm not familiar with the academia
| behind their decisions, it seems that I arrived at the same
| result with regard to their lazy clones: I realized early in the
| language that caching the eval results would make things _really_
| fast, and this caching ends up doing exactly what their lazy
| clones achieves!
|
| Of course one place I don't cache is in function application
| because the language is not pure (so we want side effects to
| occur again), but this makes me think it might be really good to
| derive which functions/subexpressions are pure and allow the
| cache to be retained through function calls for those.
|
| I'm gonna keep a close watch on this. I should probably read more
| white papers :)
| LightMachine wrote:
| Thank you!
| [deleted]
| carterschonwald wrote:
| The fellow behind this has been hammering at experiments around
| so called optimal reduction strategies for a while!
|
| As another commenter's remarks imply; some of the so called
| benefits for what are called optimal reduction strategies are
| limited to efficiently manipulating data structures that are
| represented by lambdas. And that's also probably why this is
| Untyped. Makes it easier to embed / support such an encoding
| throwaway17_17 wrote:
| Agreed, but the reference he makes to the symmetric interaction
| calculus blog post seems to at least have basis in sound
| logic/semantic principles. I haven't read the whole post, but I
| am at least willing to give it a chance.
| carterschonwald wrote:
| Linear logic inspired ideas are always great
| LightMachine wrote:
| Author here.
|
| HVM is the ultimate conclusion to years of optimal evaluation
| research. I've been a great enthusiast of optimal runtimes. Until
| now, though, my most efficient implementation had barely passed
| 50 million rewrites per second. It did beat GHC in cases where
| optimality helped, like l-encoded arithmetic, but in more real-
| world scenarios, it was still far behind. Thanks to a recent
| memory layout breakthrough, though, we managed to reach a peak
| performance of _2.5 billion_ rewrites per second, on the same
| machine. That 's a ridiculous 50x improvement.
|
| That is enough for it to enjoy roughly the same performance of
| GHC in normal programs, and even outperform it when automatic
| parallelism kicks in, if that counts! Of course, there are still
| cases where it will perform worse (by 2x at most usually, and
| some weird quadratic cases that should be fixed [see issues]),
| but remember it is a 1-month prototype versus the largest lazy
| functional compiler in the market. I'm confident HVM's current
| design is able to scale and become the fastest functional runtime
| in the world, because I believe the optimal algorithm is
| inherently superior.
|
| I'm looking for partners! Check the notes at the end of the
| repository's README if you want to get involved.
| auggierose wrote:
| JFYI, the "This book" link on
| https://github.com/Kindelia/HVM/blob/master/HOW.md goes to a
| research gate page which has the wrong book for download
| (something about category theory).
|
| So, this dup primitive, is that explained in the book as well,
| or is this a new addition in your implementation?
| LightMachine wrote:
| I fixed the link. This is all part of the system described on
| the book, HVM is merely a very fast practical implementation.
| The additions (thinks like machine integers and constructors)
| don't affect the core.
| pchiusano wrote:
| This is very cool research that I've been loosely following for
| a while but I feel the benchmarks you've presented are very
| misleading. They are comparing parallelized code to sequential
| code and then making a big deal that it's faster. Of course,
| you could also write a parallel Haskell version of the same
| benchmarks in about the same amount of code, and I'd expect
| similar speedups.
|
| Haskell doesn't parallelize every independent expression
| because it's a general purpose language and that's unlikely to
| be the correct choice in all contexts.
|
| I don't have much of an intuition for whether the optimal
| evaluation stuff will be useful in practice for the kinds of
| programs people actually write. Like I get that it helps a lot
| if you're doing multiplication with Church numerals... but can
| you give some more compelling examples?
| LightMachine wrote:
| I didn't want to be misleading, sorry. My reasoning was to
| just benchmark identical programs.
|
| I personally think Haskell's approach to parallelism is
| wrong, though, since it demands in-code annotations to work.
| The problem is that the decision on whether an expression
| should be parallelized doesn't depend on the code itself, but
| on where the expression is used. For example, if `fib(42)` is
| the topmost node of your program's normal form, you always
| want to parallelize its branches (`fib(41)` and `fib(40)`),
| but if it is called in a deeply nested list node, you don't.
| That information isn't available on the code of `fib`, so
| placing "spark" annotations seems conceptually wrong.
|
| HVM parallelizes by distributing to-be-evaluated redexes of
| the normal form among available cores, prioritizing these
| close to root. Here is an animation:
| https://imgur.com/a/8NtnEa3. That always seems like the right
| choice to me. After all, it just returns the same result,
| faster. I could be wrong, though. In which case you think
| parallelism isn't the correct choice? Is it because you don't
| always want to use the entire CPU? Would love to hear your
| reasoning.
|
| > Like I get that it helps a lot if you're doing
| multiplication with Church numerals...
|
| This isn't about multiplication with Church numerals. Don't
| you find it compelling to write binary addition as "increment
| N times" and have it be as efficient as the add-with-carry
| operation? Making mathematically elegant code fast matters,
| and HVM does that. See the overview [0] for instance. Also,
| this allows us to have all the "deforestation" optimizations
| that Haskell applies on List with hardcoded #rewrite pragmas,
| for any user-defined datatype, which is also quite useful.
| There are certainly many uses that I'm not creative enough to
| think of.
|
| [0] https://github.com/Kindelia/HVM/blob/master/HOW.md#bonus-
| abu...
| acchow wrote:
| This work is mindblowing me to me. Also I love the README!
|
| You did mention that you pretty much implement pages 14-39 of
| The Optimal Implementation of Functional Programming Languages.
| Any idea why the authors of the book didn't implement it
| themselves?
|
| Also, what lead you to this recent memory layout breakthrough.
| What was the journey of thinking towards this end?
| conaclos wrote:
| The How page [0] is nicely written! It was a real pleasure to
| read :)
|
| [0] https://github.com/Kindelia/HVM/blob/master/HOW.md
| The_rationalist wrote:
| How does it compare to https://github.com/beehive-lab/TornadoVM
| omginternets wrote:
| If I were serious about porting this project to Go, where would
| you recommend that I start?
| LightMachine wrote:
| You mean, the whole project? Or just the runtime? The runtime
| has recently been ported to go by Caue F. He posted it in our
| Telegram: https://pastebin.com/0X0bbW8b
|
| Perhaps you could team up?
| omginternets wrote:
| Oh my lord, this is seriously the best news of the last
| decade. You, sir -- along with Caue F. -- have just made my
| _decade_!!
|
| EDIT: is there a license for this? Can I use it?
| LightMachine wrote:
| This is MIT licensed, so feel free to fork, use, edit and
| sell it without even notifying me. Now go ahead and get
| rich!
| omginternets wrote:
| I'll get right on that. :)
|
| In all seriousness, thank you. I have exactly zero
| experience with Rust, but if I can help with anything,
| feel free to reach out: @lthibault on GitHub.
|
| Moreover, I'll likely be spinning this off into a full-
| fledged repo of some sort. I'll keep you updated, and am
| more than happy to coordinate our efforts.
|
| Thanks again, and congratulations on this incredible
| piece of engineering!
| cauefcr wrote:
| Hey, this was my port, nice to see people interested.
|
| Yeah, it still needs a few changes on the HVM rust
| compiler to work, but we could figure it out together if
| you want.
|
| Hit me up on @Cauef on telegram, caue.fcr@gmail.com, or
| let's talk on the issue pages of HVM!
| auggierose wrote:
| And another question, is this for purely functional code only,
| or does it / could it also apply to mutable data structures. In
| particular, is it somehow related to copy-on-write techniques
| (like for example used for Swift's data structures), or is this
| something entirely different?
| LightMachine wrote:
| Since HVM is linear, adding some mutability would be
| completely fine and would NOT break referential transparency
| (because values only exist in one place!). So, we could
| actually have "pure mutable arrays". In order to make that
| mix up well with lazy cloning, though, we'd need to limit the
| size of array to about 16. But larger arrays could be made as
| trees of mutable 16-tuples. There was a post about it, but I
| can't find it right now.
| herbstein wrote:
| Based on my understanding on the HOW.md text this relies
| heavily on mathematical equality for performance. In its
| execution it is essentially constantly inlining operations as
| it goes.
| tromp wrote:
| This looks pretty awesome, and holds much promise for the future.
| Optimal beta reduction has always seemed like something of
| theoretical interest only, but Victor has been working many years
| on making it more practical, which deserves a lot of respect.
|
| > HVM files look like untyped Haskell.
|
| Why not make it look exactly like Haskell? So that every valid
| Haskell program is automatically a valid Hvm program, while the
| reverse need not hold due to hvm being untyped.
|
| Instead the syntax looks like a mix of Haskell and Lisp, with
| parentheses around application, and prefix operators. I prefer
| the cleaner Haskell syntax.
|
| Some of the speedup examples look somewhat artificial:
|
| The exponential speedup is on 2^n compositions of the identity
| function, which has no practical use. It would be nice to show
| such a speedup on a nontrivial function.
|
| The arithmetical example uses a binary representation, but
| strangely uses unary implementation of operators, with addition
| implemented as repeated increment, and multiplication as repeated
| addition. Why not use binary implementation of operators? Does
| that not show a good speedup?
| divs1210 wrote:
| > I prefer the cleaner Haskell syntax.
|
| My God, this is written so matter-of-factly that it hurts.
|
| To me, Lisp is awesome BECAUSE of its uniform syntax!
|
| To me, Lisp is waaaaaay cleaner and always unambiguous!
|
| I guess what I'm saying is that it's subjective.
| JonChesterfield wrote:
| Lisp and Haskell are both easier to read than this syntactic
| hybrid of the two, but that might be familiarity
| salimmadjd wrote:
| I totally agree on the syntax, Haskell is far cleaner.
|
| I'm not sure what the reasoning was here. I hope the author or
| others can shed some light.
| sfvisser wrote:
| My guess is the author just picked the simplest syntax to
| parse in order to demonstrate the tech. If it works and shows
| to be successful you can always write a GHC (or whatever)
| backend that compiles to this runtime. Maybe come up with
| some binary IL etc
| hexo wrote:
| Or write self-hosting GHC backend that works like HVM does.
| That would be very neat.
|
| For me, these projects (such as HVM) are great research
| stuff showing us how to do (or not do) things.
| capableweb wrote:
| > I'm not sure what the reasoning was here. I hope the author
| or others can shed some light.
|
| From my point of view, the author almost made it into
| s-expressions, but decided not to go all the way, which (imo)
| would have been amazing and the "cleanest" (although I don't
| like using the term "clean" for code, it's so subjective).
| I'd like to have some light shed over the decision not to go
| all the way.
| fithisux wrote:
| Not very knowledgeable, does it mean it can be a foundation
| for a Scheme compiler?
| [deleted]
| [deleted]
| LightMachine wrote:
| Changing it to pure s-expressions would be easy though, I
| guess just `let` isn't following that rule? I do love the
| no-parenthesis lets though.
| capableweb wrote:
| On a quick scan, it seems to be some more things than
| just `let`. One example would be `(Main n) = (Sum (Gen
| n))` should be closer to `(define Main (n) (Sum (Gen
| n)))` or similar. Not sure the change would be as easy as
| you think, but happy to be proven otherwise ;)
|
| A `let` could assume un-even amount of forms in it and
| only evaluate the last one, using the other ones as
| bindings.
|
| Example from your README: (Main n) =
| let size = (\* n 1000000) let list = (Range
| size Nil) (Fold list lalb(+ a b) 0)
| (define Main (n) (let size (\* n 1000000)
| list (Range size Nil) (Fold list lalb(+ a b)
| 0)))
|
| Could even get rid of the parenthesis for arguments
| (`(n)` => `n`) and treating forms inside `define` the
| same as `let`.
| JonChesterfield wrote:
| Curious, this suggests (lambda a b form) to go along with
| (let a 42 form). I've seen let without the extra parens
| but not define or lambda. Thanks for the aside.
| LightMachine wrote:
| > On a quick scan, it seems to be some more things than
| just `let`. One example would be `(Main n) = (Sum (Gen
| n))` should be closer to `(define Main (n) (Sum (Gen
| n)))` or similar.
|
| Good point.
|
| > Could even get rid of the parenthesis for arguments
| (`(n)` => `n`) and treating forms inside `define` the
| same as `let`.
|
| No, because non-curried functions are a feature. If we
| did that, every function would be curried. Which is nice,
| but non-curried functions are faster (lots of lambdas and
| wasteful copies are avoided using the equational rewrite
| notation), so they should be definitely accessible.
| capableweb wrote:
| Just wanted to clarify that I definitely don't think this
| looks like a bad language as-is, I don't want to give the
| impression because of this small preference, it's less
| valuable (but I'm sure you knew that already). It's
| really impressive design, congratulations on getting it
| out for the world to play with :)
| klysm wrote:
| Well we gotta have _some_ word for subjective quality.
| dkarl wrote:
| We do have "elegant," which to me means "intellectually
| ergonomic." Something can be "beautiful" while being
| totally intimidating and impossible for a human to work
| with, it can be "easy" despite wasteful complexity
| because it you can confidently work through the cruft,
| but "elegant" implies both beauty and ease, fitting
| naturally to our human mental capabilities without
| unnecessary detail.
| LightMachine wrote:
| The reason for the syntax is that HVM aims to be a low level
| compile target, which sounds confusing because closures make
| it look very high level, but it should be seen as LLVM IR. It
| isn't meant for direct human use on the long term. Ideally it
| will be the compile target of languages like Haskell, Lean,
| Idris, Agda, Kind (my language) and others. As such, I just
| went for a syntax that simplifies and speeds up parsing,
| while still keeping it usable if you need to manually edit:
| there is no backtracking on this syntax.
| conaclos wrote:
| Is there some pages that compare Kind and Idris 2?
| LightMachine wrote:
| There aren't. Kind is more stable, is more JS-looking and
| less Haskell-looking, which makes it more practical IMO,
| has a super fast JS compiler and you can write React-like
| apps on it easily, but some work is needed to improve the
| type-checker performance when certain syntax sugars are
| used. The core's performance is superb, though.
|
| Idris2, I can't comment much. All I know is that I envy
| its unification algorithm and synthesis features. Its
| syntax is more haskellish, if you like that. It seems
| less mature in some aspects, though. Very promising
| language overall.
| LightMachine wrote:
| VictorTaelin here. It won't show a speedup because you already
| optimized it to a low level algorithm manually! The point of
| that benchmark is to stress-test the cost of overwhelming
| abstraction. What is really notable is that addition by
| repeated increment on HVM performs as well as addition with a
| carry bit. The former is an elegant one-liner, the later is a
| 8-cases error prone recursive definition. The point is to show
| how you can often write highly abstract, elegant mathematical
| definitions, and it will perform as well as a manually crafted
| version, and that is very cool.
| tromp wrote:
| Oh, you can write addition as repeated increment, and you get
| the efficiency of addition in binary?
|
| Wow; that certainly is impressive.
| LightMachine wrote:
| Yes! The fact HVM can apply a function 2^N times in N steps
| is still mind-blowing to me. I think solutions to important
| problems might come from exploiting this fact. Keep in mind
| you need to use some techniques for that to work. In
| special, there are 3 important rules. I've just written an
| overview here:
| https://github.com/Kindelia/HVM/blob/master/HOW.md#bonus-
| abu...
| chriswarbo wrote:
| > Why not make it look exactly like Haskell? So that every
| valid Haskell program is automatically a valid Hvm program,
| while the reverse need not hold due to hvm being untyped.
|
| > I prefer the cleaner Haskell syntax.
|
| "Haskell syntax" is a pretty bad design in my experience.
| Firstly, it isn't just one thing: there's Haskell 98 and
| Haskell 2010, but most "Haskell" code uses alternative syntax
| from GHC extensions (lambda case, GADTs, type applications,
| view patterns, tuple sections, etc.). (Frustratingly, those
| extensions are often applied implicitly, via a separate .cabal
| file, which makes parsing even harder; plus lots of "Haskell
| code" is actually written as input for a pre-processor, in
| which case all bets are off!)
|
| GHC alone includes two separate representations of Haskell's
| syntax (one used by the compiler, one used by TemplateHaskell).
| Other projects tend to avoid both of them, in favour of
| packages like haskell-src-exts.
|
| I've worked on projects which manipulate Haskell code, and
| getting it to parse was by far the hardest step; once I'd
| managed to dump it to an s-expression representation the rest
| was easy!
| jsnell wrote:
| This had a Show HN a few days ago:
| https://news.ycombinator.com/item?id=30152714
| CyberRabbi wrote:
| A problem with Haskell and with this is that they are inherently
| only suitable for batch processing. You cannot build interactive
| systems that have real-time requirements with these languages
| because how computation is done is not generally under control of
| the programmer.
|
| People attempt to program interactive systems with Haskell but
| then they spend most of their time adapting their program to
| GHC's particular evaluation strategy. Usually the optimized
| program ends up convoluted and nothing like how Haskell code
| should look, additionally still with no guarantees on the run
| time.
| LightMachine wrote:
| That is really not true, but I do agree Haskell passes that
| impression, for the wrong reasons. I'm working hard to fix
| these misconceptions on HVM, Kind-Lang and related projects!
| CyberRabbi wrote:
| It is true and it's not a bug. It's a feature. It's an
| inherent property of the lazy pure functional programming
| model, not any particular language. I can't remember where he
| said this but SPJ himself said that was a design goal of
| Haskell. In C you must specify both how and where
| computations take place. In Java you don't have to worry
| about the where (because memory allocation is automatic) but
| you still how to worry about the how. Haskell goes one step
| further and abstracts both time and space away from the
| programmer. Touting this as a benefit of the language but
| then denying the negative consequences is attempting to have
| your cake and eat it too.
|
| And for the record Java and other garbage collected languages
| are not generally suitable for interactive applications
| either. Anyone who has ever waited on a GC pause can attest
| to that. This is the exact reason Rust exists and why people
| continue to use C/C++ despite being inconvenient languages to
| use.
| LightMachine wrote:
| I do disagree with SPJ here, though. On HVM, you can have
| complete control over how the resources (both space and
| time) are used in your programs and algorithms. That is why
| it outputs the memory (space) and rewrites (time) cost of
| each program you run, and it is so precise you can even
| make formulas of how much memory and how many rewrites your
| functions will demand. You can absolutely have tight memory
| control in HVM, just like in C. Being lazy, high-level,
| etc. is NOT incompatible with that, I'd argue.
| tromp wrote:
| Would you say DOOM is interactive with real-time requirements?
|
| https://github.com/rainbyte/frag
| CyberRabbi wrote:
| The vast majority of the code in that repository is in the IO
| monad and uses carefully placed "!" eager evaluation
| annotations. Both facts only serve to reinforce my point that
| a programmer must have control over the way in which
| computations proceed to build interactive applications.
| Haskell does allow some level of control over this as I said
| but it ends up not looking like Haskell, it looks like C with
| funny syntax.
| travv0 wrote:
| > The vast majority of the code in that repository is in
| the IO monad and uses carefully placed "!" eager evaluation
| annotations.
|
| Looking through that repository, I believe we have
| extremely different definitions of "vast majority."
| CyberRabbi wrote:
| Nearly everything in Render.hs is in the IO monad. That
| is a fact, not a subjective opinion. I point out those
| routines because they are the heart of the application.
| jwlato wrote:
| It's hard to build systems with hard real-time requirements
| with GHC Haskell.
|
| The vast majority of systems people build do not have hard
| real-time requirements. People have built video games, real-
| time audio, and all sorts of other soft-real-time systems with
| Haskell
| CyberRabbi wrote:
| > soft-real-time systems
|
| No they aren't soft real time systems either, most
| applications in general a don't satisfy soft real time
| requirements.
|
| Most people hack it but hacking it with Haskell requires
| rewriting your pure functional code into a form that strongly
| resembles procedural languages like C. This defeats the
| purpose of a lazy pure functional programming language.
| mountainriver wrote:
| Really awesome, any thoughts on autodiff?
| gbrown_ wrote:
| I see the author is replying here so I just wanted to say I
| enjoyed following the Formality posts on your blog and updates on
| GitHub and hope there's time for more of that in the future.
| Wishing you all the best with this project!
|
| As an aside it may be a convenient reference if you laid out the
| history of Formality/Kind as I think a large portion of your
| target audience already knew about Formality. The rename gets a
| little lost in IMHO, at first glance at least.
| [deleted]
| fulafel wrote:
| The submission title says "optimal", the README says "beta-
| optimal", what do they mean in this context and are they true?
| voxl wrote:
| Optimal beta reduction is a very technical term. In effect it
| means any "family" of lambda terms will all be reduced "at
| once." What is a family? Go take two semesters in rewriting
| theory and then perhaps our two heads together can pin it down
| exactly.
|
| In laymen's terms, it means that you're doing a variant of
| call-by-need, except you can be absolutely sure you don't copy
| applications without need.
|
| I am personally skeptical it's a useful idea at all. Machine
| computation is what we really care about (how fast can you push
| instructions through the pipeline) and graph reduction systems
| were already all the rage in the 80s. We gave up on them
| because they didn't interact with the cache well.
|
| So, this is the "motherload" of all graph reduction strategies,
| yet it will get absolutely trounced in settings like numerical
| computation.
| Azsy wrote:
| As a counter argument ( and i'm not 100% sure it holds up ).
|
| The cache failures was because the cache was to small.
| Whereas now we care about CPU OP data dependencies.
| opnitro wrote:
| "Optimal" in this context means it never repeats the work of
| beta reduction when it doesn't have to. Ie, evaluating `(\x ->
| x + x) (2 * 2)` only evaluates `2 * 2` once.
| rowanG077 wrote:
| Why is this special? Doesn't that mean GHC is beta optimal
| since afaik it stores thunks to computations.
| opnitro wrote:
| GHC is not beta optimal, due to some complications around
| what happens when a closures are created. (This is `HOW.md`
| claims)
| fritzo wrote:
| Great work Victor, it's so encouraging to see Asperti &
| Guerrini's research receive engineering attention! Anton
| Salikhmetov also had some nice implementations [1] a few years
| ago. As I understand, even Andrea Asperti didn't believe his
| approach was practical [2] :)
|
| Any idea how hard it would be to extend with a nondeterminism
| operator, as in Plotkin's parallel or? (fork a computation and
| terminate if either branch terminates)
|
| [1] https://dblp.org/pid/49/4772.html
|
| [2] https://arxiv.org/abs/1701.04240
| LightMachine wrote:
| Andrea Asperti's only mistake was thinking he was wrong.
| Labo333 wrote:
| Can someone point me to a reference explaining what beta
| reduction is?
| tromp wrote:
| https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reducti...
|
| Basically, beta-reduction is the single primitive that performs
| all computation in the lambda calculus. When you apply the
| function mapping x to M, to argument N, the result is M with
| all occurences of x replaced by N.
| melony wrote:
| Isn't that the process of compilation?
| agounaris wrote:
| Is there any practical example on this? Whats a common use
| casE?
| chriswarbo wrote:
| > Whats a common use case?
|
| If we expand the discussion from "lambda calculus" to
| "pretty much every programming language", then "beta
| reduction" becomes "calling a function with an argument"
|
| > Is there any practical example on this?
|
| Given the above, you'll be able to find beta-reduction in
| practically all software ever written ;)
| opnitro wrote:
| Any evaluation of a functional-based language is going to
| use this. Here's a simple example:
|
| Let's say I have a function `add1` `add1 = \x -> x + 1` (A
| function that takes a value `x` and then computes `x + 1`
| And then I write the program: `add1 2`
|
| If we want to evaluate this program, first we substitute
| the variable to get `add1 2` -> `(\x -> x + 1) 2`
|
| Then we perform "beta reduction" to get: `(\x -> x + 1) 2`
| -> `2 + 1`
|
| Then it's simple arithmetic: `2 + 1` -> `3`
|
| "The point" here is to have formal rules for defining what
| a computation means. This helps with writing proofs about
| what programs do, or what is possible for programs to do.
|
| For example, say I have a simple program with static types.
| I might want to prove that if the programs type checks,
| type errors will never occur when you run the program. In
| order to do this proof, I have to have some formal notion
| of what it means to "run the program". For a functional
| language, beta reduction is one of those formal rules.
| tsimionescu wrote:
| I will note though that in the actual lambda calculus
| there is no "+", "2" or "1" - it's functions all the way.
|
| 1 is typically defined in the Church encoding as \f -> \x
| -> f x. Addition is \m -> \n -> \f -> \x -> m f (n f x).
| Finding the Church encoding of 2 is left as an exceecise.
|
| We can then use beta reduction to compute 1 + 1 by
| replacing m and n with 1: 1 = \f -> \x ->
| f x (\m -> \n -> \f -> \x -> m f (n f x)) 1 1
| =>beta \f -> \x -> 1 f (1 f x) \f -> \x
| -> 1 f x = (\f -> \x -> f x) f x =>beta 1 f x = f x
| \f -> \x -> 1 f (1 f x) <=> \f -> \x -> 1 f (f x)
| (\f -> \x -> f x) f (f x) =>beta \f -> \x -> f f x
| - the Church encoding of 2.
|
| This is how computation using beta reduction only looks
| like.
| opnitro wrote:
| Yup, was just trying to give an example that utilized
| primitives to make it easier.
| tsimionescu wrote:
| Yes yes, I wanted to add to your example, not to say that
| you said anything wrong!
___________________________________________________________________
(page generated 2022-02-05 23:00 UTC)