[HN Gopher] I'm Betting on Call-by-Push-Value
       ___________________________________________________________________
        
       I'm Betting on Call-by-Push-Value
        
       Author : todsacerdoti
       Score  : 48 points
       Date   : 2024-03-09 18:56 UTC (4 hours ago)
        
 (HTM) web link (thunderseethe.dev)
 (TXT) w3m dump (thunderseethe.dev)
        
       | falcor84 wrote:
       | I really want to like this more, but need a better notation
        
       | rezonant wrote:
       | Can someone TLDR this? It's pretty thick, and I can't help but
       | think this is a solved problem with the ability to pass functions
       | as arguments. What's the new insight here?
        
         | amluto wrote:
         | I can't. I think it would have been nice if the article defined
         | the terminology it used to describe its toy languages.
         | 
         | But it really seemed like it was describing a language like C++
         | or Rust where a "computation" is a value that happens to be a
         | callable function (std::function<int ()> or Fn() -> int, for
         | example). A thunk is a value of callable (computable? is this
         | really different?) type, and Return is the magic operation that
         | wraps a value into a trivial closure, like:
         | [val]() { return val; }
         | 
         | in C++.
         | 
         | Maybe there's more to it than that.
        
         | crq-yml wrote:
         | If you're in eager evaluation land, everything evaluates as you
         | come to it, so you can handle all arguments at runtime by using
         | a stack and no problem is felt. Once we say, "actually we don't
         | evaluate until it's used" ambiguity arises.
         | 
         | So the context of this is to solve a problem-in-practice with
         | arguments in a lazy evaluation environment, which is that you
         | don't know how many arguments you need to supply without doing
         | the evaluation.
        
           | analognoise wrote:
           | Is that what they mean by "calculating the arity"?
        
       | burakemir wrote:
       | It is nice to see CBPV on HN. It is a calculus that deal with a
       | fundamental choice in PL of how to approach evaluation. For a
       | different take, here is the first part of a mini series of posts
       | on CBPV that aims at working out the connection to logic
       | ("polarised natural deduction"): https://burakemir.ch/post/cbpv-
       | pt1-small-steps/
        
       ___________________________________________________________________
       (page generated 2024-03-09 23:00 UTC)