Skip to main content
Computer Science

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

9
  • 1
    $\begingroup$ G, x:S, G' ⊢ x is S -: G' ⊬ x? $\endgroup$ Commented Nov 11, 2015 at 9:30
  • 1
    $\begingroup$ @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.) $\endgroup$ Commented Nov 11, 2015 at 9:47
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Nov 11, 2015 at 10:09
  • 1
    $\begingroup$ 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! $\endgroup$ Commented Nov 11, 2015 at 22:27
  • 1
    $\begingroup$ @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. $\endgroup$ Commented Sep 1, 2016 at 9:18