Abstracts.2020.CBPV

Call-By-Push-Value

by Andreas Abel

Abstract

This will be a talk about call-by-push-value.

The main reference is Paul Levy's PhD thesis [1].

Below is an excerpt of the abstract.

"Call-by-push-value (CBPV) is a new programming language paradigm, based on the slogan “a value is, a computation does”. We claim that CBPV provides the semantic primitives from which the call-by-value and call-by-name paradigms are built…"

If you are curious on why to care about CBPV, check out the FAQ [1].

Notes

1. Motivation: Lazy effects

   foo :: a -> IO a
   foo = do
     putStrLn "function"
     \ a -> do
        putStrLn "argument"
        return a

2. Introduction to monads and monad algebras (see Hutton.hs and Chapter 5, in particular §5.2 and §5.4, in Emily Riehl's book [6])

3. Frank Pfenning's lecture notes [3] give, starting at natural deduction, a polarization of formulas that yields the CBPV calculus. Formulas are separated into positive or value types that can serve as hypotheses (and also as conclusion) and negative or computation types that can only serve as conclusion. The positive formulas are disjoint sums (tagged unions) and eager tuples, both with sequent-style elimination rules (i.e., pattern matching), plus embedding of negative formulas which is interpreted as thunking. The negative formulas are function types and lazy tuples (record types), both with natural-deduction style elimination rules. Note that the domain of a function type is positive, since it serves as hypothesis in the typing of the function body. Further, positive types are embedded into negative types, interpreted as the monad with elimination via bind.

   The lecture notes argue how the CBPV calculus arises necessarily from the polarization of formulas and the decision that only positive formulas can play the role of hypotheses.

References

1. ^ ^{a b} Paul Blain Levy. 2001. Call-By-Push-Value. Thesis, FAQ.

Bibliography

1. Paul Blain Levy. 2006. Call-By-Push-Value: Decomposing Call-By-Value and Call-By-Name. HOSC paper.
2. Paul Blain Levy. 2016. A Tutorial on Call-By-Push-Value. Slides.
3. ^ Frank Pfenning. 2016. 15-816 Substructural Logics: Call-by-Push-Value. Notes.
4. Andreas Abel and Christian Sattler. 2019. Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda-Calculus. PPDP paper.
5. Andreas Abel. 2020. Graded Call-By-Push-Value. Preprint.
6. ^ Emily Riehl. 2015–2016. Category Theory in Context. Book.