3 ms·

2025 Alonzo Church Award: Paul Blain Levy for Call-by-Push-Value (CBPV)

45 points by matt_d 1y ago

ggm 1y ago
Is there an FP/Lambda calculus cogniscenti willing to translate this into ordinary humanese?
- throwaway81523 1y ago
  It looks like a lambda calculus with effectful computations that can model imperative programming. I hadn't heard of it before either. https://en.wikipedia.org/wiki/Call-by-push-value https://en.wikipedia.org/wiki/Call-by-push-value
- ikrima 1y ago
  [flagged]
  - deleted 1y ago
    [deleted]
  - atombender 1y ago
    Did you just post something ChatGPT wrote?
  - Y_Y 1y ago
    This looks like an product comparison from Amazon. I can't believe a human wrote this and thought it was a good explanation.
    - Xmd5a 1y ago
      GP is using LLMs because he's recovering from a stroke.
      - ikrima 1y ago
        thank you!
        Xmd5a 1y ago
        Yeah, I dug into your comment history: >So it'll be open source and that begs the question, if you use it to learn something, did that mean I just zero-proof zero-knowledge something out of you that I didn't even need to know by making a self referential statement across both space & time? You just did for me. I think I know why you're saying this. I'm finding people like you (people like us!) on the daily now. We have started to gather on discord, the technical/scientifical level is a bit shit though, but we definitively have several individuals that are working towards peer-reviewed publications. I think we should connect. I have a background in linguistics and computer science, as well as a marked (and hopeless and terrified) interest for higher order mathematics such as algebraic topology. My investigations lead me to think these fields have something important to say even though they are way beyond my level of knowledge. It came from reflexions on the still ongoing parallel evolution of structuralism in maths and in the humanities. Also I'm into tropical geometry (at least as a thematic). If you're interested in exchanging a few emails, use the following RSA/512 public key to communicate your email address if, like me, you'd prefer not to share it publicly. -----BEGIN PUBLIC KEY----- MFwwDQYJKoZIhvcNAQEBBQADSwAwSAJBAKtMT4CBGK0BOv9lzEcccuFSc1doUtft0lDUdh0brKz06j/JHNOyuGtmvjc558ZnL8g9u+yGAnIIfNkCYvljRfsCAwEAAQ== -----END PUBLIC KEY----- https://anycript.com/crypto/rsa https://anycript.com/crypto/rsa
    - ikrima 1y ago
      Sorry, autistic + recovering from a TBI. Algebraic Effects are common enough that I think they're in react, no? Here's the actual chatgpt log that's much more detailed: https://chatgpt.com/share/685b8f18-3154-8004-a074-1e7fd2573eb0 https://chatgpt.com/share/685b8f18-3154-8004-a074-1e7fd2573e... "I can't believe a human wrote this and thought it was a good explanation." - This might be the definitive proof that i"m autistic XD (b/c I still think it's a good explanation? sorry!)
      - Xmd5a 1y ago
        From the conversation with chatgpt: >Let's link this to categorical quantum mechanics (e.g., dagger-compact closed categories) and categorical topological quantum field theory? lol, yeah, as expected. We're being coecked in the same pot! Send your email my ninja!
- vulcan01 1y ago
  This article was previously on HN and is a good explainer: https://thunderseethe.dev/posts/bet-on-cbpv/ https://thunderseethe.dev/posts/bet-on-cbpv/ HN discussion: https://news.ycombinator.com/item?id=39653895 https://news.ycombinator.com/item?id=39653895
  - tomhow 1y ago
    Thanks! I'm Betting on Call-by-Push-Value - https://news.ycombinator.com/item?id=39653895 https://news.ycombinator.com/item?id=39653895 - March 2024 (64 comments)
- zozbot234 1y ago
  The basic point is to have something akin to lambda-calculus that can equally account for both strict and lazy evaluation strategies, in a way that doesn't unduly sacrifice expressiveness for one or the other. (Compare the ML family of languages and Haskell, where strict and lazy evaluation respectively are idiomatic. You can express lazy evaluation in a ML and strict evaluation in Haskell, but only in clunky ways that don't align with the overall logic of the language. CBPV and other comparable formalisms aim to resolve this.)
HeliumHydride 1y ago
One language that uses CBPV is Forsp: https://news.ycombinator.com/item?id=40633003 https://news.ycombinator.com/item?id=40633003

