A Core Calculus for XQuery 3.0

Combining Navigational and Pattern-Matching Approaches

+ + + + + + + + + +

Giuseppe Castagna¹	Hyeonseung Im²
Kim Nguyá»n³	VÃ©ronique Benzaken³

+ CNRS, PPS, UniversitÃ© Paris-Diderot, Paris, France
+ Kangwon National University, Chuncheon, Rep. of Korea
+ LRI, UniversitÃ© Paris-Sud, Orsay, France +

XQuery 3.0

W3C standard language for querying XML + databases/documents


+   declare function get_links($page, $print) {
+
+       for $i in $page/descendant::a[not(ancestor::b)]
+       return print($i)
+   }
+
+   declare function pretty($link) {
+       typeswitch($link)
+           case $l as element(a)
+              return switch ($l/@class)
+                 case "style1"
+                     return <a href={$l/@href}><b>{$l/text()}</b></a>
+                 default return $l
+
+           default return $link
+   }
+

+ +

XQuery 3.0

Pros
+ + standardized
+ + nice declarative syntax for paths +
Cons
+ - weird distinction between types/value case
+ - ~~no type-checking for functions~~ +

It's a pity since XML documents are very precisely + typed (DTD, XMLSchemas)

Document type information is validated at runtime rather than + checked statically

&cduce;

A polymorphic functional language (ML-style) equipped with + semantic subtyping

+ +


+  let pretty (<a>_ -> <a>_  &  Any\<a>_ &rarrow; Any\<a>_)
+
+    | <a class="style1" href=h ..> l &rarrow; <a href=h>[ <b>l ]
+    | x &rarrow; x
+
+
+  let get_links (page: <_>_) (print: <a>_ -> <a>_) : [ <a>_ * ] =
+
+      match page with
+      <a>_ & x &rarrow; [ (print x) ]
+    | < (_\âb) > l &rarrow;
+                 (transform l with (i & <_>_) &rarrow; get_links i print)
+    | _ -> [ ]
+
+
+
+
+

+ + +

&cduce;

Pros
+ + Statically typed
+ + compact (and efficient) type and value pattern-matching +
Cons
+ - ~~complex navigation encoded through recursion~~ + - no type inference for functions +

Writing functions to traverse documents is painfull

This work

Add support for path navigation to + &cduce; +
- Enrich the type algebra with zippers (Ã la Huet)
- Extend pattern-matching construct to zipped values and types
- Encode path expressions as recursive patterns
+
Perform a type-directed translation from XQuery to + &cduce;

+ +

&cduce;'s type algebra

+    t ::=  b  |  c  |  t Ã t  |  t &rarrow; t  |  t &lor; t  |  t  &land; t  |  t ∖ t  |  ⊤  |  ⊥  |  α
+

b : ranges over basic types (Int, String, â¦)
+ c : ranges over singleton types + (`A, 42, â¦)
+ α : type variables
+ types are interpreted co-inductively (recursive types) and regular + expression types
+

+    t₁ â¡ (Int Ã t₁) &lor; t₂
+    t₂ â¡ (Bool Ã t₂) &lor; (Bool Ã `nil)
+
+    t₁ â¡ [ Int* Bool+ ]
+
+

Semantic subtyping

+t ≤ s   &Lrarrow;   [t] ⊆  [s]
+

[ ] interpretation of types as sets of + values
+ Allows to reason modulo semantic equivalence of type connectives : +

+      [ Int* (Int | Bool*)? ] &land; [ Int+ (Bool+ | Int)* ] â¡ [Int+ Bool*]
+

&cduce; patterns

    p ::=  t  |  p | p  |  p & p  | (p, p) |  x

t ranges over types
+ x ranges over capture variables
+ patterns are also co-inductively interpreted (recursive patterns) +

v / p : matching a value against a pattern yields a + substitution from variables to values
+ &lbag; p &rbag; : the set of values accepted by a + pattern is a type
+ t / p : matching a type against a pattern yields a + substitution from variables to types
+

&cduce; patterns (example)

Assume l has type [ Int+ Bool* ], consider:


