Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthormaxsnew
   • CommentTimeApr 20th 2018
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexQuick idea section for call-by-push-value <a href="https://ncatlab.org/nlab/revision/call-by-push-value/1">v1</a>, <a href="https://ncatlab.org/nlab/show/call-by-push-value">current</a>

   Quick idea section for call-by-push-value

   v1, current

2. • CommentRowNumber2.
   • CommentAuthormaxsnew
   • CommentTimeJul 17th 2018
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexAn overview of some of CBPV, specifically its judgments and the $F,U$ types. Mostly wanted to record this presentation of the mode theory Dan Licata and I worked out. <a href="https://ncatlab.org/nlab/revision/diff/call-by-push-value/2">diff</a>, <a href="https://ncatlab.org/nlab/revision/call-by-push-value/2">v2</a>, <a href="https://ncatlab.org/nlab/show/call-by-push-value">current</a>

   An overview of some of CBPV, specifically its judgments and the $F,U$ types. Mostly wanted to record this presentation of the mode theory Dan Licata and I worked out.

   diff, v2, current

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeJul 18th 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWe should fill in CBV and CBN. Is this [post](https://bambielli.com/til/2016-07-24-CBV-vs-CBN/) a good start?

   We should fill in CBV and CBN. Is this post a good start?

4. • CommentRowNumber4.
   • CommentAuthorjonsterling
   • CommentTimeOct 16th 2018
   • PermaLink
   Author: jonsterling
   Format: MarkdownItexI would like to better understand the remark that says of F, "It is a positive computation type, with invertible elimination rule...". I am very suspicious of this remark for the following reasons: 1. Computation types are negative (or at least, so I thought) --- there is an account of CBPV as the natural deduction account of polarized intuitionistic logic, in which F and U are the up and downshift connectives respectively, and these are by definition respectively negative and positive. 2. Whether an elimination rule is invertible is neither here nor there when determining the polarity of a connective. Polarity arises from the invertibility of the left and right rules in (linear) sequent calculus.

   I would like to better understand the remark that says of F, “It is a positive computation type, with invertible elimination rule…”. I am very suspicious of this remark for the following reasons:

   1. Computation types are negative (or at least, so I thought) — there is an account of CBPV as the natural deduction account of polarized intuitionistic logic, in which F and U are the up and downshift connectives respectively, and these are by definition respectively negative and positive.

   2. Whether an elimination rule is invertible is neither here nor there when determining the polarity of a connective. Polarity arises from the invertibility of the left and right rules in (linear) sequent calculus.

5. • CommentRowNumber5.
   • CommentAuthormaxsnew
   • CommentTimeOct 16th 2018
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexThe statement that F is positive and U is negative do refer to the invertibility of their elimination and introduction rules. Any stack out of $FA$ in cbpv is equivalent to one of the form $\bullet to x. M$ and any value of type $UB$ is equivalent to one of the form $thunk M$ and their other rules are not invertible: there are computations of $F A$ not equivalent to $return V$ (for instance one that prints a string before returning) and there are computations with free variable $x : UB$ that are not equivalent to $S[force x/\bullet]$ (for instance something that doesn't use $x$ at all. Re 1: Can you give a reference for a specific system of polarized intuitionistic logic so that I can see if I can make sense of this difference? Re 2: Are you saying the notion of polarity only makes sense in the context of sequent calculus? And in this case the F and U types do not have the polarities I've described? If so then what would you consider to be the correct description in CBPV? It is the case that in the semantics of CBPV all value connectives except U have a "mapping out" universal property, and U has a "mapping in" universal property, whereas all computation connectives except F have mapping in universal properties and F has a "mapping in" universal property. It was my understanding that this aspect of the semantics is what corresponds to polarity of connectives, but maybe you are saying that a logician would disagree with this?

   The statement that F is positive and U is negative do refer to the invertibility of their elimination and introduction rules. Any stack out of $FA$ in cbpv is equivalent to one of the form $\bullet to x. M$ and any value of type $UB$ is equivalent to one of the form $thunk M$ and their other rules are not invertible: there are computations of $F A$ not equivalent to $return V$ (for instance one that prints a string before returning) and there are computations with free variable $x : UB$ that are not equivalent to $S[force x/\bullet]$ (for instance something that doesn’t use $x$ at all.

   Re 1: Can you give a reference for a specific system of polarized intuitionistic logic so that I can see if I can make sense of this difference?

   Re 2: Are you saying the notion of polarity only makes sense in the context of sequent calculus? And in this case the F and U types do not have the polarities I’ve described?

   If so then what would you consider to be the correct description in CBPV? It is the case that in the semantics of CBPV all value connectives except U have a “mapping out” universal property, and U has a “mapping in” universal property, whereas all computation connectives except F have mapping in universal properties and F has a “mapping in” universal property. It was my understanding that this aspect of the semantics is what corresponds to polarity of connectives, but maybe you are saying that a logician would disagree with this?

6. • CommentRowNumber6.
   • CommentAuthorjonsterling
   • CommentTimeOct 16th 2018
   • PermaLink
   Author: jonsterling
   Format: MarkdownItex1. Invertibility of intro and elimination rules is not a reliable way to measure polarity; but maybe you are meaning something completely different from what we mean by "invertibility" in structural proof theory and proof search. At least according to the sense that we mean by "invertibility of rules" in proof theory, not even disjunction would be positive if we looked at its natural deduction elimination rule. 2. Here's some lecture notes on CBPV from Frank Pfenning: https://www.cs.cmu.edu/~fp/courses/15816-f16/lectures/21-cbpv.pdf. Well, he calls it CBPV, but it is just polarized intuitionistic logic; if you happen to be right about the polarity, then this mustn't be actually CBPV. Note that in this presentation, you can't really measure invertibility, because that is a property of sequent calculus. to see how the shift connectives work in polarized intuitionistic sequent calculus, see Rob Simmons' paper: https://www.cs.cmu.edu/~rjsimmon/drafts/focus.pdf. Notice how in the sequent calculus, the upshift is negative and the downshift is positive. And this calculus is sound and complete for the calculus that Frank presents in CBPV note, and moreover, the rules in the CBPV note seem to be the same as CBPV a la Levy, modulo notation. 3. I'm saying that the easiest way to observe polarity of a connective is through sequent calculus, but there are other ways too which have to do with eta rules; IMO these are more subtle, and should actually be understood as *arising* from the more primitive notion of polarity that I describe. Mapping-in vs mapping-out in category theory doesn't usually determine polarity, because in many categorical models, these are two presentations of the universal property of the same connective. (This corresponds to how in intuitionistic logic, there is not semantic distinction between the positive and the negative conjunction). Of course, in a sufficiently rarefied categorical model the real differences can be observed. Anyway, I'm just feeling a little confused here and I'd like to square what I see in this post with my intuitions from structural proof theory, and what I've read in the work of Pfenning, Zeilberger, Munch, etc.

   1. Invertibility of intro and elimination rules is not a reliable way to measure polarity; but maybe you are meaning something completely different from what we mean by “invertibility” in structural proof theory and proof search. At least according to the sense that we mean by “invertibility of rules” in proof theory, not even disjunction would be positive if we looked at its natural deduction elimination rule.

   2. Here’s some lecture notes on CBPV from Frank Pfenning: https://www.cs.cmu.edu/~fp/courses/15816-f16/lectures/21-cbpv.pdf. Well, he calls it CBPV, but it is just polarized intuitionistic logic; if you happen to be right about the polarity, then this mustn’t be actually CBPV. Note that in this presentation, you can’t really measure invertibility, because that is a property of sequent calculus. to see how the shift connectives work in polarized intuitionistic sequent calculus, see Rob Simmons’ paper: https://www.cs.cmu.edu/~rjsimmon/drafts/focus.pdf. Notice how in the sequent calculus, the upshift is negative and the downshift is positive. And this calculus is sound and complete for the calculus that Frank presents in CBPV note, and moreover, the rules in the CBPV note seem to be the same as CBPV a la Levy, modulo notation.

   3. I’m saying that the easiest way to observe polarity of a connective is through sequent calculus, but there are other ways too which have to do with eta rules; IMO these are more subtle, and should actually be understood as arising from the more primitive notion of polarity that I describe. Mapping-in vs mapping-out in category theory doesn’t usually determine polarity, because in many categorical models, these are two presentations of the universal property of the same connective. (This corresponds to how in intuitionistic logic, there is not semantic distinction between the positive and the negative conjunction). Of course, in a sufficiently rarefied categorical model the real differences can be observed.

   Anyway, I’m just feeling a little confused here and I’d like to square what I see in this post with my intuitions from structural proof theory, and what I’ve read in the work of Pfenning, Zeilberger, Munch, etc.

7. • CommentRowNumber7.
   • CommentAuthormaxsnew
   • CommentTimeOct 17th 2018
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexOk it looks like I'm certainly using Positive/Negative differently from those papers, because they are defining that value type means positive and computation type means negative. I certainly don't mean that F is a value type and U is a computation type. I mean mapping in vs mapping out UP. For the F and U types there is certainly no ambiguity here that F has a mapping out UP and U has a mapping in UP.

   Ok it looks like I’m certainly using Positive/Negative differently from those papers, because they are defining that value type means positive and computation type means negative. I certainly don’t mean that F is a value type and U is a computation type.

   I mean mapping in vs mapping out UP. For the F and U types there is certainly no ambiguity here that F has a mapping out UP and U has a mapping in UP.

8. • CommentRowNumber8.
   • CommentAuthorjonsterling
   • CommentTimeOct 17th 2018
   • PermaLink
   Author: jonsterling
   Format: MarkdownItexAlright -- I feel that there are still questions to figure out here, because in proof theory one cannot just declare by fiat that value types are "positive" and computation types are "negative". The reason that assignment works out is semantical, and it seems to suggest to me that maybe there is some subtle difference in the adjunctions that we are considering. For instance, something I have never completely understood, is the fact that in some models of polarity, the up-shift and the downshift are left and right adjoints respectively, whereas in other models, they are right and left adjoints. I think Guillaume Munch would be the right person to explain it to us, since I never got far enough to understand those details fully. (And I'm not sure if this is related, I just thought I'd mention it, since it's another subtlety.)

   Alright – I feel that there are still questions to figure out here, because in proof theory one cannot just declare by fiat that value types are “positive” and computation types are “negative”. The reason that assignment works out is semantical, and it seems to suggest to me that maybe there is some subtle difference in the adjunctions that we are considering. For instance, something I have never completely understood, is the fact that in some models of polarity, the up-shift and the downshift are left and right adjoints respectively, whereas in other models, they are right and left adjoints. I think Guillaume Munch would be the right person to explain it to us, since I never got far enough to understand those details fully. (And I’m not sure if this is related, I just thought I’d mention it, since it’s another subtlety.)

9. • CommentRowNumber9.
   • CommentAuthormaxsnew
   • CommentTimeOct 18th 2018
   • (edited Oct 18th 2018)
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexI'm not sure if that explains everything about our confusion here, but the difference in whether upshift is a right or left adjoint is explained in this paper by Guillaume: https://hal.inria.fr/hal-00996729 . Specifically section 3.2 constructs a duploid from a (unary) CBPV model (an adjunction) where the left adjoint is the upshift, and then section 3.4 describes the adjunction arising from a duploid where the upshift is a right adjoint. The difference is that when upshift is a left adjoint, the adjunction is between the *pure* terms, i.e. values and stacks, and is the semantics for CBPV: the stack judgment F A |- B is naturally isomorphic to the value judgment A |- U B (Guillaume calls U G since U usually means a forgetful functor and any strong adjunction will do. On the other hand, when upshift is a right adjoint, the adjunction is between *effectful* terms, i.e. CBV effectful terms between positive types and CBN effectful terms between negative types. If we look at a duploid arising from a CBPV adjunction, then this is an adjunction between the Kleisli $(A \to_{cbv} A' = A \to F A')$ and Co-Kleisli $(B \to_{cbn} B' = U B \to B')$ categories of the adjunction. Then $\Uparrow = F, \Downarrow = U$ at the level of objects, and the equivalence is $\Downarrow B \to_{cbv} A = U B \to F A = B \to_{cbn} \Uparrow A$. So I guess the page should instead say the $F$ is a left adjoint and $U$ is a right adjoint rather than using polarity terminology.

   I’m not sure if that explains everything about our confusion here, but the difference in whether upshift is a right or left adjoint is explained in this paper by Guillaume: https://hal.inria.fr/hal-00996729 . Specifically section 3.2 constructs a duploid from a (unary) CBPV model (an adjunction) where the left adjoint is the upshift, and then section 3.4 describes the adjunction arising from a duploid where the upshift is a right adjoint.

   The difference is that when upshift is a left adjoint, the adjunction is between the pure terms, i.e. values and stacks, and is the semantics for CBPV: the stack judgment F A |- B is naturally isomorphic to the value judgment A |- U B (Guillaume calls U G since U usually means a forgetful functor and any strong adjunction will do.

   On the other hand, when upshift is a right adjoint, the adjunction is between effectful terms, i.e. CBV effectful terms between positive types and CBN effectful terms between negative types. If we look at a duploid arising from a CBPV adjunction, then this is an adjunction between the Kleisli $(A \to_{cbv} A' = A \to F A')$ and Co-Kleisli $(B \to_{cbn} B' = U B \to B')$ categories of the adjunction. Then $\Uparrow = F, \Downarrow = U$ at the level of objects, and the equivalence is $\Downarrow B \to_{cbv} A = U B \to F A = B \to_{cbn} \Uparrow A$.

   So I guess the page should instead say the $F$ is a left adjoint and $U$ is a right adjoint rather than using polarity terminology.

10. • CommentRowNumber10.
    • CommentAuthormaxsnew
    • CommentTimeOct 18th 2018
    • PermaLink
    Author: maxsnew
    Format: MarkdownItexAvoid polarity terminology. <a href="https://ncatlab.org/nlab/revision/diff/call-by-push-value/4">diff</a>, <a href="https://ncatlab.org/nlab/revision/call-by-push-value/4">v4</a>, <a href="https://ncatlab.org/nlab/show/call-by-push-value">current</a>

    Avoid polarity terminology.

    diff, v4, current

11. • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 18th 2018
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI'm not following all the subtleties here, but are we still OK in our descriptions of [[negative type]] and [[positive type]]?

    I’m not following all the subtleties here, but are we still OK in our descriptions of negative type and positive type?

12. • CommentRowNumber12.
    • CommentAuthormaxsnew
    • CommentTimeOct 18th 2018
    • PermaLink
    Author: maxsnew
    Format: MarkdownItexI'm not sure, I was going to bring that up as well

    I’m not sure, I was going to bring that up as well

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJan 25th 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexThe first sentence of this entry started out as: > Call-by-push-value is a type theory and programming language which contains... This does not seem to make (grammatical) sense.(?) I am assuming what is meant is something as follows (emphasis added): > Call-by-push-value is a type theory and programming language **paradigm** which **subsumes** I have taking the liberty/chance to edit this accordingly. But if any expert is seeing this, please feel invited to adjust. In fact, if such experts are around, it would be a great service if you could create the promised entries * *[[call-by-value]]* * *[[call-by-name]]* which are referred to here and in a rather large number of other entries (see [here](https://www.google.com/search?client=firefox-b-d&q=%22call-by-value%22+site%3Ancatlab.org) and [here](https://www.google.com/search?q=%22call-by-name%22+site%3Ancatlab.org&client=firefox-b-d&sxsrf=AJOqlzWeW6k5_5TJin0BzSmXgB19q4JVOg%3A1674665095095&ei=h1zRY8S5BcHxkwWd6oKYBA&ved=0ahUKEwiEmfHQleP8AhXB-KQKHR21AEMQ4dUDCA4&uact=5&oq=%22call-by-name%22+site%3Ancatlab.org&gs_lcp=Cgxnd3Mtd2l6LXNlcnAQA0oECEEYAUoECEYYAFAAWABgK2gBcAB4AIABAIgBAJIBAJgBAMABAQ&sclient=gws-wiz-serp)) but which remain missing. <a href="https://ncatlab.org/nlab/revision/diff/call-by-push-value/8">diff</a>, <a href="https://ncatlab.org/nlab/revision/call-by-push-value/8">v8</a>, <a href="https://ncatlab.org/nlab/show/call-by-push-value">current</a>

    The first sentence of this entry started out as:

    Call-by-push-value is a type theory and programming language which contains…

    This does not seem to make (grammatical) sense.(?) I am assuming what is meant is something as follows (emphasis added):

    Call-by-push-value is a type theory and programming language paradigm which subsumes

    I have taking the liberty/chance to edit this accordingly. But if any expert is seeing this, please feel invited to adjust.

    In fact, if such experts are around, it would be a great service if you could create the promised entries

    • call-by-value

    • call-by-name

    which are referred to here and in a rather large number of other entries (see here and here) but which remain missing.

    diff, v8, current