{"action":"created","issue":{"url":"https://api.github.com/repos/siddhartha-gadgil/ProvingGround/issues/85","labels_url":"https://api.github.com/repos/siddhartha-gadgil/ProvingGround/issues/85/labels{/name}","comments_url":"https://api.github.com/repos/siddhartha-gadgil/ProvingGround/issues/85/comments","events_url":"https://api.github.com/repos/siddhartha-gadgil/ProvingGround/issues/85/events","html_url":"https://github.com/siddhartha-gadgil/ProvingGround/issues/85","id":130256835,"number":85,"title":"Refine Scala types to apply Modus Ponens etc","user":{"login":"siddhartha-gadgil","id":3583396,"avatar_url":"https://avatars.githubusercontent.com/u/3583396?v=3","gravatar_id":"","url":"https://api.github.com/users/siddhartha-gadgil","html_url":"https://github.com/siddhartha-gadgil","followers_url":"https://api.github.com/users/siddhartha-gadgil/followers","following_url":"https://api.github.com/users/siddhartha-gadgil/following{/other_user}","gists_url":"https://api.github.com/users/siddhartha-gadgil/gists{/gist_id}","starred_url":"https://api.github.com/users/siddhartha-gadgil/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/siddhartha-gadgil/subscriptions","organizations_url":"https://api.github.com/users/siddhartha-gadgil/orgs","repos_url":"https://api.github.com/users/siddhartha-gadgil/repos","events_url":"https://api.github.com/users/siddhartha-gadgil/events{/privacy}","received_events_url":"https://api.github.com/users/siddhartha-gadgil/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/siddhartha-gadgil/ProvingGround/labels/active","name":"active","color":"009800"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2016-02-01T05:05:11Z","updated_at":"2016-02-01T05:19:22Z","closed_at":null,"body":"* If we apply Modus Ponens to a refined type, say NatTyp, we end up with the correct expression, but with the _wrong_ scala type, namely with the wrong type parameters for Func\r\n* This is inevitable as we want Lambda's, Func's and FuncTyp's with given parameters to be invariant under substitution, so the refinements of types is lost.\r\n* We need to rectify this a posteriori."},"comment":{"url":"https://api.github.com/repos/siddhartha-gadgil/ProvingGround/issues/comments/177769647","html_url":"https://github.com/siddhartha-gadgil/ProvingGround/issues/85#issuecomment-177769647","issue_url":"https://api.github.com/repos/siddhartha-gadgil/ProvingGround/issues/85","id":177769647,"user":{"login":"siddhartha-gadgil","id":3583396,"avatar_url":"https://avatars.githubusercontent.com/u/3583396?v=3","gravatar_id":"","url":"https://api.github.com/users/siddhartha-gadgil","html_url":"https://github.com/siddhartha-gadgil","followers_url":"https://api.github.com/users/siddhartha-gadgil/followers","following_url":"https://api.github.com/users/siddhartha-gadgil/following{/other_user}","gists_url":"https://api.github.com/users/siddhartha-gadgil/gists{/gist_id}","starred_url":"https://api.github.com/users/siddhartha-gadgil/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/siddhartha-gadgil/subscriptions","organizations_url":"https://api.github.com/users/siddhartha-gadgil/orgs","repos_url":"https://api.github.com/users/siddhartha-gadgil/repos","events_url":"https://api.github.com/users/siddhartha-gadgil/events{/privacy}","received_events_url":"https://api.github.com/users/siddhartha-gadgil/received_events","type":"User","site_admin":false},"created_at":"2016-02-01T05:19:22Z","updated_at":"2016-02-01T05:19:22Z","body":"Note that we cannot simply use typ.Obj for function types, but need to separately refine the domain and codomain."}}