Prose Fine-tuning Todos #141
Description
Prioritisation
(P1) Correctness (highest priority)
(P2) Functionality
(P3) Comprehensibility
(P4) Appearance (lowest priority)
Validation
General issues
-
The biggest omission is that we are still missing most hyperlinks in the prose:
- (P2) for syntax (“number type”, “defined type”, etc.)
- (P2) for relations (“valid”, “matches”, etc.)
-
(P3) Validity judgements are all rendered in prose as “… is valid with …”. But in some cases, “with” isn’t the right preposition, because the rhs is not a type. We may need some (hint?) mechanism to customise this. For example:
- Rectype_ok: “valid with ok(x)” to “valid for type index x”
- Limits_ok: “valid within range k”
- Blocktype_ok: “valid as …”
- Data_ok: “valid”
-
(P3) When unrolling mappings that implicitly introduce repeated variables, their origin and dependency order isn't really reflected, such that they appear to be coming out of nowhere. For example, with lt* in Func_ok we have steps:
- The length of lt* is equal to the length of local*.
- For all lt in lt*, and corresponding local in local*:
- The local local is valid with the local type lt.
What we'd ideally want here is something like
- For each local in local*:
- The local local is valid with some local type lt.
- Let lt* be the concatenation of all lt.
The current rendering becomes less readable in more complex rules, e.g., consider x* and x'** in Rectype_ok.
General rendering nits
-
(P3) Can we always use long names for antiunification variables? E.g., “storagetype” instead of “zt” etc.
-
Can we eliminate antiunification indices where possible, and drop the “u” elsewhere? For example,
- (P4) Valtype_ok: plain “t” instead of “t_{u1}”
- (P4) Heaptype_sub: “ht_1” and “ht_2” instead of “ht_{u1}” and “ht_{u2}”
-
(P3) In places where a rule case is identified by a step like “ is equal to ”, can we instead say “… is of the form ”? That makes it clearer that this is case matching, and it is more fitting when the rhs is just a variable, or contains variables that are bound by the statement. (For example, see Valtype_sub, Comptype_sub.)
-
(P4) Can we render “|x*|” as prose “the length of x*”?
-
(P3) If there are multiple iteration variables, can we say “For every in <x*> and corresponding in <y*>” to clarify that this is pairwise, not combinatorial?
-
(P3) When a typing rule has no premise, can we insert a clarifying word? For example, instead of “The number type numtype is valid” produce “The number type numtype is unconditionally valid”.
-
(P3) Similarly, for a matching rule that is just reflexivity, can we say “… matches only itself”?
-
(P4) Types (ref ht) are always rendered as (ref eps t); the epsilon is redundant and not shown in other places.
Specific rules
-
Reftype_ok:
- (P0) "The null? null? is absent" — I assume this is due to the show hints. What we'd want here is "The attribute null? is absent".
-
Instrtype_ok:
- (P1) spurious appearance of lct* ?
- (P3) lt* is used before defined
-
Rectype_ok:
- (P2) This includes the rule Rectype_ok/rec2, which is only relevant for proving soundness and should not appear in this section. Is there some way to suppress rendering that rule?
- (P2) Missing parens for “ok(x)” and “ok(x + 1)” (also in Type_ok)
- (P4) Can we specialise “is equal to ε” to “is empty”?
- (P2) "okx"/"okx+1 should be "ok(x)"/"ok(x+1)"
- (P3) x* and x'* are constrained before they are introduced, see above
- (P4) Can we rename
subtype'tosubtype?
-
Subtype_ok:
- (P3) In various places, the “*” are typeset incorrectly.
- (P3) Some occurrences of comptype' are not hyperlinked.
-
Limits_ok:
- (P4) There is odd extra space inside the brackets (similarly in other places).
- (P4) It says “the limits … is”, while English grammar would require plural here (“the limits … are”). I assume that would be highly non-trivial to handle. Perhaps we could say “limits range” so that it works with singular?
-
Heaptype_sub:
- (P3) For case Heaptype_sub/rec, the range check for j appears after j is used.
- (P4) Odd choice of meta variables heaptype'' and heaptype'''.
-
Resulttype_sub:
- (P3) It should say “the result type” instead of “value type sequence” (similarly in Instrtype_sub and Functype_sub).
- (P3) The “*” is typeset on the subscript in some cases.
-
(**P2**) Externtype_sub: In case /tag, the “tagtype” variables aren’t hyperlinked. #149
-
(P3) Instr_ok/ref.func: “The index C.refs[0] exists.” That is an odd condition, where is it coming from?
-
(P3) Instr_ok/{struct,array}.{new[_fixed],get,set}, array.fill, sh.{splat,extract_lane,replace_lane}, {table,memory}.copy: The last statement is a Let, which reads very odd, especially since t was already used in the header. Would it be possible to specialise this to “The value type t is …”?
-
(P2) Instr_ok/{struct,array}.new_default: “A default value for value type the value type unpack(zt) is defined.”
-
(P2) Instr_ok/br_on_cast[_fail]: The type difference rt1 \ rt2 should be rendered in prose, or at least have a hyperlink to the definition of the \ operator.
-
(P3) Instrs_ok: Can we render context updates as prose? Something like “C with the local types of x* updated to (set t*)”. Can prose render hints on the definition of $with_locals do that?
-
(P4) {Instr,Expr}_const: Can we render “const” as “constant” in prose?
-
Func_ok:
- (P1) Spurious appearance of a lct* ?
- (P4) "The expanion ... is the composite type" – wouldn't "is some composite type" be more appropriate?
- (P3) Can we render the complex context extension in prose?
-
(P1) Tag_ok: “The tag type 𝐶.types[𝑥] exists.” This isn’t adequate, since C.types[x] isn’t necessarily a tag type. It needs to say “defined type” there, and in the next line.
-
Module_ok:
-
(P3) Do not use “t” for the module type, since that meta variable is reserved for value types. Use “moduletype” instead.
-
(P3) We need to turn all the context constructions into prose — they're too long and too complex.
-
(P3) The way the type sequences are introduced is rather unintuitive. For example, it says
- |mt*| is equal to |mem*|.
- For all mem in mem* and mt in mt*:
– Under the context 𝐶′, the memory mem is valid with the memory type mt.
In reality, the mt are an output of the loop. I’m not sure how difficult it would be to somehow detect and tweak this.
-
The import type sequences dt_i*, ft_i*, etc are defined only after they are used.
-
Unfortunate but probably difficult to improve(?)
-
Heaptype_sub:
- In case /refl, one would rather want to say that both types are equal.
- In case /trans, the introduction of heaptype_1/2 becomes redundant.
-
Instrtype_sub: The header “For all t in t* and x in x*” should really just be “For all x in x*”, since the t* don’t matter and are throwaways local to the loop.
-
Instr_ok/{struct,array}.get: “zt is equal to unpack(zt)” would be more intuitively rendered as “zt is a packed type”
-
Instrs_ok/sub: The type it’ is redundant.
Execution
Long-standing todos in document
-
(P3) Todos about (5) generating “the expansion of”
-
(P?) Todos about (7) rendering inverse
-
(**P1**) Todo about the inability to render the rule for return_call_ref & handler due to deep nesting. #146
This ultimately is just a consequence of the problem that the AL does not distinguish conditions from assertions accurately, especially about syntactic cases, but sometimes also side conditions. For example, in the rule for struct.get, Step 5 should not be a condition but an assertion. Likewise, the condition 5.b.4 is really an assertion. This leads to other problems as well, like the fall-through in the interpreter. As we discussed before, the translation should generally assume that the last case in a branch cannot fail due to soundness.
Other general issues
-
${rule-prose: Num_type}⇒ splicing error: unknown prose relation identifier
Num_type -
(P2) Splicing for Eval_expr does not work, same problem.
General wording nits
-
(P4) “is of the case” — That sounds like somewhat odd English, would simply saying “is” work?
-
-
For one, it uses the word “context” in a sense that isn’t defined in the spec, which uses it for other things. For example:
Let (frame { f }) be the current frame context.
I recently extended the spec document to introduce the generic term “control frames” for call frames, label frames, and handler frames, which we could use here.
-
(P3) Also, these things conceptually live on the stack. Instead of “current”, it hence is more accurate to say “topmost X on the stack”.
-
(P3) If at all possible, the wording should avoid spelling out the syntax of these control frames, since it is not a good match with the mental model of the prose — in particular, labels are just pointers to code in that model, so it is weird to include code in them, which is more an artefact of the reduction semantics. That’s why the manual prose always only calls them L abstractly and describes what they're pointing to in prose. However, I’m not sure if there is an easy way to auto-generate that.
At least for call frames, can the above be simplified to just saying “Let f be the current call frame.”?
-
-
(P3) “Let 𝑡* → resulttype be functype” — As mentioned before, it would be good if we could make the pattern match nature of this binding apparent by phrasing it something like “Let 𝑡* → resulttype be the destructuring of functype” when the l.h.s. isn’t a plain variable.
-
(P3) Conversely, in let bindings that do have a variable on the left, can we somehow include (and link) the type of object produced? That is not always super-obvious. For example, for struct.new, step 8, “let si be the structure instance { … }”?
-
(P1) In various places the prose says “Due to validation, an instruction is on the top of the stack.” — But instructions are not on the stack. It has to be “value”. Accordingly, the meta variable val not instr should be used in the consecutive steps.
-
(P3) As for validation, can the concatenation operator big-⨁︀ be translated to prose?
-
(P4) As for validation, can the naming of unification variables be improved?
-
(P3) As for validation, can we render extension expressions like “Perform 𝑧[.structs =⊕ si]” to less cryptic prose? Something “Append si to z.structs”?
Specific rules
-
(P4) Ref_ok/exn: the second premise is redundant, since exn is not used.
-
(P1) Externaddr_ok: In all rules the prose says "Under the context s...", but s is not a context but a store. (And it does not differ between premise and conclusion, so there is no need to mention it at all.)
-
(P3) drop: todo to remove trailing “do nothing”
-
(P3) unop: “If |unop_nt (c1)| ≤ 0” — the ≤ is odd here, since the cardinality is a natural number. In the written rule, this simply says “unop_nt (c1) = ε”, why is that converted to the more indirect condition? (The same occurs in other rules for numeric or vector ops.)
-
(P3) ref.eq: This becomes quite blown up. Why is the conjunction in the side condition split into multiple branches?
-
ref.test, ref.cast:
- (P1) The check for “if ref is not valid” shouldn’t be there, since refs are always valid. That is, this trap can never happen.
- (P2) Todo regarding ref_type_of
-
(P2) array.new_data: The assertion in Step 10 lost me a little. Where is fresh_i coming from?
-
(P1) extern.convert_any: “If the type of instr_u1 is address value, then...” — I think I understand what this is saying, but “address value” is not a type in the sense of the spec. This ought to say something like “If instr_u1 is an address value”. (And shouldn’t use instr, see above.)
-
(P1) sh.extract_lane: similar issue with “is number type” and “is packed type”.
-
nt.load:
- (P1) “If the type of ntu1 is Inn” — same problem; also, Inn is not typeset.
- (P3) “loadop_o” (with a literal underscore)
- (P2) “is of the case _” (with a literal underscore)
- (P3) the variable nt is redundant — could this be avoided by more clever naming of unification variables? For example, if all cases are a CaseE, but only one is VarE, then use the name of that VarE.
-
block/loop, etc: “Enter val^𝑚 instr* with label (label𝑛{ (loop bt instr*) }).”
- (P3) The label needs to be represented differently and should not contain code in the prose representation, since it is interpreted as just a jump target. The manual spec instead says something like "Let 𝐿 be the label whose arity is 𝑛 and whose continuation is the start of the loop.”
- (P3) Can it say “Enter the block …” for clarity?
-
br:
- (P1) See issues with “label context” above.
- (P3) The condition “If l > 0” in Step 1.c.2 shouldn’t be there, since we are already in the case where l <> 0, so that is vacuously true (l is a natural number).
-
(P1) growmem/growtable: The partiality of these functions isn’t reflected in the prose. In particular, they need an explicit “fail” step.
-
(P1) Module allocation: Todo about prose not working due to unexpected error (which was about indentation).
- (P3) All iterations should be expanded to prose loops.
-
Module instantiation:
- (P3) Step 3, 9, 12, 13, 15, 17: confusing redundant assertions, since there is only 1 case for each
- (P3) Step 6: the iteration over the tuple should use a prose formulation with “and” like in other places
- (P3) Step 7, 8, 11, 25, 28: The iterations are not converted into prose
-
(P1) evalglobal: Step 2, 4: These assertions are unrelated to validation, but hold due to Step 1
-
- (P3) Step 1: Redundant assertion again
- (P4) Step 4: don’t list empty fields
- (P1) Steps 12, 14, 15: The step 12 is incorrect, since val* is no longer on the stack at that point. Instead, this step needs to pop val^k (which should probably be renamed to val’^k), and steps 14 and 15 need to be removed.