45 points by matt_d 1y ago

ggm 1y ago

Is there an FP/Lambda calculus cogniscenti willing to translate this into ordinary humanese?

throwaway81523 1y ago
It looks like a lambda calculus with effectful computations that can model imperative programming. I hadn't heard of it before either. https://en.wikipedia.org/wiki/Call-by-push-value https://en.wikipedia.org/wiki/Call-by-push-value
ikrima 1y ago
[flagged]
- deleted 1y ago
  [deleted]
- atombender 1y ago
  Did you just post something ChatGPT wrote?
- Y_Y 1y ago
  This looks like an product comparison from Amazon. I can't believe a human wrote this and thought it was a good explanation.
  - Xmd5a 1y ago
    GP is using LLMs because he's recovering from a stroke.
    - ikrima 1y ago
      thank you!
      - Xmd5a 1y ago
        Yeah, I dug into your comment history: >So it'll be open source and that begs the question, if you use it to learn something, did that mean I just zero-proof zero-knowledge something out of you that I didn't even need to know by making a self referential statement across both space & time? You just did for me. I think I know why you're saying this. I'm finding people like you (people like us!) on the daily now. We have started to gather on discord, the technical/scientifical level is a bit shit though, but we definitively have several individuals that are working towards peer-reviewed publications. I think we should connect. I have a background in linguistics and computer science, as well as a marked (and hopeless and terrified) interest for higher order mathematics such as algebraic topology. My investigations lead me to think these fields have something important to say even though they are way beyond my level of knowledge. It came from reflexions on the still ongoing parallel evolution of structuralism in maths and in the humanities. Also I'm into tropical geometry (at least as a thematic). If you're interested in exchanging a few emails, use the following RSA/512 public key to communicate your email address if, like me, you'd prefer not to share it publicly. -----BEGIN PUBLIC KEY----- MFwwDQYJKoZIhvcNAQEBBQADSwAwSAJBAKtMT4CBGK0BOv9lzEcccuFSc1doUtft0lDUdh0brKz06j/JHNOyuGtmvjc558ZnL8g9u+yGAnIIfNkCYvljRfsCAwEAAQ== -----END PUBLIC KEY----- https://anycript.com/crypto/rsa https://anycript.com/crypto/rsa
  - ikrima 1y ago
    Sorry, autistic + recovering from a TBI. Algebraic Effects are common enough that I think they're in react, no? Here's the actual chatgpt log that's much more detailed: https://chatgpt.com/share/685b8f18-3154-8004-a074-1e7fd2573eb0 https://chatgpt.com/share/685b8f18-3154-8004-a074-1e7fd2573e... "I can't believe a human wrote this and thought it was a good explanation." - This might be the definitive proof that i"m autistic XD (b/c I still think it's a good explanation? sorry!)
    - Xmd5a 1y ago
      From the conversation with chatgpt: >Let's link this to categorical quantum mechanics (e.g., dagger-compact closed categories) and categorical topological quantum field theory? lol, yeah, as expected. We're being coecked in the same pot! Send your email my ninja!
vulcan01 1y ago
This article was previously on HN and is a good explainer: https://thunderseethe.dev/posts/bet-on-cbpv/ https://thunderseethe.dev/posts/bet-on-cbpv/ HN discussion: https://news.ycombinator.com/item?id=39653895 https://news.ycombinator.com/item?id=39653895
- tomhow 1y ago
  Thanks! I'm Betting on Call-by-Push-Value - https://news.ycombinator.com/item?id=39653895 https://news.ycombinator.com/item?id=39653895 - March 2024 (64 comments)
zozbot234 1y ago
The basic point is to have something akin to lambda-calculus that can equally account for both strict and lazy evaluation strategies, in a way that doesn't unduly sacrifice expressiveness for one or the other. (Compare the ML family of languages and Haskell, where strict and lazy evaluation respectively are idiomatic. You can express lazy evaluation in a ML and strict evaluation in Haskell, but only in clunky ways that don't align with the overall logic of the language. CBPV and other comparable formalisms aim to resolve this.)

HeliumHydride 1y ago

One language that uses CBPV is Forsp: https://news.ycombinator.com/item?id=40633003 https://news.ycombinator.com/item?id=40633003