Comments on: Call-by-push-value

By: Wouter

Wouter — Sun, 07 Dec 2008 17:07:44 +0000

Justin: No particular reason, I’m afraid. You could just as well give small-step semantics I suppose. Most of these rules are from Paul Levy’s book on CBPV – he may have a better reason than I do.

By: Justin

Justin — Thu, 04 Dec 2008 17:25:02 +0000

Wouter,

Why the choice for big-step evaluation rules rather than single-step in your PDF? Just curious.

By: Noam

Noam — Mon, 24 Nov 2008 14:53:17 +0000

Paul: I meant both lazy and eager. Specifically I’m thinking of Haskell, where both lambdas and lazy pairs are considered “values”. You could argue that that is misleading terminology, but in any case it’s a potential source of confusion with cbpv.

By: Paul

Paul — Mon, 24 Nov 2008 12:50:41 +0000

Noam: when you say “in ordinary functional programming, lambdas are values”, does
“ordinary” mean lazy or eager? If you mean eager, I agree that lambdas are values, but cbv lambda translates into thunk lambda, so it remains a value in cbpv.

By: Andrej Bauer

Andrej Bauer — Sun, 23 Nov 2008 10:10:27 +0000

You might be interested in looking at the toy language "levy" in my Programming Languages Zoo. It closely follows Paul Levy's call-by-push-value language and might be a good starting point for experimentation with call-by-push-value.

By: Noam

Noam — Sat, 22 Nov 2008 18:09:53 +0000

Wouter/Hank: so I think the terminology "value" vs "computation" is a bit misleading, because in ordinary functional programming, lambda's are values. The way Paul explains value types vs computation types is in terms of the semantics: value types are modelled by sets, computation types by algebras. The coercions F (turning a value type into a computation type) and U (turning a computation type into a value type) represent an adjunction between sets and algebras (hence Paul's use of the symbols F and U, by analogy to the free algebra functor, and the underlying set functor). So rather than thinking of computations as modelled by "computation types" as such, it's better to think of them as modelled by this adjunction. The unity of duality paper also had some misleading terminology, and these days I like to speak of both positive and negative values, and positive and negative continuations. My favorite way to think about these is in terms of pattern-matching: positive types are eliminated (i.e., we build positive continuations) by pattern-matching, while negative types are introduced (i.e., we build negative values) by pattern-matching. This explains why the ordinary function space of functional programming is negative, because we define functions by pattern-matching. (A positive function space would be weird, because it would be eliminated by pattern-matching...but indeed that's what the paper on "focusing on binding and computation" is about.) A slightly subtle point, though, is that we build negative values by pattern-matching against patterns of destructors. It so happens that a destructor pattern for A -> B contains a constructor pattern for A (and a destructor pattern for B). You can also think of the negative type of lazy pairs: the way we build a lazy pair is by pattern-matching against the two possible destructors, fst and snd, saying what value to return in each case.

By: Wouter

Wouter — Sat, 22 Nov 2008 11:17:27 +0000

Jean-Philippe: You may want to have a look at some of Noam Zeilberger’s papers. He has written quite a lot about focusing. On the unity of duality is probably a good place to start.

I don’t think Conor’s ever written anything up about Frank, but you might be interested in the slides of his talk at the Effects in Type Theory Workshop.

Noam: Thanks for your reply! I’ve had “Read Noam’s Agda code” on my “Todo someday” list for about a year now. I guess I got distracted by writing my thesis

Ralf Hinze was visiting when I gave talked about this and he asked an interesting question: why does the function space necessarily build computation types? I’m afraid I couldn’t give him a satisfactory answer. Do you have a convincing explanation?

Hank: Computation types are what Noam calls “negative types” – types characterised by their elimination rules rather than their introduction rules. For example, the function space operator build computation types. In Paul and Noam’s work, functions abstract over value types but return computation types. Inhabitants of Nat would be values (which is different from a computation that will return a Nat).

By: Hank

Hank — Fri, 21 Nov 2008 22:05:27 +0000

Wouter, I don’t think I know what a computation is.

Is Nat a value or a computation?

Hank

By: Noam

Noam — Fri, 21 Nov 2008 17:56:29 +0000

There's a very close relationship between CBPV and focusing. You can view the types of CBPV as formulas of polarized intuitionistic logic: value types are positive formulas, computation types are negative. At the DTP workshop last spring, I went through some agda code that shows how to view proofs in a focused sequent calculus for polarized intuitionistic logic as pattern-matching programs. There's a pretty simple translation guide between this syntax and CBPV. (We came up with it when Paul Levy was visiting CMU this summer, but haven't written it down anywhere...hmm...) The only significant differences between focused, polarized IL and CBPV is that the former distinguishes a few more syntactic categories, and more importantly, that we build "inversion" constructs (i.e., elimination of positive/value types, or introduction of negative/computation types) by "maximally deep" pattern-matching. For example, to eliminate a positive/value type, we have to pattern-match all the way down to variables of negative/computation type. But this idea also shows up in the semantics of CBPV, with what Levy and Soren Lassen called "ultimate pattern-matching". It makes it a lot easier to reason about the operational behaviour of programs.

By: Jean-Philippe Bernardy

Jean-Philippe Bernardy — Fri, 21 Nov 2008 16:50:47 +0000

Care to give pointers for the references you mention? (Frank, focussing)
Thanks!