This is your brain on CBPV

Rob Simmons has written an amazing new post - What does focusing tell us about language design? - on Call-by-Push-Value, an exciting new paradigm that exposes previously hidden fine structure of computation (previously).

I'm a PL dilettante, so I can't follow the theory behind CBPV but it just seems right, and the thinking and writing behind it and articles like Rob's are clear, highly insightful, and practical.

Call-by-push-value

Call-by-push-value has a seducing PR message: Science is reductionism. Once the fine structure has been exposed, why ignore it?

Unfortunately, I'm too unsophisticated to be able to gain much insight from the CBPV papers. There's an introduction to CBPV for more mortal-like folks. Other material is hard to find.

What caught my eye was the following code sample from Paul Blain Levy's (rhymes with "all plain Stevie") PhD thesis:

thunk(print "hello1"; λz. print "we just popped" z; ...)

So, apparently you can do stuff in a function before you're even taking arguments. Interested!

Maybe one of you can provide more information about this interesting new thing?!