tag:blogger.com,1999:blog-7486674684844560197.post6123604858738600733..comments2013-02-22T06:53:13.919-08:00Comments on The Paralyzing Paradoxes of Professor Polaro: What is the logic of ML values?Noamhttp://www.blogger.com/profile/09175792123472366590noreply@blogger.comBlogger5125tag:blogger.com,1999:blog-7486674684844560197.post-55522872953244488692009-11-22T07:03:49.377-08:002009-11-22T07:03:49.377-08:00Neel, all I can say is that yes, that seems like a...Neel, all I can say is that yes, that seems like a very important point, and I've been thinking about it...Noamhttps://www.blogger.com/profile/09175792123472366590noreply@blogger.comtag:blogger.com,1999:blog-7486674684844560197.post-19985863566564225882009-11-19T05:25:16.128-08:002009-11-19T05:25:16.128-08:00Hi Noam,
Your translation of functions reminds m...Hi Noam, <br /><br />Your translation of functions reminds me of something about System F I have always found curious: any type A is isomorphic to forall α. (A -> α) -> α. <br /><br />To go backwards, you can just instantiate α with A, and then pass the identity function. Because of this impredicativity, the isomorphism is stable under basically any type constructors you feel like adding to the language. <br /><br />So the sense in which you are holding β abstract has to be subtly different from type abstraction in the System F sense. It's not "you must be parametric over any choice of result", but rather "there is a globally unique choice of result which you must not look at".<br /><br />Speculating wildly, I wonder if this might suggest some way to find some constructive content in Hilbert's choice operator....Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-7486674684844560197.post-48116868472204538122009-11-17T02:40:48.515-08:002009-11-17T02:40:48.515-08:00(It looks like I second-guessed the terminology &q...(It looks like I second-guessed the terminology "values*" there, probably for the best...)<br /><br />And non-termination is of course important too. I think a good way to model ML is to say that we are allowed to introduce cycles when building "proofs" of β. (In call-by-push-value, we can use recursion when defining computations. In polarized type theory, we can use recursion to define values of negative type.)Noamhttps://www.blogger.com/profile/09175792123472366590noreply@blogger.comtag:blogger.com,1999:blog-7486674684844560197.post-85429656076590906492009-11-17T02:25:23.554-08:002009-11-17T02:25:23.554-08:00Hello Andrej. So if we ignore the second point, a...Hello Andrej. So if we ignore the second point, and just view "values" as "valuable expressions" (let's call them values*), then we can literally interpret values of type τ as identical to intuitionistic proofs of τ* (in a context of effects), where τ* is defined as:<br /><br />(σ × τ)* = σ* ∧ τ*<br />(σ + τ)* = σ* ∨ τ*<br />(σ → τ)* = σ → (τ → β) -> β<br /><br />(This translation is sound for proper values as well.)<br /><br />Expressions of type τ, on the other hand, we interpret as proofs of β, abstract in a continuation of type τ* → β.<br /><br />So the difference between "the logic of values" and "the logic of expressions" is a single double-negation.<br /><br />The rest is an exercise in CPS. For example, the left-to-right pairing construct on expressions takes k:σ*→β.E₁ and k:τ*→β.E₂ and builds k:(σ*∧τ*)→β.E₁[k := λx.E₂[k := λy.k(x,y)]]. We can similarly describe application of one expression to another, with left-to-right evaluation. But we can also describe application of one value to another, building an expression. Intuitionistically, given v₁:σ* and v₂:σ*→(τ*→β)→β, we can form k:τ*→β.v₂ v₁ k.<br /><br />We can also derive some composition principles that just involve values. For example, given v₁:σ* and v₂:τ* we can form (v₁,v₂):σ*∧τ*. Given v₁:σ* and x:σ*.v₂:τ* (a value abstract in a value variable), we can substitute v₂[x := v₁] and the result is still a value.<br /><br />(We might consider *internalizing* this substitution principle as another type constructor, representing a pure function space on values. This is something we don't have in ML, and I don't understand very well. But Alex Simpson has looked at this recently...see his <a href="http://homepages.inf.ed.ac.uk/als/Talks/popl09.pdf" rel="nofollow">POPL09</a> talk.)Noamhttps://www.blogger.com/profile/09175792123472366590noreply@blogger.comtag:blogger.com,1999:blog-7486674684844560197.post-53384159068922882002009-11-17T00:20:39.507-08:002009-11-17T00:20:39.507-08:00If you consider ML values as proof terms for some ...If you consider ML values as proof terms for some unknown logic, then it looks like you will get a restricted form of implication elimination (modus ponens), since an application need not result in a value, as you observe. Have you or someone else thought about what this form is?Andrej Bauerhttps://www.blogger.com/profile/17920316604280193336noreply@blogger.com