{"action":"created","issue":{"url":"https://api.github.com/repos/jonsterling/tt/issues/9","repository_url":"https://api.github.com/repos/jonsterling/tt","labels_url":"https://api.github.com/repos/jonsterling/tt/issues/9/labels{/name}","comments_url":"https://api.github.com/repos/jonsterling/tt/issues/9/comments","events_url":"https://api.github.com/repos/jonsterling/tt/issues/9/events","html_url":"https://github.com/jonsterling/tt/issues/9","id":296134259,"number":9,"title":"Elaboration","user":{"login":"jonsterling","id":55057,"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":15,"created_at":"2018-02-10T21:11:35Z","updated_at":"2018-02-19T21:38:40Z","closed_at":null,"author_association":"OWNER","body":"We'll need an elaborator, and I want it to have support from early on for both holes and some kind of implicit arguments to functions. The reason for this is, this is the sort of thing that distinguishes and toy language from a proof assistant, and I think if we don't carry it out, we never will.\r\n\r\nThis opens up a whole can of worms, and I'm not sure what the least gnarly way to implement it is.\r\n\r\nOne decision choice I would kind of like to make, if possible, is to not expose any of this in the core language; that is, I would like to avoid core terms for `Pi` and `App` keeping track of whether something was implicit or not, etc. It seems like we should be able to isolate this in the source language and the elaboration process. But I'm not certain.\r\n\r\nIt may even be reasonable to restrict implicit arguments to top-level declarations, and distinguish between \"type schemes\" and actual types. I think this is how it was done in Epigram. Not sure what's best."},"comment":{"url":"https://api.github.com/repos/jonsterling/tt/issues/comments/366808779","html_url":"https://github.com/jonsterling/tt/issues/9#issuecomment-366808779","issue_url":"https://api.github.com/repos/jonsterling/tt/issues/9","id":366808779,"user":{"login":"jonsterling","id":55057,"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},"created_at":"2018-02-19T21:38:40Z","updated_at":"2018-02-19T21:38:40Z","author_association":"OWNER","body":"@freebroccolo Let me give a little bit more explanation about some questions I'm having...\r\n\r\nSuppose we start with a proof state like `X : (G !- ? <= A->A); Psi`; this should be read as letting the meta `X` stand for an unknown element of type `A->A` in context `G`, where the *remainder* of the proof state is `Psi`. Things in `Psi` can mention `X`.\r\n\r\nNow, we can refine the goal `X` using the function introduction rule. The, we would have something like the following: `Y : (G.A !- ? <= A); X : (G !- lam(@Y) <= A -> A); Psi`. Now, at this point what our elaboration algorithm does is kind of up for grabs. There's a couple options:\r\n\r\n1. One option would be to immediately get rid of `X` and just substitute `lam(@Y)` for `X` in the rest of the proof state. This is the approach taken in RedPRL/Dependent LCF; in fact the representation of proof states there forces the substitution to take place right away. At least in RedPRL this is extremely expensive, because if you refine a goal early in a very wide proof state, this can result in dozens of substitutions needing to occur at every elaboration step. This basically ruins performance in RedPRL, but I want to note that we don't have any memoization in RedPRL so it's hard for me to compare.\r\n\r\n2. Another option would be to leave `X` as it is! When we need to learn something about X (for instance, if we try to evaluate the term `app(@X; N)`, we just look it up in the environment.\r\n\r\n3. Maybe something in between, or completely different?\r\n\r\nAnyway, this is one of the main design questions that's been bugging me. Do you have any insight into what you think would be the right way to think about this stuff?\r\n\r\n"}}
{"actor":{"display_login":"jonsterling"}}