From 4dc5a5d25fbacec5f5ddb30601966289af9d329a Mon Sep 17 00:00:00 2001 From: Reece Dunn Date: Tue, 16 Oct 2018 13:15:50 +0100 Subject: [PATCH 1/7] Proposal for Tuple Sequence Types --- tuple-sequence-types.md | 112 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 112 insertions(+) create mode 100644 tuple-sequence-types.md diff --git a/tuple-sequence-types.md b/tuple-sequence-types.md new file mode 100644 index 0000000..4396263 --- /dev/null +++ b/tuple-sequence-types.md @@ -0,0 +1,112 @@ +# Tuple Sequence Types + +**Author**: Reece H. Dunn. 67 Bricks. + +Define a sequence type with a fixed number of items and explicit types for each element. + + +## Description + +\[Definition: A *tuple sequence* is a sequence where each instance of that sequence always has the same number of items, and the type of the items in the sequence do not change between different instances of the same tuple sequence.\] The tuple sequence applies to the flattened sequence, where nested sequences have been combined and empty sequences have been removed. + +> Example: +> +> A 2D point could be defined as: +> +> declare type point2D = ( xs:double, xs:double ); +> +> Here, the first value is the x coordinate and the second value is the y coordinate. + +> Note: +> +> A tuple sequence must have more than one value. If a type in parenthesis only specifies a single item, it is a parenthesized item type. + +If a tuple sequence is assigned a flattened sequence that contains a different number of items than is specified by the tuple sequence type, a type error is raised. + +If an item in the flattened sequence being assigned to a tuple sequence type is not convertible to the corresponding type at the same position, a type error is raised. + +If the types of two tuple sequence types are not compatible (see the judgement `subtype(A, B)` definition below) a type error is raised. + +An XQuery processor may infer a tuple sequence type from an untyped sequence during the static analysis phase. + + +### The judgement subtype(A, B) + +The following draft text is added before the table in this section of the XPath/XQuery specification. + +1. `B` is a tuple sequence type `(Bi_1, Bi_2, ..., Bi_N)`, `A` is a tuple sequence type `(Ai_1, Ai_2, ..., Ai_M)`, where `N` equals `M`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai_I)`. +1. `B` is `Bi*` or `Bi+`, `A` is a tuple sequence type `(Ai_1, Ai_2, ..., Ai_N)`; for values of `I` between `1` and `N`, `subtype(Bi, Ai_I)`. +1. `B` is a tuple sequence type `(Bi_1, Bi_2, ..., Bi_N)`, `A` is `Ai*` or `Ai+`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai)`. +1. The result of the `subtype(A, B)` judgement can be determined from the table below, which makes use of the auxiliary judgement `subtype-itemtype(Ai, Bi)` defined in __2.5.6.2 The judgement `subtype-itemtype(Ai, Bi)`__. + + +### Influences + +Various other languages such as Python, Scala, C#, and C++ have support for tuple types. + +The syntax for this is the syntax that MarkLogic use to describe the MarkLogic [math:modf](https://docs.marklogic.com/math:modf) function. There, the return type of that function is given as: + +> as (xs:double,xs:integer) + +There is support for tuple-like constructs with the [Type](https://www.w3.org/TR/xquery-semantics/#doc-fs-Type) grammar in XQuery 1.0 and XPath 2.0 Formal Semantics (Second Edition). The difference is that the `Type` syntax allows for mixing tuple, union, and intersection without operator precedence or how to evaluate mixed types. + + +## Use Cases + +This allows better static type checking of these fixed-length sequence types. + +This interacts with the `ParenthesizedItemType` syntax, so could cause confusion there when implementing XQuery. There is no ambiguity in the grammar, provided they are ordered such that `ParenthesizedItemType` takes precedence when parsing a single type in parenthesis. + +I have kept these separate in the grammar for consistency with the existing XQuery type model, especially regarding section 2.5.5.2 Matching an ItemType and an Item: + +> A ParenthesizedItemType matches an item if and only if the item matches the ItemType that is in parentheses. + + +## Examples + +Calculating sin and cos at the same time: + + declare function sincos($angle as xs:double?) as (xs:double, xs:double)? { + (: could use a sincos assembly instruction :) + math:sin($angle), math:cos($angle) + }; + +Complex number conversion: + + declare function polar-to-cartesian($polar as (xs:double, xs:double)) as (xs:double, xs:double) { + $polar[1] * math:cos($polar[2]), + $polar[1] * math:sin($polar[2]) + }; + +Defining a rational number type (using the Saxon 9.8 type declaration syntax): + + declare type rational = ( xs:integer, xs:integer ); + +Using the MarkLogic modf function: + + let $ret as (xs:double, xs:integer) := math:modf(1.25) + return $ret[2] (: returns: 1 :) + + +## Grammar + +__Modified (Integration Points):__ + + ItemType ::= KindTest | ("item" "(" ")") | FunctionTest | MapTest | ArrayTest | AtomicOrUnionType | ParenthesizedSequenceType + +__New:__ + + ParenthesizedSequenceType ::= ParenthesizedItemType | TupleSequenceType + TupleSequenceType ::= "(" ItemType ("," ItemType)* ")" + +__NOTE:__ This allows other sequence-based types to be added to the `ParenthesizedSequenceType` EBNF symbol. + +## Implementation Experience + +1. [XQuery IntelliJ Plugin](https://github.com/rhdunn/xquery-intellij-plugin) -- hand-written recursive-descent parser only for the above syntax, with the fallback to `ParenthesizedItemType` for a single `ItemType` in parenthesis; no type checking. +1. XQuantum XQuery 1.0 -- http://www.cogneticsystems.com/xquery/alignment.html#reg +1. Galax 1.0 -- http://galax.sourceforge.net/doc/alignment.html#toc19, using the XQuery Formal Semantics syntax + +## Related Proposals + +1. Tuple Decomposition -- Extracting the values from a sequence into separate variables in a single for/let/etc. clause. From b08f78c23168776cfeb4af7d790a543b07430850 Mon Sep 17 00:00:00 2001 From: "Reece H. Dunn" Date: Thu, 25 Oct 2018 20:53:40 +0100 Subject: [PATCH 2/7] tuple sequence types: Reworded the influences section for clarity. --- tuple-sequence-types.md | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) diff --git a/tuple-sequence-types.md b/tuple-sequence-types.md index 4396263..c64af21 100644 --- a/tuple-sequence-types.md +++ b/tuple-sequence-types.md @@ -42,25 +42,21 @@ The following draft text is added before the table in this section of the XPath/ ### Influences -Various other languages such as Python, Scala, C#, and C++ have support for tuple types. +Various other languages such as Python, Scala, C#, and C++ have support for tuple types that have a fixed number of items. They allow the type of each item to be specified such that they can be different types. The syntax for this is the syntax that MarkLogic use to describe the MarkLogic [math:modf](https://docs.marklogic.com/math:modf) function. There, the return type of that function is given as: -> as (xs:double,xs:integer) +> as (xs:double, xs:integer) -There is support for tuple-like constructs with the [Type](https://www.w3.org/TR/xquery-semantics/#doc-fs-Type) grammar in XQuery 1.0 and XPath 2.0 Formal Semantics (Second Edition). The difference is that the `Type` syntax allows for mixing tuple, union, and intersection without operator precedence or how to evaluate mixed types. +There is support for tuple-like constructs with the [Type](https://www.w3.org/TR/xquery-semantics/#doc-fs-Type) grammar in XQuery 1.0 and XPath 2.0 Formal Semantics (Second Edition). The difference is that the `Type` syntax allows for mixing tuple, union, and intersection without operator precedence or how to evaluate mixed types. The formal methods Type or similar syntax is implemented in the following XPath/XQuery processors: +1. XQuantum XQuery 1.0 -- http://www.cogneticsystems.com/xquery/alignment.html#reg +1. Galax 1.0 -- http://galax.sourceforge.net/doc/alignment.html#toc19 ## Use Cases This allows better static type checking of these fixed-length sequence types. -This interacts with the `ParenthesizedItemType` syntax, so could cause confusion there when implementing XQuery. There is no ambiguity in the grammar, provided they are ordered such that `ParenthesizedItemType` takes precedence when parsing a single type in parenthesis. - -I have kept these separate in the grammar for consistency with the existing XQuery type model, especially regarding section 2.5.5.2 Matching an ItemType and an Item: - -> A ParenthesizedItemType matches an item if and only if the item matches the ItemType that is in parentheses. - ## Examples @@ -101,12 +97,6 @@ __New:__ __NOTE:__ This allows other sequence-based types to be added to the `ParenthesizedSequenceType` EBNF symbol. -## Implementation Experience - -1. [XQuery IntelliJ Plugin](https://github.com/rhdunn/xquery-intellij-plugin) -- hand-written recursive-descent parser only for the above syntax, with the fallback to `ParenthesizedItemType` for a single `ItemType` in parenthesis; no type checking. -1. XQuantum XQuery 1.0 -- http://www.cogneticsystems.com/xquery/alignment.html#reg -1. Galax 1.0 -- http://galax.sourceforge.net/doc/alignment.html#toc19, using the XQuery Formal Semantics syntax - ## Related Proposals 1. Tuple Decomposition -- Extracting the values from a sequence into separate variables in a single for/let/etc. clause. From e2de9258abf18b6ece9881f7b40be7061363a556 Mon Sep 17 00:00:00 2001 From: "Reece H. Dunn" Date: Thu, 25 Oct 2018 21:21:11 +0100 Subject: [PATCH 3/7] tuple sequence types: Changed the 'tuple sequence' term to 'restricted sequence' and better clarify the intention of the proposal. --- tuple-sequence-types.md | 42 +++++++++++++++++++++++------------------ 1 file changed, 24 insertions(+), 18 deletions(-) diff --git a/tuple-sequence-types.md b/tuple-sequence-types.md index c64af21..5a5845a 100644 --- a/tuple-sequence-types.md +++ b/tuple-sequence-types.md @@ -1,13 +1,13 @@ -# Tuple Sequence Types +# Restricted Sequence Type **Author**: Reece H. Dunn. 67 Bricks. -Define a sequence type with a fixed number of items and explicit types for each element. +Define a sequence with a fixed number of items and explicit types for each element. ## Description -\[Definition: A *tuple sequence* is a sequence where each instance of that sequence always has the same number of items, and the type of the items in the sequence do not change between different instances of the same tuple sequence.\] The tuple sequence applies to the flattened sequence, where nested sequences have been combined and empty sequences have been removed. +\[Definition: A *restricted sequence type* is a sequence type that is limited to containing a fixed number of items.\] This restriction places constraints on a sequence type like specifying the type and cardinality of a sequence, it does not define a new type. > Example: > @@ -19,40 +19,46 @@ Define a sequence type with a fixed number of items and explicit types for each > Note: > -> A tuple sequence must have more than one value. If a type in parenthesis only specifies a single item, it is a parenthesized item type. +> A restricted sequence must have more than one value. If a type in parenthesis only specifies a single item, it is a parenthesized item type. -If a tuple sequence is assigned a flattened sequence that contains a different number of items than is specified by the tuple sequence type, a type error is raised. +A restricted sequence type may specify different types for the items in the sequence. -If an item in the flattened sequence being assigned to a tuple sequence type is not convertible to the corresponding type at the same position, a type error is raised. +> Example: +> +> declare function find-at($items, $value) as (item(), xs:integer)? external; + +If a restricted sequence is assigned a flattened sequence that contains a different number of items than is specified by the restricted sequence type, a type error is raised. -If the types of two tuple sequence types are not compatible (see the judgement `subtype(A, B)` definition below) a type error is raised. +If an item in the flattened sequence being assigned to a restricted sequence type is not convertible to the corresponding type at the same position, a type error is raised. -An XQuery processor may infer a tuple sequence type from an untyped sequence during the static analysis phase. +If the types of two restricted sequence types are not compatible (see the judgement `subtype(A, B)` definition below) a type error is raised. + +An XQuery processor may infer a restricted sequence type from an untyped sequence during the static analysis phase. ### The judgement subtype(A, B) The following draft text is added before the table in this section of the XPath/XQuery specification. -1. `B` is a tuple sequence type `(Bi_1, Bi_2, ..., Bi_N)`, `A` is a tuple sequence type `(Ai_1, Ai_2, ..., Ai_M)`, where `N` equals `M`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai_I)`. -1. `B` is `Bi*` or `Bi+`, `A` is a tuple sequence type `(Ai_1, Ai_2, ..., Ai_N)`; for values of `I` between `1` and `N`, `subtype(Bi, Ai_I)`. -1. `B` is a tuple sequence type `(Bi_1, Bi_2, ..., Bi_N)`, `A` is `Ai*` or `Ai+`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai)`. +1. `B` is a restricted sequence type `(Bi_1, Bi_2, ..., Bi_N)`, `A` is a restricted sequence type `(Ai_1, Ai_2, ..., Ai_M)`, where `N` equals `M`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai_I)`. +1. `B` is `Bi*` or `Bi+`, `A` is a restricted sequence type `(Ai_1, Ai_2, ..., Ai_N)`; for values of `I` between `1` and `N`, `subtype(Bi, Ai_I)`. +1. `B` is a restricted sequence type `(Bi_1, Bi_2, ..., Bi_N)`, `A` is `Ai*` or `Ai+`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai)`. 1. The result of the `subtype(A, B)` judgement can be determined from the table below, which makes use of the auxiliary judgement `subtype-itemtype(Ai, Bi)` defined in __2.5.6.2 The judgement `subtype-itemtype(Ai, Bi)`__. ### Influences -Various other languages such as Python, Scala, C#, and C++ have support for tuple types that have a fixed number of items. They allow the type of each item to be specified such that they can be different types. - -The syntax for this is the syntax that MarkLogic use to describe the MarkLogic [math:modf](https://docs.marklogic.com/math:modf) function. There, the return type of that function is given as: +Various other languages such as Python, Scala, C#, and C++ support restricted sequences as a distinct tuple type that has a fixed number of items. They allow the type of each item to be specified such that they can be different types. -> as (xs:double, xs:integer) - -There is support for tuple-like constructs with the [Type](https://www.w3.org/TR/xquery-semantics/#doc-fs-Type) grammar in XQuery 1.0 and XPath 2.0 Formal Semantics (Second Edition). The difference is that the `Type` syntax allows for mixing tuple, union, and intersection without operator precedence or how to evaluate mixed types. The formal methods Type or similar syntax is implemented in the following XPath/XQuery processors: +There is support for restricted sequence constructs with the [Type](https://www.w3.org/TR/xquery-semantics/#doc-fs-Type) grammar in XQuery 1.0 and XPath 2.0 Formal Semantics (Second Edition). The difference is that the `Type` syntax allows for mixing tuple, union, and intersection without operator precedence or how to evaluate mixed types. The formal methods Type or similar syntax is implemented in the following XPath/XQuery processors: 1. XQuantum XQuery 1.0 -- http://www.cogneticsystems.com/xquery/alignment.html#reg 1. Galax 1.0 -- http://galax.sourceforge.net/doc/alignment.html#toc19 +This is used in the MarkLogic definition of the vendor-specific [math:modf](https://docs.marklogic.com/math:modf) function. There, the return type of that function is given as: + +> as (xs:double, xs:integer) + ## Use Cases This allows better static type checking of these fixed-length sequence types. @@ -99,4 +105,4 @@ __NOTE:__ This allows other sequence-based types to be added to the `Parenthesiz ## Related Proposals -1. Tuple Decomposition -- Extracting the values from a sequence into separate variables in a single for/let/etc. clause. +1. Sequence Decomposition -- Extracting the values from a sequence into separate variables in a single for/let/etc. clause. From 501c4cbcb8dcc74eefeb0c2cef0d64b4f409fbc7 Mon Sep 17 00:00:00 2001 From: "Reece H. Dunn" Date: Thu, 25 Oct 2018 21:54:50 +0100 Subject: [PATCH 4/7] restricted sequence types: Update the syntax based on a suggestion by Michael Kay. --- tuple-sequence-types.md | 41 ++++++++++++++++++++++++----------------- 1 file changed, 24 insertions(+), 17 deletions(-) diff --git a/tuple-sequence-types.md b/tuple-sequence-types.md index 5a5845a..db25757 100644 --- a/tuple-sequence-types.md +++ b/tuple-sequence-types.md @@ -1,8 +1,8 @@ -# Restricted Sequence Type +# Restricted Sequences **Author**: Reece H. Dunn. 67 Bricks. -Define a sequence with a fixed number of items and explicit types for each element. +Limit a sequence to a fixed number of items with explicit types for each element. ## Description @@ -13,7 +13,7 @@ Define a sequence with a fixed number of items and explicit types for each eleme > > A 2D point could be defined as: > -> declare type point2D = ( xs:double, xs:double ); +> declare type point2D = sequence-of( xs:double, xs:double ); > > Here, the first value is the x coordinate and the second value is the y coordinate. @@ -25,7 +25,9 @@ A restricted sequence type may specify different types for the items in the sequ > Example: > -> declare function find-at($items, $value) as (item(), xs:integer)? external; +> declare function find-at( +> $items, $value +> ) as sequence-of( item(), xs:integer )? external; If a restricted sequence is assigned a flattened sequence that contains a different number of items than is specified by the restricted sequence type, a type error is raised. @@ -40,9 +42,9 @@ An XQuery processor may infer a restricted sequence type from an untyped sequenc The following draft text is added before the table in this section of the XPath/XQuery specification. -1. `B` is a restricted sequence type `(Bi_1, Bi_2, ..., Bi_N)`, `A` is a restricted sequence type `(Ai_1, Ai_2, ..., Ai_M)`, where `N` equals `M`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai_I)`. -1. `B` is `Bi*` or `Bi+`, `A` is a restricted sequence type `(Ai_1, Ai_2, ..., Ai_N)`; for values of `I` between `1` and `N`, `subtype(Bi, Ai_I)`. -1. `B` is a restricted sequence type `(Bi_1, Bi_2, ..., Bi_N)`, `A` is `Ai*` or `Ai+`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai)`. +1. `B` is a restricted sequence `sequence-of(Bi_1, Bi_2, ..., Bi_N)`, `A` is a restricted sequence `sequence-of(Ai_1, Ai_2, ..., Ai_M)`, where `N` equals `M`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai_I)`. +1. `B` is `Bi*` or `Bi+`, `A` is a restricted sequence `sequence-of(Ai_1, Ai_2, ..., Ai_N)`; for values of `I` between `1` and `N`, `subtype(Bi, Ai_I)`. +1. `B` is a restricted sequence `sequence-of(Bi_1, Bi_2, ..., Bi_N)`, `A` is `Ai*` or `Ai+`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai)`. 1. The result of the `subtype(A, B)` judgement can be determined from the table below, which makes use of the auxiliary judgement `subtype-itemtype(Ai, Bi)` defined in __2.5.6.2 The judgement `subtype-itemtype(Ai, Bi)`__. @@ -59,34 +61,40 @@ This is used in the MarkLogic definition of the vendor-specific [math:modf](http > as (xs:double, xs:integer) +Due to incompatibilities with the XQuery 3.0 `ParenthesizedItemType` a different syntax is used in this proposal, based on a suggestion by Michael Kay. + ## Use Cases -This allows better static type checking of these fixed-length sequence types. +This allows better static type checking of fixed-length sequences. ## Examples Calculating sin and cos at the same time: - declare function sincos($angle as xs:double?) as (xs:double, xs:double)? { + declare function sincos( + $angle as xs:double? + ) as sequence-of(xs:double, xs:double)? { (: could use a sincos assembly instruction :) math:sin($angle), math:cos($angle) }; Complex number conversion: - declare function polar-to-cartesian($polar as (xs:double, xs:double)) as (xs:double, xs:double) { + declare function polar-to-cartesian( + $polar as sequence-of(xs:double, xs:double) + ) as sequence-of(xs:double, xs:double) { $polar[1] * math:cos($polar[2]), $polar[1] * math:sin($polar[2]) }; Defining a rational number type (using the Saxon 9.8 type declaration syntax): - declare type rational = ( xs:integer, xs:integer ); + declare type rational = sequence-of( xs:integer, xs:integer ); Using the MarkLogic modf function: - let $ret as (xs:double, xs:integer) := math:modf(1.25) + let $ret as sequence-of(xs:double, xs:integer) := math:modf(1.25) return $ret[2] (: returns: 1 :) @@ -94,14 +102,13 @@ Using the MarkLogic modf function: __Modified (Integration Points):__ - ItemType ::= KindTest | ("item" "(" ")") | FunctionTest | MapTest | ArrayTest | AtomicOrUnionType | ParenthesizedSequenceType + SequenceType ::= ("empty-sequence" "(" ")") + | (ItemType OccurrenceIndicator?) + | (SequenceOfTest "?"?) /* new */ __New:__ - ParenthesizedSequenceType ::= ParenthesizedItemType | TupleSequenceType - TupleSequenceType ::= "(" ItemType ("," ItemType)* ")" - -__NOTE:__ This allows other sequence-based types to be added to the `ParenthesizedSequenceType` EBNF symbol. + SequenceOfTest ::= "sequence-of" "(" ItemType ("," ItemType)* ")" ## Related Proposals From 4cac38e54646fe6486b85b2635168d681a5fba5a Mon Sep 17 00:00:00 2001 From: "Reece H. Dunn" Date: Thu, 25 Oct 2018 21:57:15 +0100 Subject: [PATCH 5/7] Rename tuple-sequence-types.md to restricted-sequences.md. --- tuple-sequence-types.md => restricted-sequences.md | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename tuple-sequence-types.md => restricted-sequences.md (100%) diff --git a/tuple-sequence-types.md b/restricted-sequences.md similarity index 100% rename from tuple-sequence-types.md rename to restricted-sequences.md From ded33c9f02dd02e3ab0e32b8954834505c921815 Mon Sep 17 00:00:00 2001 From: Reece Dunn Date: Fri, 26 Oct 2018 12:21:12 +0100 Subject: [PATCH 6/7] restricted sequences: expand the subtype judgement definition text. --- restricted-sequences.md | 43 ++++++++++++++++++++++++++++++++++++----- 1 file changed, 38 insertions(+), 5 deletions(-) diff --git a/restricted-sequences.md b/restricted-sequences.md index db25757..868a949 100644 --- a/restricted-sequences.md +++ b/restricted-sequences.md @@ -2,6 +2,8 @@ **Author**: Reece H. Dunn. 67 Bricks. +**Revision**: 3 + Limit a sequence to a fixed number of items with explicit types for each element. @@ -40,12 +42,34 @@ An XQuery processor may infer a restricted sequence type from an untyped sequenc ### The judgement subtype(A, B) -The following draft text is added before the table in this section of the XPath/XQuery specification. +\[Definition: The *cardinality* of a sequence is a possibly infinite set of non-negative integers.\] This constrains the number of items in a sequence. + +\[Definition: The *required item type list* of a restricted sequence subtype is the specified `ItemType`s of each item in the restricted sequence.\] If the sequence type is not a restricted sequence, each type in the *required item type list* is the same as the *item type* of the sequence type. + +The *cardinality* and *item type* of a sequence are given as follows: + +| Type | Cardinality | Item Type | Description | +|----------------------|-----------------|-------------------|--------------------------------------| +| `xs:error` | `{}` | *missing* | An XSD error type. | +| `xs:error?` | `{0}` | *missing* | An optional XSD error type. | +| `xs:error+` | `{}` | *missing* | An XSD error type sequence. | +| `xs:error*` | `{0}` | *missing* | An optional XSD error type sequence. | +| `empty-sequence()` | `{0}` | *missing* | An empty sequence `()`. | +| `T?` | `{0,1}` | `T` | An optional item. | +| `T` | `{1}` | `T` | A single item. | +| `T*` | `{0..infinity}` | `T` | An optional sequence. | +| `T+` | `{1..infinity}` | `T` | A sequence. | +| `(T1, T2, ..., Tn)?` | `{0..n}` | `item()` | An optional restricted sequence. | +| `(T1, T2, ..., Tn)` | `{1..n}` | `item()` | A restricted sequence. | + +> Proposal Note: +> +> The rules for `xs:error?`, `xs:error+`, and `xs:error*` here are for compatibility with the XPath/XQuery 3.1 rules for those sequence types. + +The `subtype(A,B)` judgement is true if and only if both of the following are true: -1. `B` is a restricted sequence `sequence-of(Bi_1, Bi_2, ..., Bi_N)`, `A` is a restricted sequence `sequence-of(Ai_1, Ai_2, ..., Ai_M)`, where `N` equals `M`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai_I)`. -1. `B` is `Bi*` or `Bi+`, `A` is a restricted sequence `sequence-of(Ai_1, Ai_2, ..., Ai_N)`; for values of `I` between `1` and `N`, `subtype(Bi, Ai_I)`. -1. `B` is a restricted sequence `sequence-of(Bi_1, Bi_2, ..., Bi_N)`, `A` is `Ai*` or `Ai+`; for values of `I` between `1` and `N`, `subtype(Bi_I, Ai)`. -1. The result of the `subtype(A, B)` judgement can be determined from the table below, which makes use of the auxiliary judgement `subtype-itemtype(Ai, Bi)` defined in __2.5.6.2 The judgement `subtype-itemtype(Ai, Bi)`__. +1. The permitted cardinality of `A` is a subset of the permitted cardinality of `B`. +1. Let `Ai` be the required item type of item `i` in `A` and let `Bi` be the required item type of `i` in `B`; for all `i` in the permitted cardinality of `A`, `itemtype-subtype(Ai, Bi)` is true. ### Influences @@ -63,6 +87,7 @@ This is used in the MarkLogic definition of the vendor-specific [math:modf](http Due to incompatibilities with the XQuery 3.0 `ParenthesizedItemType` a different syntax is used in this proposal, based on a suggestion by Michael Kay. + ## Use Cases This allows better static type checking of fixed-length sequences. @@ -110,6 +135,14 @@ __New:__ SequenceOfTest ::= "sequence-of" "(" ItemType ("," ItemType)* ")" + ## Related Proposals 1. Sequence Decomposition -- Extracting the values from a sequence into separate variables in a single for/let/etc. clause. + + +## Version History + +1. Initial proposal. +1. Revised the *tuple sequence type* terminology as *restricted sequences*, and updated the syntax to avoid parse conflicts with `ParenthesizedItemType`. +1. Updated the `subtype` judgement semantics using a combination of a proposal by Michael Kay and static analysis rules for the XQuery IntelliJ plugin. From b9800b9882ded23d812641ef82209cc59861d6cc Mon Sep 17 00:00:00 2001 From: Reece Dunn Date: Fri, 26 Oct 2018 12:35:01 +0100 Subject: [PATCH 7/7] restricted sequences: updated the main text to reflect feedback from Michael Kay. --- restricted-sequences.md | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/restricted-sequences.md b/restricted-sequences.md index 868a949..1b12209 100644 --- a/restricted-sequences.md +++ b/restricted-sequences.md @@ -9,7 +9,7 @@ Limit a sequence to a fixed number of items with explicit types for each element ## Description -\[Definition: A *restricted sequence type* is a sequence type that is limited to containing a fixed number of items.\] This restriction places constraints on a sequence type like specifying the type and cardinality of a sequence, it does not define a new type. +\[Definition: A *restricted sequence type* is a sequence type that is limited to containing a fixed number of items.\] This restriction places constraints on a sequence type like specifying the type and cardinality of a sequence. It does not define a new distinct type, but instead defines a subtype of a sequence type. > Example: > @@ -23,7 +23,7 @@ Limit a sequence to a fixed number of items with explicit types for each element > > A restricted sequence must have more than one value. If a type in parenthesis only specifies a single item, it is a parenthesized item type. -A restricted sequence type may specify different types for the items in the sequence. +A restricted sequence type may specify different types for the items in the sequence. Additionally, the restricted sequence may be made optional by using the `?` occurrence relation. > Example: > @@ -31,14 +31,6 @@ A restricted sequence type may specify different types for the items in the sequ > $items, $value > ) as sequence-of( item(), xs:integer )? external; -If a restricted sequence is assigned a flattened sequence that contains a different number of items than is specified by the restricted sequence type, a type error is raised. - -If an item in the flattened sequence being assigned to a restricted sequence type is not convertible to the corresponding type at the same position, a type error is raised. - -If the types of two restricted sequence types are not compatible (see the judgement `subtype(A, B)` definition below) a type error is raised. - -An XQuery processor may infer a restricted sequence type from an untyped sequence during the static analysis phase. - ### The judgement subtype(A, B) @@ -88,10 +80,9 @@ This is used in the MarkLogic definition of the vendor-specific [math:modf](http Due to incompatibilities with the XQuery 3.0 `ParenthesizedItemType` a different syntax is used in this proposal, based on a suggestion by Michael Kay. -## Use Cases - -This allows better static type checking of fixed-length sequences. +## Rationale +The proposal allows the type of a sequence to be further constrained. This (a) makes code more understandable by documenting the interface between functions; (b) enables improved diagnostics as a result of more precise type checking of function arguments and function results; and (c) enables processors (if they wish) to perform more precise static type checking and to use the extra information for optimization. ## Examples @@ -145,4 +136,4 @@ __New:__ 1. Initial proposal. 1. Revised the *tuple sequence type* terminology as *restricted sequences*, and updated the syntax to avoid parse conflicts with `ParenthesizedItemType`. -1. Updated the `subtype` judgement semantics using a combination of a proposal by Michael Kay and static analysis rules for the XQuery IntelliJ plugin. +1. Updated the `subtype` judgement semantics using a combination of a proposed wording by Michael Kay and static analysis rules for the XQuery IntelliJ plugin. The rationale text wording has been written by Michael Kay.