[spec] Address comments by Luke #752
Conversation
document/core/valid/conventions.rst
Outdated
| Likewise, the |CRETURN| field may be omitted when it is |NORETURN|. | ||
|
|
||
| * :math:`C,\K{field}\,A^\ast` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence. | ||
| * The notation :math:`\K{field}\,A^\ast, C` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence. |
There was a problem hiding this comment.
Do you have a rendered link I could see? Naively, it looks like it would read labels A, C which is different (and more confusing, imho) than the C.A labels or A C.labels I was expecting. Actually, what about parens: C.(A labels)? You could maybe even hyperlink the ".(" and ") to this particular rule...
There was a problem hiding this comment.
This is the main repo, but since all the changes are editorial I took the liberty to upload it to the main GH.io.
I agree that this isn't ideal either, and after a couple of days I like it less. :) But I am somewhat reluctant to introduce extra indexing notation for one single use case. I'm almost tempted to stay with the original version, and just trying to make the note clearer. WDYT?
There was a problem hiding this comment.
Yeah, looking at the rendered version is, imho, just as confusing as before. The problem with improving the note is that the use sites are still hard to read. I still think both C.(A* labels) and C.labels⟬l⟭ (with hyperlink to the explanation in conventions) would be a lot more readable. As another idea: could we do something with with (which already seems to be in the overall conventions for field update)?
There was a problem hiding this comment.
Okay, I reverted the inverse context extension notation.
Hm, dot notation expresses projection, while extension is a form of injection, i.e., the opposite, so "C.(A* labels)" would be backwards. In general, I think it's preferable to stick as close to standard notation as possible, so that readers with prior exposure to type systems can understand it as is and aren't confused for no reason -- ultimately there is nothing magic going on here, it's just standard de Bruijn indexing.
I would be surprised if introducing multiple different lookup notations would help clarity for most readers. Conceptually, I also think that lookup is the wrong place to tweak: there is nothing noteworthy about the lookup of labels, the crux is in how the index space is organised, i.e., how the bindings are introduced.
Maybe it was the note that was just more confusing than necessary? I gave another shot at trying to make it clearer. I also added extra notes at the extension and lookup sites. Let me know what you think.
There was a problem hiding this comment.
Fair enough and good notes; lgtm!
|
Thanks! |
2 participants
Addresses @lukewagner's comments on #725, #726, and #727, plus his suggestion for back-porting a minor refactoring of the elements grammar (analogously applied to data segments).