+       match l with
+       [ _* (x & Int) Bool* (y & Bool) ] &rarrow;  (x, y)
+    |  [ _* (x & Int) ]                  &rarrow;  (x, `false)
+    |  [ ]                               &rarrow;  (0, `false)
+

&lbag;[ _* (x & Int) Bool* (y & Bool) ]&rbag; â¡ [ ⊤* Int Bool+ ]
+ yield : { x ↦ Int, y ↦ Bool } +
&lbag;[ _* (x & Int) ]&rbag; â¡ [ ⊤* Int ]
+ yield : { x ↦ Int } +
Since [Int+ Bool* ] ∖ ( [ ⊤* Int Bool+ ] &lor; [ ⊤* Int]) â¡ ⊥ + the third case is unreachable. +

+ +

&cduce; data-model

Sequences are nested pairs: [ v₁ â¦ v_n ] â¡ (v₁, (â¦, (v_n, `nil))) +

XML documents are tagged sequences:

<foo>[ v₁  â¦ v_n ] â¡ (`foo, [ v₁  â¦ v_n ])

Ususal lisp-like encoding of trees, how to perform navigation + (including upward ?)

Zippers (1/2)

Introduced in 1997 by GÃ©rard Huet
Stack of visited
Push the current node on the stack when descending
Put the top of the stack and pop it to go backward
Tag the elements of the stack to remember which of a node we + have visited

 v ::=  â¦  |  v_δ
+ δ ::=  &bcirc;  | &left;v Â· δ | &right;v Â· δ
+

+ +

Zippers (2/2)

fst (resp. snd) takes the first (resp. second) + projection of a pair and update its zipper accordingly:

    v₁ â¡ (1, (2, (3, (4, `nil))))_&bcirc;
+    v₁₁ â¡ fst v₁ â¡ 1_{&left;(1, (2, (3, (4, `nil))))_&bcirc; Â· &bcirc;}
+    v₂ â¡ snd v₁ â¡ (2, (3, (4, `nil)))_{&right;(1, (2, (3, (4, `nil))))_&bcirc; Â· &bcirc;}
+    v₃ â¡ snd v₂ â¡ (3, (4, `nil))_{&right;v₂ Â· &right;v₁ Â· &bcirc;}
+

up pops returns the head of the zipper:

    up v₃ â¡ v₂ â¡ (2, (3, (4, `nil)))_{&right;(1, (2, (3, (4, `nil))))_&bcirc; Â· &bcirc;}
+

Zipper types

We extend the type-algebra with zipper types:

 t ::=  â¦  |  t_τ
+ τ ::=  &bcirc;  |  &left;t Â· τ  | &right;t Â· τ  |  τ &lor; τ  |  τ ∖ τ  |  &ztop;
+

&bcirc;: singleton type denoting the empty zipper
+ &ztop;: the top zipper types
+ Zipper types are interpreted co-inductively (regular expressions on + zippers)

+ Int_{(&left;⊤)* &bcirc;}: type of + integers that are the leftmost descendant of a tree.
+ [ [â¦] [â¦] ]]]>_&bcirc;: type of + HTML documents
+ [ â¦ ]]]>_&ztop;: types of links in any context + +

Tree navigation

Since patterns contain types, we can check complex + conditions:

+    p â¡ <a>_   &lor;   <_>[ _* p _* ]
+ 
+    τ â¡ &bcirc;   &lor;   &right;⊤ Â· τ   &lor;   &left;(⊤∖ <b>_) Â· τ 
+
+


+    match v with
+       p_τ & x &rarrow; â¦
+   | _        &rarrow; â¦
+

+We want more, namely return all descendants (ancestor, + children, siblings, â¦) of a node matching a particular condition +

+Remark: (recursive) patterns already perform a recursive traversal + of the value +

+Idea: Piggy back on the traversal and accumulate +nodes in special variables +

+ +

Operators and Accumulators

An operator is a 4-tupple (o, n_o, + &rleadsto;_o, &rarrow;_o), where:

o: is the accumulator name
+n_o: is the arity of o
+&rleadsto;_o: +&mathV;^n_o &rsarrow; &mathV;, the reduction relation
+&rarrow;_o: +&mathT;^n_o &rsarrow; &mathT;, the typing relation
+

An accumulator is a variable (ranged over + by áº, áº, â¦) with:

+ Op(áº): an operator
+ Init(áº) ∈ &mathV; : an initial value
+

Some operators

+    v, v' &rleadsto;^cons, (v, v') 

+    v, `nil &rleadsto;^snoc (v, `nil)

+    v, (v',v'') &rleadsto;^snoc (v', snoc(v,v''))

+

Now we can use accumulators equipped with cons/snoc in + patterns. Instead of matching a single node against a variable, it + accumulates that node in sequence (in reverse or in-order).

Pattern matching semantics (v/p)

+  σ; δ ⊢ v / p &rleadsto; γ, σ'
+

σ, σ': mapping from accumulators to + values
+ v: input value
+ p: pattern
+ γ: mapping from capture variables to + values
+ δ: current context +

+ v ∈ [ t ] + σ; δ ⊢ v / t &rleadsto; ∅, + σ +

(type) + +

+ + σ; δ ⊢ v / áº &rleadsto; ∅, + σ[ áº := Op(áº) (v_δ, σ(áº)) ] +

(acc) + +

+ + σ; δ ⊢ v / x &rleadsto; { x ↦ v }, + σ +

(var) + +

+ σ; &left;v Â· δ ⊢ (fst v)/p₁ + &rleadsto; γ₁, σ' + σ'; &right;v Â· δ ⊢ (snd v)/p₂ + &rleadsto; γ₂, σ'' + + σ; δ ⊢ v / + (p₁, p₂) &rleadsto; + γ₁∪ γ₂, + σ'' +

(pair) +â¦ and some other rules for alternation, failure, recursion, etc. +

Typing of patterns (with accumulators) 1/2

Well known that typing path expressions escapes regular tree languages + (i.e. &cduce;'s types). Consider: +

+      t â¡ <c>[ <a>[] t <b>[] ]    &lor;   <c>[]   
+

The set of all a or b labeled + descendants + is { [<a>[]ⁿ <b>[]ⁿ ] | n â¥ 0 } +which is not a type.

Intuitively it means that when applying a + recursive pattern against a recursive type, we may generate an + ~~infinite number of distinct types~~ for an accumulator. +

Typing of patterns (with accumulators) 2/2

We use the typing relation of operators to introduce + approximations:

+    t₀, [ (t₁ &lor; â¦ &lor; t_n)* ] &rarrow;^cons [ (t₀ &lor; t₁ &lor; â¦ &lor; t_n)* ] 

+    t₀, [ (t₁ &lor; â¦ &lor; t_n)* ] &rarrow;^snoc [ (t₀ &lor; t₁ &lor; â¦ &lor; t_n)* ]
+

Ensures termination of typechecking of patterns.

Results

Zippers (in values, types, patterns) are orthogonal to the rest of the language

Subtyping and typechecking are extended straightforwardly
Typing of patterns introduces sound approximations only for accumulators
Provided the operators are sound, the whole language remains type-safe

From zippers to XPath

We use regular expressions over basic &left;/&right; zippers to encode XPath

   [ [
+          []
+          []
+          [  [] ]
+        ]
+   ]]]>
+

+
+

A Core Calculus for XQuery 3.0

Combining Navigational and Pattern-Matching Approaches

XQuery 3.0

XQuery 3.0

&cduce;

&cduce;

This work

&cduce;'s type algebra

Semantic subtyping

&cduce; patterns

&cduce; patterns (example)

&cduce; data-model

Zippers (1/2)

Zippers (2/2)

Zipper types

Tree navigation

Operators and Accumulators

Some operators

Pattern matching semantics (v/p)

Typing of patterns (with accumulators) 1/2

Typing of patterns (with accumulators) 2/2

Results

From zippers to XPath

Downward axes

Upward axes

Other results

Conclusion, thoughts and future work