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?!
Thanks for the link, I'm encouraged whenever I hear that my writing isn't totally incomprehensible.
ReplyDeleteI'd love to write some more example posts that informally explore programming in the Levy implementation of CBPV; it might be helpful to extend Andrej's interpreter with some effects (like print) to make more informative examples possible and interesting.
Any requests?
Oh, and another comment. That example? It can (basically) be written in Standard ML too:
ReplyDelete(print "hello1"; (fn z => (print ("we just popped " ^ z); ...)))
This is an ML expression of type (string -> whatever), where the "whatever" depends on the contents of "...". This is non-mysterious to the ML programer: it will print "hello1", and then return a function that, given a string "s", prints "we just popped s".
Now, we can also thunk things in Standard ML, but we do everything with functions, including thunking, so it looks like this:
let f = (fn () => (print "hello1"; (fn z => (print ("we just popped" ^ z); ...)))
So there's very little funny business going on in that example by Levy: the only curiosity of CBPV is that I believe it's not possible to partially apply that particular expression, so you can't do something analogous to what you could do in our ML example, which is to write
let g = f () in (g " the first one"; g " the second one")
which will print "hello1we just popped the first onewe just popped the second one". For the CBPV thunk you gave, whenever you print "we just popped" it will print immediately after the accompanying "hello1" is printed - there's no way to get the effect of printing "hello1" unless you've already supplied the accompanying argument "z". (Why is this? Oh, I know the title of my next Request for Logic blog post now...)
Hi Rob, thanks for your replies.
ReplyDeleteFor me the big question is how the "fine structure exposed by" CBPV can help us in practical programming (languages).
I've finally made something like an attempt to answer the questions you asked way back a long time ago. I'm sure I did an imperfect job, but hopefully this is informative.
ReplyDeleteThe title I was alluding to above was going to be "functions aren't values," because functions are computation (negative) types, so they aren't values, they're computations! (It's suspended - or thunked - functions that are values.) But that got lost in revision.