{"action":"created","issue":{"url":"https://api.github.com/repos/RedPRL/redtt/issues/231","repository_url":"https://api.github.com/repos/RedPRL/redtt","labels_url":"https://api.github.com/repos/RedPRL/redtt/issues/231/labels{/name}","comments_url":"https://api.github.com/repos/RedPRL/redtt/issues/231/comments","events_url":"https://api.github.com/repos/RedPRL/redtt/issues/231/events","html_url":"https://github.com/RedPRL/redtt/issues/231","id":350460583,"node_id":"MDU6SXNzdWUzNTA0NjA1ODM=","number":231,"title":"Find a way to limit the pain of restriction pretypes (or remove them)","user":{"login":"jonsterling","id":55057,"node_id":"MDQ6VXNlcjU1MDU3","avatar_url":"https://avatars2.githubusercontent.com/u/55057?v=4","gravatar_id":"","url":"https://api.github.com/users/jonsterling","html_url":"https://github.com/jonsterling","followers_url":"https://api.github.com/users/jonsterling/followers","following_url":"https://api.github.com/users/jonsterling/following{/other_user}","gists_url":"https://api.github.com/users/jonsterling/gists{/gist_id}","starred_url":"https://api.github.com/users/jonsterling/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonsterling/subscriptions","organizations_url":"https://api.github.com/users/jonsterling/orgs","repos_url":"https://api.github.com/users/jonsterling/repos","events_url":"https://api.github.com/users/jonsterling/events{/privacy}","received_events_url":"https://api.github.com/users/jonsterling/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2018-08-14T14:43:52Z","updated_at":"2018-08-14T16:35:19Z","closed_at":null,"author_association":"COLLABORATOR","body":"The restriction pretypes are brutal, and a lot of things are broken because of them. I would like to find a way to remove them, or at least limit their influence. Let me start by recalling why they exist in the first place: we need to be able to have a goal with a restriction, and then skolemize that goal as some kind of type (or other structure) that can be made into a hole in the global context.\r\n\r\nUnfortunately they make the implementation very complicated, and in practice really unreliable and confusing. In most places, we are either too clever wrt restrictions or not clever enough.\r\n\r\nI would like to remove them and instead make restrictions part of the *judgments*. Stratifying things in this way would clarify a LOT. I don't yet see how to remove the restriction pretypes entirely without making holes impossible (there is probably a way), but to start, I think we could try and implement this judgmental structure.\r\n\r\n/cc @ecavallo "},"comment":{"url":"https://api.github.com/repos/RedPRL/redtt/issues/comments/412935480","html_url":"https://github.com/RedPRL/redtt/issues/231#issuecomment-412935480","issue_url":"https://api.github.com/repos/RedPRL/redtt/issues/231","id":412935480,"node_id":"MDEyOklzc3VlQ29tbWVudDQxMjkzNTQ4MA==","user":{"login":"favonia","id":1471328,"node_id":"MDQ6VXNlcjE0NzEzMjg=","avatar_url":"https://avatars1.githubusercontent.com/u/1471328?v=4","gravatar_id":"","url":"https://api.github.com/users/favonia","html_url":"https://github.com/favonia","followers_url":"https://api.github.com/users/favonia/followers","following_url":"https://api.github.com/users/favonia/following{/other_user}","gists_url":"https://api.github.com/users/favonia/gists{/gist_id}","starred_url":"https://api.github.com/users/favonia/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/favonia/subscriptions","organizations_url":"https://api.github.com/users/favonia/orgs","repos_url":"https://api.github.com/users/favonia/repos","events_url":"https://api.github.com/users/favonia/events{/privacy}","received_events_url":"https://api.github.com/users/favonia/received_events","type":"User","site_admin":false},"created_at":"2018-08-14T16:35:19Z","updated_at":"2018-08-14T16:35:19Z","author_association":"COLLABORATOR","body":"Yes, please."}}
{"actor":{"display_login":"favonia"}}