Timeline for What is a brief but complete explanation of a pure/dependent type system?
Current License: CC BY-SA 3.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 1, 2016 at 9:18 | comment | added | pigworker | @cody Yes, there is no expansion. To see why it's not necessary, note that the two computation rules allow you to deploy the strategy where you normalize types completely before you check terms, and you also normalize types immediately after synthesizing them from eliminations. So in the rule where the types must match, they are already normalized, hence equal on the nose if the "original" checked and synthesized types were convertible. Meanwhile, restricting equality checks to that place only is ok because of this fact: if T is convertible to a canonical type, it reduces to a canonical type. | |
| Aug 29, 2016 at 17:49 | comment | added | cody | I'm confused: You don't have type expansion (vs reduction)? Is it easy to prove you don't need it? There was an open question about this at some point... | |
| Nov 23, 2015 at 19:04 | history | migrated | from stackoverflow.com (revisions) | ||
| Nov 11, 2015 at 22:29 | vote | accept | MaiaVictor | ||
| Sep 28, 2018 at 18:11 | |||||
| Nov 11, 2015 at 22:27 | comment | added | MaiaVictor | I just wanted you and the other answerers to know that I'm coming back to this thread every break from work. I really want to learn this, and for the first ime I fell like I actually get most of it. The next step will be implementing and writing a few programs. I'm delighted to be able to live in an era where information about such wonderful topics are available across the globe to someone like me, and that is all thanks to geniuses like you who dedicate some time of their life to spread that knowledge, for free, on the internet. Sorry again for phrasing my question badly, and thank you! | |
| Nov 11, 2015 at 10:22 | comment | added | pigworker | My system also allows terms to shadow at their own risk: the invariant is enforced only on contexts. | |
| Nov 11, 2015 at 10:15 | comment | added | effectfully | Ah, I missed the invariant part. Also, Agda accepts hm : (A : Set) -> (A : A) -> _; hm _ A = A (but she converts to de Bruijn indices). | |
| Nov 11, 2015 at 10:09 | comment | added | pigworker | Oh, I thought you were just pointing out the typo. The rule says that, for each variable in the context, we synthesize the type that the context assigns it. When introducing contexts, I said "We maintain the invariant that the variables ascribed types in the context are distinct." so shadowing is disallowed. You'll see that every time the rules extend the context, they always choose of a fresh "z" which instantiates whatever binders we're stepping under. Shadowing is anathema. If you have context x : *, x : x then the type of the more local x is no longer ok because it's the x out of scope. | |
| Nov 11, 2015 at 10:01 | comment | added | effectfully | @pigworker, could you explain why nope? Since you handle weakening explicitly I thought it worth to explicitly handle shadowing in this rule. Or am I misunderstanding something? | |
| Nov 11, 2015 at 9:47 | comment | added | pigworker | @user3237465 Nope. Thanks! Fixed. (When I was replacing ascii art turnstiles with html turnstiles (thus making them invisible on my phone; sorry if that's happening elsewhere) I missed that one.) | |
| Nov 11, 2015 at 9:30 | comment | added | effectfully | G, x:S, G' ⊢ x is S -: G' ⊬ x? | |
| Nov 11, 2015 at 0:12 | history | answered | pigworker | CC BY-SA 3.0 |