1 <?xml version="1.0" encoding="utf-8" ?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
3 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"
5 <!ENTITY in "<small style='font-size:small'>∈</small>">
6 <!ENTITY notin "<small style='font-size:small'>∉</small>">
13 <!ENTITY cduce "ℂDuce">
16 <!ENTITY setminus "∖" >
17 <!ENTITY bottom "<tt>Empty</tt>" > <!-- 𝟘 -->
18 <!ENTITY top "<tt>Any</tt>" > <!-- 𝟙 -->
19 <!ENTITY subseteq "⊆" >
24 <!ENTITY lbrack "<span style='font-size:xx-large;'>⟦</span>" >
25 <!ENTITY rbrack "<span style='font-size:xx-large;'>⟧</span>" >
27 <!ENTITY left "<tt style='color:#d33'>L</tt>" >
28 <!ENTITY right "<tt style='color:#33d'>R</tt>">
30 <!ENTITY rleadsto "⟿"> <!-- -->
37 <html xmlns="http://www.w3.org/1999/xhtml" >
39 <title>A Core Calculus for XQuery 3.0</title>
41 <meta http-equiv="Content-Type"
42 content="text/html; charset=utf-8" />
43 <meta name="copyright"
44 content="Copyright © 2013 Kim Nguyễn" />
47 <script src="../jquery-2.0.3.min.js" type="text/javascript" ></script>
48 <script src="../libs/raphael-min.js" type="text/javascript" ></script>
49 <!-- Load the library -->
50 <script src="../simpleWebSlides.js" type="text/javascript" ></script>
52 <link rel="stylesheet" href="../simpleWebSlides.css" type="text/css" media="all" />
53 <!-- Load a custom Theme, the class-element marks this style-sheet
54 a "theme" that can be swtiched dynamicaly -->
55 <link class="sws-theme" rel="stylesheet" title="U-Psud style" href="../themes/uPsud.css" type="text/css" />
57 <!-- Customize some templates and initialize -->
59 <script type="text/javascript">
60 SWS.Config['sws-slide-change'] = SWS.Effects.slideChangeFadeOutIn;
61 SWS.Config['sws-object-deactivate'] = SWS.Effects.objectDeactivateFadeOut;
62 SWS.Config['sws-object-activate'] = SWS.Effects.objectActivateFadeIn;
64 //Ensures that we load SWS at the very end, after MathJax has
67 $(window).load(SWS.Presentation.init);
69 var col_change = function (sel, col) {
70 return function (canvas) {
71 canvas.find(".xpath *").css("color","");
72 var objs = canvas.find(sel);
73 objs.css("color", col);
76 var reg = SWS.Presentation.registerCallback;
82 src: url("OpenSans-Regular.ttf") format("truetype");
83 font-family: "Open Sans";
88 src: url("OpenSans-Bold.ttf") format("truetype");
89 font-family: "Open Sans";
94 src: url("OpenSans-Italic.ttf") format("truetype");
95 font-family: "Open Sans";
100 src: url("OpenSans-BoldItalic.ttf") format("truetype");
101 font-family: "Open Sans";
109 font-family: 'Open Sans',sans-serif;
111 background-color: white;
121 pre, dfn, .infer { font-family : serif;
128 vertical-align:text-bottom;
129 display:inline-block;
140 vertical-align:text-bottom;
141 display:inline-block;
147 margin: 0pt 0pt 0pt 0pt;
148 padding: 0pt 0pt 0pt 0pt;
151 .infer > span:last-child {
152 margin: 0pt 0pt 0pt 0pt;
153 padding: 0pt 0pt 0pt 0pt;
154 border-width: 1pt 0pt 0pt 0pt;
156 border-color: #292928;
159 vertical-align:text-top;
165 margin: 0pt 0pt 0pt 0pt;
166 padding: 0pt 0pt 0pt 0pt;
168 span.fill { display:inline-block;
176 <div class="sws-slide sws-cover sws-option-nofooter">
177 <h1 style="font-size:200%;position:relative;top:-1em;">A Core Calculus for XQuery 3.0</h1>
178 <h3>Combining Navigational and Pattern-Matching Approaches</h3>
179 <div style="text-align:center;">
180 <table style="display:inline-block">
182 <td>Giuseppe Castagna<sup>1</sup></td>
183 <td>Hyeonseung Im<sup>2</sup></td>
186 <td><u>Kim Nguyễn</u><sup>3</sup></td>
187 <td>Véronique Benzaken<sup>3</sup></td>
191 <p style="font-size:80%;position:absolute;bottom:2.5em;left:4em;">
192 1 CNRS, PPS, Université Paris-Diderot, Paris, France <br/>
193 2 Kangwon National University, Chuncheon, Rep. of Korea<br/>
194 3 LRI, Université Paris-Sud, Orsay, France
197 <div class="sws-slide">
199 <p>W3C standard to query XML documents</p>
200 <code style="background:white;font-size:90%;">
201 declare function <u>get_links</u>(<u>$page</u>, <u>$print</u>) {
202 <span class="for">for</span> <u>$i</u> <span class="for">in</span> <u>$page</u><span class="xpath">/descendant::a[not(ancestor::b)]</span>
203 <span class="for">return</span> <u>$print</u>(<u>$i</u>)
206 declare function <u>pretty</u>(<u>$link</u>) {
207 <span class="ts">typeswitch</span>(<u>$link</u>)
208 <span class="ts">case</span> <u>$l</u> <span class="ts">as element(a)</span>
209 return <span class="sw">switch</span> (<u>$l</u><span class="xpath">/@class</span>)
210 <span class="sw">case</span> "style1"
211 return <a href={<u>$l</u><span class="xpath">/@href</span>}><b>{<u>$l</u><span class="xpath">/text()</span>}</b></a>
212 default return <u>$l</u>
214 <span class="ts">default return</span> <u>$link</u>
217 let $bold_links := get_links(document("file.xhtml"), $pretty)
219 <script type="text/javascript">
220 reg ("0", col_change(".xpath, .for, .ts, .sw",""));
221 reg ("1", col_change(".xpath", "#f80"));
222 reg ("2", col_change(".for",""));
223 reg ("2", col_change(".for", "#290"));
224 reg ("3", col_change(".ts", ""));
225 reg ("3", col_change(".ts", "#80f"));
226 reg ("4", col_change(".sw", ""));
227 reg ("4", col_change(".sw", "#0f2"));
230 <div class="sws-slide">
235 + nice declarative syntax for paths
238 - sometime tedious to extract subtrees while preserving the structure<br/>
239 - <s>no typechecking for functions (typechecking is optional in 3.0)</s>
242 <p>It's a pity since XML <em>documents</em> are very precisely
243 typed (DTD, XMLSchemas)</p>
244 <p>Document type information is validated at runtime rather than
245 checked statically</p>
247 <div class="sws-slide">
249 <p>A polymorphic functional language equipped with
250 semantic subtyping</p>
252 <code style="font-size:90%">
253 let <u>pretty</u> ((<a>Any <span class="typ">&rarrow;</span> <a>Any) <span class="typ">&</span> (Any<span class="typ">\</span><a>Any <span class="typ">&rarrow;</span> Any<span class="typ">\</span><a>Any)) =
255 | <span class="pat"><a class="style1" href=<u>h</u> ..> <u>l</u></span> &rarrow; <a href=<u>h</u>>[ <b><u>l</u> ]
256 | <span class="pat">x</span> &rarrow; x
259 let <u>get_links</u> (page: <(Any)>Any) (print: <a>Any <span class="typ">&rarrow;</span> <a>Any) : <span class="typ">[ <a>Any * ]</span> =
262 <span class="pat"><a>_ & x</span> &rarrow; [ (print x) ]
263 | <span class="pat">< (_\‘b) > l</span> &rarrow;
264 (<span class="lc">transform l with</span> <span class="pat">(i & <_>_)</span> &rarrow; get_links i print)
265 | <span class="pat">_</span> &rarrow; [ ]
267 <script type="text/javascript">
268 reg ("0", col_change(".pat,.typ,.lc",""));
269 reg ("1", col_change(".pat", "#f80"));
270 reg ("2", col_change(".typ", "#290"));
271 reg ("3", col_change(".lc", "#80f"));
275 <div class="sws-slide">
279 + Statically typed <br/>
280 + compact (and efficient) type and value pattern-matching
283 - <s>complex navigation encoded through explicit recursion</s><br/>
284 - no type inference for functions
287 <p>Writing functions to traverse documents is painfull</p>
289 <div class="sws-slide">
291 <ol style="margin-left:1em; margin-right:0.25em;list-style-position:inside;">
292 <li id="tobox" style="padding:1em 0em 1em 0em;"><span class="lh">Add support for path navigation to
294 <ul style="margin-top:2em;">
295 <li>Enrich the type algebra with <em>zippers</em> (à la Huet)</li>
296 <li>Extend pattern-matching construct to <em>zipped values and types</em></li>
297 <li>Encode path expressions as recursive patterns</li>
300 <li class="ll" style="padding:1em 0em 1em 0em;">Perform a type-directed translation from XQuery to
303 <script type="text/javascript">
304 reg (1, col_change(".lh", "#f83"));
305 reg (1, col_change(".ll", "#bbb"));
308 <div class="sws-slide">
309 <h1>&cduce;'s type algebra</h1>
310 <p>A set &mathT; of types</p>
311 <pre style="text-align:center;"> t ::= b | c | <u>t × t</u> | <u>t &rarrow; t</u> | <mark>t &lor; t</mark> | <mark>t &land; t</mark> | <mark>t ∖ t</mark> | <mark>⊤</mark> | <mark>⊥</mark> | α
313 <p><dfn>b</dfn> : ranges over basic types (<tt>Int</tt>, <tt>String</tt>, …)<br/>
314 <dfn>c</dfn> : ranges over singleton types
315 (<tt>`A</tt>, <tt>42</tt>, …)<br/>
316 <u>Type constructors</u> <br/>
317 <mark>Boolean connectives</mark> <br/>
318 <dfn>α</dfn> : type variables<br/>
319 types are interpreted co-inductively: recursive types and regular
320 expression types<br/>
322 <div style="vertical-align:top;">
323 <pre style="width:50%;display:inline-block;"> t<sub>1</sub> ≡ (<tt>Int</tt> × t<sub>1</sub>) &lor; t<sub>2</sub>
324 t<sub>2</sub> ≡ (<tt>Bool</tt> × t<sub>2</sub>) &lor; (<tt>Bool</tt> × <tt>`nil</tt>)
326 <pre style="width:30%;display:inline-block;"> <span class="sws-pause">t<sub>1</sub> ≡ <tt>[ Int* Bool+ ]</tt></span></pre>
329 <div class="sws-slide">
330 <h1>Semantic subtyping</h1>
331 <pre style="text-align:center;">
332 t ≤ s &Lrarrow; [t] ⊆ [s]
334 <p><dfn>[ ]</dfn> interpretation of types as sets of
336 Allows to reason <i>modulo</i> semantic equivalence of type connectives :
339 <tt>[ Int* (Int | Bool*)? ]</tt> &land; <tt>[ Int+ (Bool+ | Int)* ]</tt> ≡ <tt>[Int+ Bool*]</tt>
342 <div class="sws-slide">
343 <h1>&cduce; data-model</h1>
344 <p>The usual sets &mathV; of values:</p>
345 <pre style="text-align:center"> v ::= <tt>1</tt> | … | <tt>`Foo</tt> | (v, v) | λx.e
347 <p>Sequences are nested pairs (<i>à la</i> Lisp):</p>
348 <pre style="text-align:center;"><tt>[</tt> v<sub>1</sub> … v<sub>n</sub> <tt>]</tt> ≡ (v<sub>1</sub>, (…, (v<sub>n</sub>, <tt>`nil</tt>)))
350 <p>XML documents are tagged sequences: <pre style="text-align:center;"><tt><foo>[</tt> v<sub>1</sub> … v<sub>n</sub> <tt>]</tt> ≡ (<tt>`foo</tt>, <tt>[</tt> v<sub>1</sub> … v<sub>n</sub> <tt>]</tt>)</pre>
352 <p>(Sometimes we write <tt>[ ]</tt> for the variant <tt>`nil</tt>)</p>
353 <p>Everything is built on top of products and variants</p>
355 <div class="sws-slide">
356 <h1>&cduce; patterns</h1>
357 <p><i>(a.k.a. the left-hand side of an arrow in a match … with)</i></p>
358 <pre style="text-align:center;"> p ::= t | x | <u>(p, p)</u> | <mark>p | p</mark> | <mark>p & p</mark> </pre>
359 <p><dfn>t</dfn> ranges over types<br/>
360 <dfn>x</dfn> ranges over capture variables<br/>
361 <u>Pair patterns</u><br/>
362 <mark> Alternation |, Intersection &</mark><br/>
363 patterns are also co-inductively interpreted (recursive patterns)
365 <p><dfn><u>v / p</u></dfn> : matching a value against a pattern yields a
366 substitution from variables to values<br/>
367 <dfn><u>&lbag; p &rbag;</u></dfn> : the set of values accepted by a
368 pattern is <u>a type</u><br/>
369 <dfn><u> t / p</u></dfn> : matching a type against a pattern yields a
370 substitution from variables to types<br/>
373 <div class="sws-slide">
374 <h1>&cduce; patterns (example)</h1>
375 <p>Assume <tt><u>l</u></tt> has type <tt>[ Int+ Bool* ]</tt>, consider:</p>
378 [ _* (<u>x</u> & Int) Bool* (<u>y</u> & Bool) ] &rarrow; (<u>x</u>, <u>y</u>)
379 | [ _* (<u>x</u> & Int) ] &rarrow; (<u>x</u>, `false)
380 | [ ] &rarrow; (0, `false)
382 <ol style="list-style-position:inside;">
383 <li class="sws-pause"><dfn>&lbag;<tt>[ _* (<u>x</u> & Int) Bool* (<u>y</u> & Bool) ]</tt>&rbag; <span style="display:inline-block;width:5em;text-align:center"> ≡</span> <tt>[ ⊤* Int Bool+ ]</tt></dfn><br/>
384 <span style="text-align:right;display:inline-block;width:94%;">{ x ↦ <tt>Int</tt>, y ↦ <tt>Bool</tt> }</span>
386 <li class="sws-pause"><dfn>&lbag;<tt>[ _* (<u>x</u> & Int) ]</tt>&rbag; <span style="display:inline-block;width:5em;text-align:center"> ≡</span> <tt>[ ⊤* Int ]</tt></dfn><br/>
387 <span style="text-align:right;display:inline-block;width:58%;"> { x ↦ <tt>Int</tt> }</span>
389 <li class="sws-pause">Since <dfn><tt>[Int+ Bool* ]</tt> ∖ ( <tt>[ ⊤* Int Bool+ ]</tt> &lor; <tt>[ ⊤* Int]</tt>) ≡ <s>⊥</s> </dfn><br/>
390 the third case is unreachable.
398 <div class="sws-slide">
399 <h1>Zippers (1/2)</h1>
401 <li>Introduced in 1997 by Gérard Huet</li>
402 <li>Stack of visited nodes</li>
403 <li>Push the current node on the stack when traversing a pair</li>
404 <li>Take the top of the stack to go backward</li>
405 <li>Tag the elements of the stack to remember which component of a
406 pair we have visited</li>
408 <pre style="text-align:center;"> v ::= … | v<sub>δ</sub>
409 δ ::= &bcirc; | &left;v · δ | &right;v · δ
413 <div class="sws-slide">
414 <h1>Zippers (2/2)</h1>
415 <p><tt><u>fst</u></tt> (resp. <tt><u>snd</u></tt>) takes the first (resp. second)
416 projection of a pair and update its zipper accordingly:</p>
417 <pre> v<sub>1</sub> ≡ (1, (2, (3, (4, `nil))))<sub>&bcirc;</sub>
418 v<sub>11</sub> ≡ <tt>fst</tt> v<sub>1</sub> ≡ 1<sub>&left;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
419 v<sub>2</sub> ≡ <tt>snd</tt> v<sub>1</sub> ≡ (2, (3, (4, `nil)))<sub>&right;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
420 v<sub>3</sub> ≡ <tt>snd</tt> v<sub>2</sub> ≡ (3, (4, `nil))<sub>&right;v<sub>2</sub> · &right;v<sub>1</sub> · &bcirc; </sub>
422 <p><tt><u>up</u></tt> returns the head of the zipper: </p>
423 <pre> <tt>up</tt> v<sub>3</sub> ≡ v<sub>2</sub> ≡ (2, (3, (4, `nil)))<sub>&right;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
426 <div class="sws-slide">
427 <h1>Zipper types</h1>
428 <p>We extend the type-algebra with zipper types:</p>
429 <pre style="text-align:center;"> t ::= … | t<sub>τ</sub>
430 τ ::= &bcirc; | &left;t · τ | &right;t · τ | τ &lor; τ | τ ∖ τ | &ztop;
432 <p><dfn>&bcirc;</dfn>: singleton type denoting the empty zipper (root element)<br/>
433 <dfn>&ztop;</dfn>: the top zipper type<br/>
434 Zipper types are interpreted co-inductively<br/><br/>
435 <dfn><tt>Int</tt><sub>(&left;⊤)* &bcirc;</sub></dfn> <span style="float:right;">type of
436 integers that are the leftmost descendant of a tree</span><br/><br/>
437 <dfn><tt><![CDATA[<html>[ <head>[…] <body>[…] ]]]></tt><sub>&bcirc;</sub></dfn> <span style="float:right;">type of
438 HTML documents</span><br/><br/>
439 <dfn><tt><![CDATA[<a href=String>[ … ]]]></tt><sub> &ztop;</sub></dfn> <span style="float:right;">types of links nested in any context</span>
442 <div class="sws-slide">
443 <h1>Tree navigation</h1>
444 <p>Since patterns contain types, we can check complex
446 <pre style="margin-left:1em;width:62%;display:inline-block;border-width:0pt 1pt 0pt
447 0pt; border-style:dashed;border-color: black;vertical-align:middle"> <span style="font-family:'Open Sans';">Has a descendant <tt><a>_</tt>:</span>
448 p ≡ <tt id="test"><a>_</tt> &lor; <tt><_>[ _* <dfn>p</dfn> _* ]</tt>
450 <span style="font-family:'Open Sans';">Deos not have an ancestor <tt><b>_</tt>:</span>
451 τ ≡ &bcirc; &lor; &right;(⊤∖ <tt><b>_</tt>) · τ &lor; &left;(⊤∖ <tt><b>_</tt>) · τ </pre>
452 <code style="width:20%;display:inline-block;vertical-align:middle">
454 <dfn>p<sub>τ</sub></dfn> & <u>x</u> &rarrow; …
455 | _ &rarrow; …</code>
456 <p style="background:white">We want more, namely return <i>all</i> descendants (ancestors,
457 children, siblings, …) of a node matching a particular condition
459 Remark: (recursive) patterns <u>already perform a recursive traversal
462 <em>Idea</em>: Piggy back on the traversal and <em>accumulate</em>
463 nodes in special variables
466 <div class="sws-slide">
467 <h1>Operators and Accumulators</h1>
468 <p>An <u>operator</u> is a 4-tupple <dfn>(o, n<sub>o</sub>,
469 &rleadsto;<sub>o</sub>, &rarrow;<sub>o</sub>)</dfn>, where:</p>
470 <p><dfn><u>o</u></dfn>: is the accumulator name<br/>
471 <dfn><u>n<sub>o</sub></u></dfn>: is the arity of <u>o</u><br/>
472 <dfn><u>&rleadsto;<sub>o</sub></u></dfn>:
473 &mathV;<sup>n<sub>o</sub></sup> &rsarrow; &mathV;, the reduction relation <br/>
474 <dfn><u>&rarrow;<sub>o</sub></u></dfn>:
475 &mathT;<sup>n<sub>o</sub></sup> &rsarrow; &mathT;, the typing relation <br/>
477 <p>An <u>accumulator</u> is a variable (ranged over
478 by <u>ẋ</u>, <u>ẏ</u>, …) with:<br/><br/>
479 <dfn><u>Op(ẋ)</u></dfn>: an operator<br/>
480 <dfn><u>Init(ẋ)</u> ∈ &mathV;</dfn> : an initial value<br/>
483 <div class="sws-slide">
484 <h1>Some operators</h1>
485 <pre style="margin-left:1em;">
486 v, v' &rleadsto;<sup>cons,</sup> (v, v') <br/>
487 v, <tt>`nil</tt> &rleadsto;<sup>snoc</sup> (v, <tt>`nil</tt>)<br/>
488 v, (v',v'') &rleadsto;<sup>snoc</sup> (v', snoc(v,v''))<br/>
490 <p>Now we can use accumulators equipped with cons/snoc in
491 patterns. Instead of matching a single node against a variable, it
492 <u>accumulates</u> that node in sequence (in reverse or in-order).</p>
494 <div class="sws-slide">
495 <h1>Pattern matching semantics (simplified)</h1>
496 <pre style="text-align:center;">
497 σ ⊢ v / p &rleadsto; γ, σ'
499 <p style="font-size:90%"><dfn><u>σ</u>, <u>σ'</u></dfn>: mapping from accumulators to
500 values. Initially: <dfn> σ = { ẋ ↦ Init(ẋ) | ẋ ∈ p }</dfn><br/>
501 <dfn><u>v</u></dfn>: input value<br/>
502 <dfn><u>p</u></dfn>: pattern<br/>
503 <dfn><u>γ</u></dfn>: mapping from capture variables to
506 <div style="padding:0em 1em 0em; text-align:justify;background:white;">
508 <span> v ∈ [ t ]</span>
509 <span>σ; δ ⊢ v / t &rleadsto; ∅,
511 </div><span>(type)</span>
515 <span>σ ⊢ v / ẋ &rleadsto; ∅,
516 σ[ ẋ := Op(ẋ) (v, σ(ẋ)) ]</span>
517 </div><span>(acc)</span>
521 <span>σ ⊢ v / x &rleadsto; { x ↦ v },
523 </div><span>(var)</span>
526 <span>σ ⊢ (fst v)/p<sub>1</sub>
527 &rleadsto; γ<sub>1</sub>, σ' </span>
528 <span>σ' ⊢ (snd v)/p<sub>2</sub>
529 &rleadsto; γ<sub>2</sub>, σ''
531 <span>σ ⊢ v /
532 (p<sub>1</sub>, p<sub>2</sub>) &rleadsto;
533 γ<sub>1</sub>∪ γ<sub>2</sub>,
535 </div><span>(pair)</span> <span class="fill"></span>
536 <span style="position:relative;top:-1em;">Remember, if <dfn>v ≡ (v1,v2)<sub>δ</sub></dfn> then <dfn><tt>fst v</tt> ≡ v<sub>1 &left;v · δ</sub></dfn> and <dfn><tt>snd v</tt> ≡ v<sub>2 &right;v · δ</sub></dfn><br/>
537 (some other rules for alternation, failure, recursion, <i>etc.</i>)</span>
540 <div class="sws-slide">
541 <h1>Typing of patterns (with accumulators) 1/2</h1>
542 <p>Well known that typing path expressions escapes regular tree languages
543 (i.e. &cduce;'s types). Consider:
545 <pre style="margin:-3em 0pt -1em;">
546 t ≡ <tt><c>[ <u><a>[]</u> t <u><b>[]</u> ] </tt> &lor; <tt><c>[]</tt> <img style="margin-left:3em;width:15%;vertical-align:middle;" src="anbn_tree.svg" alt="anbn"/>
548 <p>The set of all <tt><u>a</u></tt> or <tt><u>b</u></tt> labeled
550 is <dfn>{ <tt>[<u><a>[]</u></tt><sup>n</sup> <tt><u><b>[]</u></tt><sup>n</sup> <tt>]</tt> | n ≥ 0 }</dfn>
551 which is not a type.</p>
552 <p> Intuitively it means that when applying a
553 recursive pattern against a recursive type, we may generate an
554 <s>infinite number of distinct types</s> for an accumulator.
557 <div class="sws-slide">
558 <h1>Typing of patterns (with accumulators) 2/2</h1>
559 <p>We use the typing relation of operators to introduce
562 <u>t<sub>0</sub></u>, <tt>[</tt> (t<sub>1</sub> &lor; … &lor; t<sub>n</sub>)<tt>* ]</tt> &rarrow;<sup>cons</sup> <tt>[</tt> (<u>t<sub>0</sub></u> &lor; t<sub>1</sub> &lor; … &lor; t<sub>n</sub>)<tt>* ]</tt> <br/>
563 <u>t<sub>0</sub></u>, <tt>[</tt> (t<sub>1</sub> &lor; … &lor; t<sub>n</sub>)<tt>* ]</tt> &rarrow;<sup>snoc</sup> <tt>[</tt> (<u>t<sub>0</sub></u> &lor; t<sub>1</sub> &lor; … &lor; t<sub>n</sub>)<tt>* ]</tt>
565 <p>Ensures termination of typechecking of patterns.</p>
567 <div class="sws-slide">
569 <p>Zippers (in values, types, patterns) are a conservative extension</p>
571 <li><u>Subtyping and typechecking</u> are extended straightforwardly</li>
572 <li>Typing of patterns introduces <u>sound approximations</u> only for accumulators</li>
573 <li>Provided the operators are sound, the whole language remains <u>type-safe</u></li>
576 <div class="sws-slide">
577 <h1>Downward XPath axes</h1>
578 <pre style="background:white"> <tt>self ::</tt> t ≡ (ẋ <tt>&</tt> t | _ )<sub>&ztop;</sub> (Init(ẋ) = [], Op(ẋ) = <tt>snoc</tt>)
580 <span class="sws-pause"><tt>child ::</tt> t ≡ <tt><_>[</tt> (ẋ <tt>&</tt> t | _ )<tt>* ]</tt><sub>&ztop;</sub></span>
582 <p class="sws-pause">Example: applying <tt><u>child::<b>_</u></tt> to the document</p>
583 <code> <doc>[ <a>[] <b>[] <c>[] <b>[] ]<sub>&bcirc;</sub>
584 <span class="sws-pause"><_>[ <span class="sws-pause"> _</span> <mark class="sws-pause">(ẋ & <b>_)</mark> <span>_</span> <mark>(ẋ & <b>_)</mark>]<sub >&ztop;</sub></span>
586 <span class="sws-pause"> ẋ↦ [ <b>[]<sub>&left;… &right;… &right;… &bcirc;</sub> <b>[]<sub>&left;… &right;… &right;… &right;… &right;… &bcirc;</sub> ] </span>
589 <pre class="sws-pause">
590 <tt>descendant-or-self::</tt> t ≡ X ≡ ((ẋ <tt>&</tt> t | _ ) <tt> & </tt> (<tt><_>[</tt> X <tt>* ]</tt>)<sub>&ztop;</sub> | _ )
592 <tt>descendant</tt> :: t ≡ <tt><_>[ (descendant-or-self::</tt>t<tt>)* ]</tt><sub>&ztop;</sub>
595 <script type="text/javascript">
600 svgDoc = svgDoc || document.getElementById("svgRBTree").contentDocument;
601 var f = svgDoc.getElementById("nodef");
602 f.style['fillOpacity'] = "0";
603 var elems = svgDoc.getElementsByClassName("parentf");
604 for(var i = 0; i < elems.length; i++) {
605 elems[i].style['strokeWidth'] = '2px';
609 reg (0, function (c) {
614 reg (1, function (c) {
616 var f = svgDoc.getElementById("nodef");
617 console.log(' Opacity ' + f.style['fillOpacity']);
618 f.style['fillOpacity'] = "0.5";
619 console.log(' Opacity ' + f.style['fillOpacity']);
622 reg (2, function (c) {
624 var elems = svgDoc.getElementsByClassName("parentf");
625 for(i = 0; i < elems.length; i++) {
626 elems[i].style['strokeWidth'] = '6px';
629 reg (3, function (c) { console.log(3); reset(); });
634 <div class="sws-slide">
635 <h1>Binary-tree encoding</h1>
636 <p>We use <u>regular expressions</u> over basic &left;/&right; zippers to encode upward XPath</p>
637 <code style="width:50%;float:left;"> <![CDATA[<a>[ <b>[
643 </code><img style="width:17.5%;" src="ex_ntree.svg" alt="ex_ntree" /><br/>
644 <p class="sws-pause"><img style="margin-top:-1em;margin-left:5%;width:85%;" src="rb_tree.svg" alt="rb_tree"/></p>
647 <div class="sws-slide">
648 <h1>Upward XPath axes</h1>
649 <div style="position:absolute; width:80%; left:10%;top:15%">
650 <object id="svgRBTree" data="rb_tree.svg" type="image/svg+xml" style="z-index:1;position:absolute;width:100%" />
651 <object class="sws-onframe-1" id="svgRBTree1" data="rb_tree01.svg" type="image/svg+xml" style="z-index:1;position:absolute;width:100%" />
652 <object class="sws-onframe-2" id="svgRBTree2" data="rb_tree02.svg" type="image/svg+xml" style="z-index:3;position:absolute;width:100%" />
653 <object class="sws-onframe-3" id="svgRBTree3" data="rb_tree03.svg" type="image/svg+xml" style="z-index:4;position:absolute;width:100%" />
654 <object class="sws-onframe-4" id="svgRBTree4" data="rb_tree04.svg" type="image/svg+xml" style="z-index:5;position:absolute;width:100%" />
656 <pre style="position:absolute;bottom:5%;z-index:1;"> <tt>parent ::</tt> t ≡ ⊤<sub> (&left;_) · (&right;_)* · (&right; ẋ & t) · (( (&left; _) · &ztop;) &lor; &bcirc; )</sub>
658 <span class="sws-onframe-5"> <tt>ancestor ::</tt> t ≡ ⊤<sub> ( (&left;_) · (&right;_)* · (&right; ẋ & t) )* · &bcirc; </sub></span>
664 <pre style="position:absolute;bottom:5%;z-index:2;">
666 <span class="sws-onframe-1" style="font-size:110%;color:#1fb01b;">⬆</span> <span class="sws-onframe-2" style="font-size:110%;color:#1fb01b;">⬆</span> <span class="sws-onframe-3" style="font-size:110%;color:#1fb01b;">⬆</span> <span class="sws-onframe-4" style="font-size:110%;color:#1fb01b;">⬆</span>
668 <span class="sws-onframe-5" style="color:#1fb01b;border-color:#1fb01b;border-top-style:dashed;border-top-width:3pt;position:relative;top:0.5em;"> parent </span>
674 <div class="sws-slide">
675 <h1>Other results</h1>
677 <li>Encoding of paths is compositional</li>
678 <li>Once we have paths, translation from XQuery to &cduce; is straightforward</li>
679 <li>We also give a direct typing algorithm for XQuery 3.0 rather than typing the translation to &cduce;</li>
680 <li>Accumulators in patterns allow to encode other XPath constructs (<tt>count()</tt>, <tt>position()</tt>, …)</li>
682 <p>Still some problems in the on-going implementation</p>
684 <li>Nice syntax to expose paths + patterns to the programmer</li>
685 <li>Pretty printing of error messages: décompilation of regular expressions</li>
688 <div class="sws-slide">
689 <h1>Conclusion, thoughts and future work</h1>
691 <li style="padding-top:0.5em;">Adding path expressions to a functional language such as &cduce; is possible </li>
692 <li style="padding-top:0.5em;">Semantic subtyping and regular expression types play nicely with zippers</li>
693 <li style="padding-top:0.5em;">In terms of language design, exposing directly zippers to the programmer (still need work at the syntax level)</li>
694 <li style="padding-top:0.5em;">Implementation on-going (including a &cduce; to javascript backend)</li>
695 <li style="padding-top:0.5em;">Extend the approach to Json (google ``path language for json´´), i.e. generalize from products to extensible records</li>
697 <p class="sws-pause" style="text-align:center;"><b><u>Thank you!</u></b></p>