1549 2005-07-11 22:40:46 +0000 [FS] editorial: 3.2.3 Static typing judgment 2007-01-16 17:24:14 +0000 1 1 1 Unclassified XPath / XQuery / XSLT Formal Semantics 1.0 Last Call drafts All All CLOSED FIXED P2 minor --- 1 jmdyck simeon public-qt-comments oldest_to_newest 4508 0 jmdyck 2005-07-11 22:40:46 +0000 3.2.3 Static typing judgment "the input literals '3' and '5' have type integer," Delete "input"? "so the variable $v also has type integer." You don't need to know that 5 has type integer to infer $v's type. "statEnv |- if Expr1 then ..." Add parentheses around Expr1 "The "left half" (the part before the :) of the expression below the line" Change "expression" to "judgment". "corresponds to some [expression/query], for which a type is computed." Well, except that the "statEnv |-" isn't part of the expression/query. Maybe say that the part between the turnstile and the colon corresponds to some expression/query. "The expression usually has patterns in it" Change "expression" to "judgment". "The expressions above the line" Change "expressions" to "judgments". "the expressions on each side" On each side of what? Maybe just change to "those expressions" (or "those sub-expressions"). "At each point in the recursion, an appropriate matching inference rule is sought" Maybe clarify what an "appropriate matching" rule is. (A rule whose conclusion has a structure that matches that of the premise in question.) "if at any point there is no applicable rule, then static type inference has failed" Not quite. It means that that particular avenue of inference has failed; however, an alternative avenue might succeed. And actually, I think you've written the spec so that, if failure happens, it shouldn't be for lack of a matching rule -- that would indicate incompleteness of the spec. Instead, failure of (an avenue of) inference should only happen when one is unable to satisfy the premises of a rule. Some of this discussion might fit back in section 2.1.5. 4509 1 jmdyck 2005-07-11 23:21:06 +0000 (Also...) "The overall static type inference algorithm is recursive" I don't think you can call it an algorithm, given that you haven't shown that it terminates, and you haven't given an effective means to to test the subtype relation. 8365 2 mff 2006-02-21 20:04:01 +0000 Incorporated all the suggested changes, although I left the changes in place and did not move any text to 2.1.5. 12185 3 jmdyck 2006-09-29 05:47:12 +0000 "The the part after the : and before |- in the judgment below the line..." s/The the/The/ Swap ":" and "|-". After "before", insert "the". 12558 4 simeon 2006-10-19 23:41:29 +0000 Done. - Jerome