{"comment":{"url":"https://api.github.com/repos/vikraman/2DTypes/comments/20224386","html_url":"https://github.com/vikraman/2DTypes/commit/38d474fd55ad70c6bf63005cee236a40aab44dd5#commitcomment-20224386","id":20224386,"user":{"login":"sabry","id":2972393,"avatar_url":"https://avatars.githubusercontent.com/u/2972393?v=3","gravatar_id":"","url":"https://api.github.com/users/sabry","html_url":"https://github.com/sabry","followers_url":"https://api.github.com/users/sabry/followers","following_url":"https://api.github.com/users/sabry/following{/other_user}","gists_url":"https://api.github.com/users/sabry/gists{/gist_id}","starred_url":"https://api.github.com/users/sabry/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/sabry/subscriptions","organizations_url":"https://api.github.com/users/sabry/orgs","repos_url":"https://api.github.com/users/sabry/repos","events_url":"https://api.github.com/users/sabry/events{/privacy}","received_events_url":"https://api.github.com/users/sabry/received_events","type":"User","site_admin":false},"position":null,"line":null,"path":null,"commit_id":"38d474fd55ad70c6bf63005cee236a40aab44dd5","created_at":"2016-12-17T19:15:01Z","updated_at":"2016-12-17T19:15:01Z","body":"As I am writing the end of Sec 3 and the beginning of Sec 4, I failed to convince myself that we need to do any synchronization. Specifically the naive operational semantics for zig-zag that we’ve had for years can map c^1 to c^k where k is the index that is internalized in eta. \n\nI’ve always assumed this is “bad”. But really why is it bad ??\n\nRead end of sec 3 and sec 4 and try to explain this please. \n\n—Amr\n\n\n> On Dec 16, 2016, at 6:25 PM, Sabry, Amr A. <sabry@indiana.edu> wrote:\n> \n> I am thinking of it as a small change in the sense that we already wanted to use dependent types to keep track of the synchronization of c^k and 1/c^k.  If you try to write down what it means you will probably write something like the definition in Sec. 5 (with the Sigma) and then the obvious way to explain it is to say that we have pointed types. \n> \n> The definition in Sec. 4 if we try using it directly in the operational semantics will require a side-condition, a runtime check, or some backtracking. I think the dependent type solution is much better. \n> \n> —Amr\n> \n> \n>> On Dec 16, 2016, at 6:21 PM, Jacques Carette <notifications@github.com <mailto:notifications@github.com>> wrote:\n>> \n>> This is a HUGE change! What is the (deep) reason for it?\n>> \n>> —\n>> You are receiving this because you authored the thread.\n>> Reply to this email directly, view it on GitHub <https://github.com/vikraman/2DTypes/commit/38d474fd55ad70c6bf63005cee236a40aab44dd5#commitcomment-20221204>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AC1a6evogeheRTpvkPg7Y8-Bv72epZG6ks5rIx0DgaJpZM4LPr55>.\n>> \n> \n\n"}}
{"actor":{"display_login":"sabry"}}