tag:blogger.com,1999:blog-8068466035875589791.post6102951393463925537..comments2024-03-26T00:37:39.585-07:00Comments on Semantic Domain: Polarity and bidirectional typecheckingNeel Krishnaswamihttp://www.blogger.com/profile/06853898957395028131noreply@blogger.comBlogger14125tag:blogger.com,1999:blog-8068466035875589791.post-10038509413298393872019-05-07T04:31:33.099-07:002019-05-07T04:31:33.099-07:00Hi Max, as far as I can tell, it's not a seman...Hi Max, as far as I can tell, it's not a semantic difference. However, in order to make progress on sorting out what bidirectional typechecking actually is, and how it relates to polarization and call-by-push-value, we need to make it into a semantic difference! <br /><br />Eg, it's folklore that for MLL, you can invert the checking and synthesis rules (so lambdas synthesise and applications check). This fact will remain merely a curiosity until we have a semantics for bidirectional typechecking.<br /><br />Luckily, Google tells me that Andreas Abel and Christian Sattler have just released a draft, <a href="https://arxiv.org/abs/1902.06097" rel="nofollow"><em>Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus</em></a>, which seems likely to help!Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-49186061504273531552019-04-30T12:39:48.557-07:002019-04-30T12:39:48.557-07:00Correct me if I'm wrong, but I think the fact ...Correct me if I'm wrong, but I think the fact that CBPV only has positive vars and this polarized type theory has only negative vars is not a semantic difference, but only a difference in how much focussing discipline the two calculi enforce.<br /><br />I.e. it looks like we can translate a judgment x:N |> t <= N' in this polarized calculus to a judgment x:UN |- t : N' in CBPV. We never have positive variables in the fully focussed polarized world because when we have a function type P -> N we cannot simply pop the argument off of the stack into the current environment, we have to immediately deeply pattern match on it, whereas in CBPV we have the rule<br /><br />G, x : P |- M : N<br />-------------------------<br />G |- lambda x. M : P -> N<br /><br />Need to look in more detail to see how this would affect the bidirectional stuff, though.Max S. Newhttps://www.blogger.com/profile/06397739710418207929noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-10919369098392494562019-03-06T06:22:23.115-08:002019-03-06T06:22:23.115-08:00Yes, that's right.Yes, that's right.Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-30064092606422022862019-02-21T12:33:17.676-08:002019-02-21T12:33:17.676-08:00It should be
P,Q ::= ..
instead of
P ::= ..
right?...It should be<br />P,Q ::= ..<br />instead of<br />P ::= ..<br />right?<br /><br />Also excellent post.Markhttps://www.blogger.com/profile/16416011389394197574noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-28921725856130722472018-08-17T05:38:38.589-07:002018-08-17T05:38:38.589-07:00"So a variable pattern at value type simply b..."So a variable pattern at value type simply binds the variable at that type, and when we use a value variable we have the check that the type in the context matches the type that we're checking the term at.<br /><br />"And that's the wrong thing to do! The bidirectional recipe says that we should check equality of types only when we switch between checking and synthesis..."<br /><br />Matt Oliveri: But wait, let me see if I understand.<br /><br />Variables' types are always synthesized, since they're looked up in the context. So you're switching between checking and synthesis in that rule. Are you saying there should've been a separate rule just for the switch, as usual? But isn't that actually the only rule with a direction switch? It lets you avoid eta expanding at positive types. (You can pass along a value without matching against it.)Anonymoushttps://www.blogger.com/profile/10324583900507174355noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-24363913063830728082018-08-16T04:32:45.911-07:002018-08-16T04:32:45.911-07:00I see. I guess even if the rule for positive varia...I see. I guess even if the rule for positive variables does not break relevant metatheorems it would already depart from polarized type systems.<br /><br />By the way, to clarify things to myself, for polarization to be a semantic notion you need semantics that distinguish between computations and values, right?Andrea Vezzosihttps://www.blogger.com/profile/07314943153376710289noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-12574988511937910162018-08-16T01:35:16.367-07:002018-08-16T01:35:16.367-07:00How would the application rule look like then?How would the application rule look like then?Andrea Vezzosihttps://www.blogger.com/profile/07314943153376710289noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-88554602511673591462018-08-15T11:50:48.973-07:002018-08-15T11:50:48.973-07:00What I mean by that word is something which will s...What I mean by that word is something which will stand the test of time, not in the sense of being used permanently, but in the sense of being distinguished as a "nodal point" in the design space, a moment of local harmony between theory and practice.Unknownhttps://www.blogger.com/profile/04807670051420769844noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-30723318568503695392018-08-15T03:41:06.863-07:002018-08-15T03:41:06.863-07:00@Jon: immortal?@Jon: immortal?Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-64445240899998245412018-08-15T02:40:38.591-07:002018-08-15T02:40:38.591-07:00Andrea: Part of the point is that I can't give...Andrea: Part of the point is that I can't give a good explanation! <br /><br />1. Bidirectional typechecking is not a single thing -- it is a set of heuristics about how to design type systems, for which people have varying intuitions. <br />2. There seems to be a close connection between polarization and bidirectional typechecking.<br />3. However, the connection is not tight enough for me to feel confident in saying "bidirectional typechecking is polarization" or anything even remotely close to that. <br />4. For example, in a polarized type theory, you carefully restrict things to only permit negative variables. However, the syntax of call-by-push-value, which has <em>exactly the same type structure as polarization</em>, carefully restricts things so you have only <b>positive</b> variables. <br />5. So the semantics of types isn't enough to tell us what the syntax of the bidirectional inference rules should be. This is annoying, but in retrospect it shouldn't be a huge surprise, since polarization <br />can be seen as either a refinement of Moggi's monadic metalanguage or the exponential of linear logic, and neither of those are canonical (ie, you can have two different, non-isomorphic monads or bangs in your language).<br />6. As a result, we have to try and figure things out from purely proof-theoretic considerations, which is always a harder row to hoe than when you can use both proof theory and semantics to constrain the search space.<br />7. This means that we have to find the "right" set of metatheorems we want to hold for a bidirectional type system to assess candidate type systems.<br />8. We don't have any consensus for that set of metatheorems.<br />9. As a result, bidirectional typechecking is not a single thing -- it is a set of heuristics about how to design type systems, for which people have varying intuitions. <br /><br />As a result, I strongly encourage you to design type systems that I don't like. If you can prove theorems that I do like about them, then perhaps I will change my mind. :)Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-22341186533166977502018-08-14T11:58:42.453-07:002018-08-14T11:58:42.453-07:00Another, possibly Immortal (not sure yet), variant...Another, possibly Immortal (not sure yet), variant of bidirectional typechecking is where at negative types, you NEVER infer. Neutrals of negative type appear only in checking mode...<br /><br />I haven't fully worked out the details of this approach, but it seems to give a more natural account of subtyping which automatically justifies eta expansion and contraction. I'll let you know when I have more.<br /><br />I think what we're seeing is that there's something closely connected to polarity in bidirectional type checking, but we shouldn't be adopt dogmatism about what bidirectional type checking means. In my opinion, it should be *determined* by the logical structure which we observe from proof theoretic concerns, rather than being some immovable thing which we struggle to make fit with other notions. Dogmatism about these things, however useful in the short term, is a funnel into weakness.<br /><br /><br />- Jon SterlingUnknownhttps://www.blogger.com/profile/04807670051420769844noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-82075228792409424502018-08-14T05:10:39.915-07:002018-08-14T05:10:39.915-07:00"The bidirectional recipe says that we should..."The bidirectional recipe says that we should check equality of types only when we switch between checking and synthesis."<br /><br />Can you explain why that should be such a stringent requirement?<br /><br />From your post the purpose of a bidirectional type system is to only type beta-short eta-long normal forms, and I would guess that introducing positive variables does not break that.<br /><br />Another feature of bidirectional typing rules is that they remove choice points in typing rules without needing annotated terms: like the domain type in the application rule. Introducing "u" does not seem to break that either.<br /><br /><br /><br />Andrea Vezzosihttps://www.blogger.com/profile/07314943153376710289noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-31352833298081349182018-08-13T03:37:07.126-07:002018-08-13T03:37:07.126-07:00Thanks, fixed:
"When we apply a term"
...Thanks, fixed: <br /><br />"When we apply a term"<br /><br />--> <br /><br />"When we apply a function, we first *infer* a type $A \to<br />B$ for the function expression, which gives us a type $A$ to *check* the argument against."Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-84015846111551900252018-08-12T07:05:28.792-07:002018-08-12T07:05:28.792-07:00This seems like a cut-off sentence (or paragraph):...This seems like a cut-off sentence (or paragraph): "When we apply a term"glaebhoerlhttps://www.blogger.com/profile/16820759981849420314noreply@blogger.com