</p>
</div>
<div class="sws-slide">
- <h1>The XQuery 3.0 W3C Standard</h1>
+ <h1>XQuery 3.0</h1>
+<p>W3C standard to query XML documents</p>
<code style="background:white;font-size:90%;">
-
declare function <u>get_links</u>(<u>$page</u>, <u>$print</u>) {
<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>
- <span class="for">return</span> <u>print</u>(<u>$i</u>)
+ <span class="for">return</span> <u>$print</u>(<u>$i</u>)
}
declare function <u>pretty</u>(<u>$link</u>) {
<span class="ts">typeswitch</span>(<u>$link</u>)
- <span class="ts">case</span> <u>$l</u> <span class="ts">as element(a)</span>
- return <span class="sw">switch</span> (<u>$l</u><span class="xpath">/@class</span>)
- <span class="sw">case</span> "style1"
+ <span class="ts">case</span> <u>$l</u> <span class="ts">as element(a)</span>
+ return <span class="sw">switch</span> (<u>$l</u><span class="xpath">/@class</span>)
+ <span class="sw">case</span> "style1"
return <a href={<u>$l</u><span class="xpath">/@href</span>}><b>{<u>$l</u><span class="xpath">/text()</span>}</b></a>
- default return <u>$l</u>
+ default return <u>$l</u>
- <span class="ts">default return</span> <u>$link</u>
+ <span class="ts">default return</span> <u>$link</u>
}
- let $bold_links := get_links(document("file.html"), $pretty)
+ let $bold_links := get_links(document("file.xhtml"), $pretty)
</code>
<script type="text/javascript">
reg ("0", col_change(".xpath, .for, .ts, .sw",""));
+ nice declarative syntax for paths
</li>
<li>Cons<br/>
- - weird distinction between types/value case<br/>
- - <s>no type-checking for functions</s>
+ - sometime tedious to extract subtrees while preserving the structure<br/>
+ - <s>no typechecking for functions (typechecking is optional in 3.0)</s>
</li>
</ul>
<p>It's a pity since XML <em>documents</em> are very precisely
<p>A polymorphic functional language equipped with
semantic subtyping</p>
-<code style="font-size:90%"> <i>(* Here _ is an alias for the top type Any *)</i>
-
- 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)
-
+<code style="font-size:90%">
+ 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)) =
+ function
| <span class="pat"><a class="style1" href=<u>h</u> ..> <u>l</u></span> &rarrow; <a href=<u>h</u>>[ <b><u>l</u> ]
| <span class="pat">x</span> &rarrow; x
+ compact (and efficient) type and value pattern-matching
</li>
<li>Cons<br/>
- - <s>complex navigation encoded through recursion</s><br/>
+ - <s>complex navigation encoded through explicit recursion</s><br/>
- no type inference for functions
</li>
</ul>
<div class="sws-slide">
<h1>&cduce;'s type algebra</h1>
<p>A set &mathT; of types</p>
-<pre style="text-align:center;"> t ::= b | c | <u>t × t</u> | <u>t &rarrow; t</u> | <a>t &lor; t</a> | <mark>t &land; t</mark> | <mark>t ∖ t</mark> | <mark>⊤</mark> | <mark>⊥</mark> | α
+<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> | α
</pre>
<p><dfn>b</dfn> : ranges over basic types (<tt>Int</tt>, <tt>String</tt>, …)<br/>
<dfn>c</dfn> : ranges over singleton types
| [ _* (<u>x</u> & Int) ] &rarrow; (<u>x</u>, `false)
| [ ] &rarrow; (0, `false)
</code>
-<ol>
-<li><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/>
+<ol style="list-style-position:inside;">
+<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/>
<span style="text-align:right;display:inline-block;width:94%;">{ x ↦ <tt>Int</tt>, y ↦ <tt>Bool</tt> }</span>
</li>
-<li><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/>
+<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/>
<span style="text-align:right;display:inline-block;width:58%;"> { x ↦ <tt>Int</tt> }</span>
</li>
-<li>Since <dfn><tt>[Int+ Bool* ]</tt> ∖ ( <tt>[ ⊤* Int Bool+ ]</tt> &lor; <tt>[ ⊤* Int]</tt>) ≡ ⊥ </dfn><br/>
+<li class="sws-pause">Since <dfn><tt>[Int+ Bool* ]</tt> ∖ ( <tt>[ ⊤* Int Bool+ ]</tt> &lor; <tt>[ ⊤* Int]</tt>) ≡ <s>⊥</s> </dfn><br/>
the third case is unreachable.
</li>
<h1>Zippers (2/2)</h1>
<p><tt><u>fst</u></tt> (resp. <tt><u>snd</u></tt>) takes the first (resp. second)
projection of a pair and update its zipper accordingly:</p>
-<pre> v<sub>1</sub> ≡ (1, (2, (3, (4, `nil))))<sub>&bcirc;</sub>
- v<sub>11</sub> ≡ <tt>fst</tt> v<sub>1</sub> ≡ 1<sub>&left;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
- 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>
- 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>
+<pre> v<sub>1</sub> ≡ (1, (2, (3, (4, `nil))))<sub>&bcirc;</sub>
+ v<sub>11</sub> ≡ <tt>fst</tt> v<sub>1</sub> ≡ 1<sub>&left;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
+ 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>
+ 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>
</pre>
<p><tt><u>up</u></tt> returns the head of the zipper: </p>
-<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>
+<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>
</pre>
</div>
<div class="sws-slide">
<h1>Tree navigation</h1>
<p>Since patterns contain types, we can check complex
conditions:</p>
-<pre style="width:62%;display:inline-block;border-width:0pt 1pt 0pt
- 0pt; border-style:dashed;border-color: black;vertical-align:middle"> <span style="font-family:'Open Sans';">Has a descendant <tt><a>_</tt>:</span>
- p ≡ <tt id="test"><a>_</tt> &lor; <tt><_>[ _* <dfn>p</dfn> _* ]</tt>
+<pre style="margin-left:1em;width:62%;display:inline-block;border-width:0pt 1pt 0pt
+ 0pt; border-style:dashed;border-color: black;vertical-align:middle"> <span style="font-family:'Open Sans';">Has a descendant <tt><a>_</tt>:</span>
+ p ≡ <tt id="test"><a>_</tt> &lor; <tt><_>[ _* <dfn>p</dfn> _* ]</tt>
<span style="font-family:'Open Sans';">Deos not have an ancestor <tt><b>_</tt>:</span>
τ ≡ &bcirc; &lor; &right;(⊤∖ <tt><b>_</tt>) · τ &lor; &left;(⊤∖ <tt><b>_</tt>) · τ </pre>
</div>
<div class="sws-slide">
<h1>Some operators</h1>
- <pre>
+ <pre style="margin-left:1em;">
v, v' &rleadsto;<sup>cons,</sup> (v, v') <br/>
v, <tt>`nil</tt> &rleadsto;<sup>snoc</sup> (v, <tt>`nil</tt>)<br/>
v, (v',v'') &rleadsto;<sup>snoc</sup> (v', snoc(v,v''))<br/>
σ ⊢ v / p &rleadsto; γ, σ'
</pre>
<p style="font-size:90%"><dfn><u>σ</u>, <u>σ'</u></dfn>: mapping from accumulators to
- values<br/>
+ values. Initially: <dfn> σ = { ẋ ↦ Init(ẋ) | ẋ ∈ p }</dfn><br/>
<dfn><u>v</u></dfn>: input value<br/>
<dfn><u>p</u></dfn>: pattern<br/>
<dfn><u>γ</u></dfn>: mapping from capture variables to
<li>Encoding of paths is compositional</li>
<li>Once we have paths, translation from XQuery to &cduce; is straightforward</li>
<li>We also give a direct typing algorithm for XQuery 3.0 rather than typing the translation to &cduce;</li>
+ <li>Accumulators in patterns allow to encode other XPath constructs (<tt>count()</tt>, <tt>position()</tt>, …)</li>
+</ul>
+<p>Still some problems in the on-going implementation</p>
+<ul>
+ <li>Nice syntax to expose paths + patterns to the programmer</li>
+ <li>Pretty printing of error messages: décompilation of regular expressions</li>
</ul>
</div>
<div class="sws-slide">
<h1>Conclusion, thoughts and future work</h1>
<ul>
- <li>Adding path expressions to a functional language such as &cduce; is possible </li>
- <li>Semantic subtyping and regular expression types play nicely with zippers</li>
- <li>In terms of language design, exposing directly zippers to the programmer (still need work at the syntax level)</li>
- <li>Implementation on-going (including a &cduce; to javascript backend)</li>
- <li>Extend the approach to Json (google ``path language for json´´), i.e. generalise from products to extensible records</li>
+ <li style="padding-top:0.5em;">Adding path expressions to a functional language such as &cduce; is possible </li>
+ <li style="padding-top:0.5em;">Semantic subtyping and regular expression types play nicely with zippers</li>
+ <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>
+ <li style="padding-top:0.5em;">Implementation on-going (including a &cduce; to javascript backend)</li>
+ <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>
</ul>
<p class="sws-pause" style="text-align:center;"><b><u>Thank you!</u></b></p>
</div>