by Wouter on November 21, 2008.
Tagged as: Lunches.
I talked about my recent attempts to understand call-by-push-value, a typed lambda calculus that is very precise about when evaluation occurs.
The idea underlying CBPV is to distinguish the type of values and computations. You can think of a value as a fully evaluated Int, String, pair of values, etc. Functions, on the other hand, are computations abstracting over values. I’ve put together an overview of all the types, terms, typing judgements, and evaluation rules(forgive me, but I’d much rather edit large formulas in latex directly than WordPress)
My motivation for this is very different from Paul Levy’s: I’m dreaming of a language with enough laziness to be interesting, but with more predictable memory usage than Haskell. The next step is to figure out how to add (value) data, and (computational) codata, effects (no IO monad), and enough syntactic sugar that you don’t need to be explicit about every thunk/force. There’s a relationship with Conor’s ideas about Frank and the recent work about focussing and duality at CMU that I haven’t managed to nail it down.