.

diff --git a/pres-esop15/01.xhtml b/pres-esop15/01.xhtml
index fe24755..d74a138 100644 (file)
--- a/pres-esop15/01.xhtml
+++ b/pres-esop15/01.xhtml
@@ -195,26 +195,26 @@
       </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 &lt;a href={<u>$l</u><span class="xpath">/@href</span>}&gt;&lt;b&gt;{<u>$l</u><span class="xpath">/text()</span>}&lt;/b&gt;&lt;/a&gt;
-                 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",""));
@@ -235,8 +235,8 @@
          + 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
@@ -249,10 +249,9 @@
       <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> (&lt;a&gt;Any <span class="typ">&rarrow;</span> &lt;a&gt;Any  <span class="typ">&amp;</span>  Any<span class="typ">\</span>&lt;a&gt;Any <span class="typ">&rarrow;</span> Any<span class="typ">\</span>&lt;a>Any)
-
+<code style="font-size:90%">   
+  let <u>pretty</u> ((&lt;a&gt;Any <span class="typ">&rarrow;</span> &lt;a&gt;Any)  <span class="typ">&amp;</span>  (Any<span class="typ">\</span>&lt;a&gt;Any <span class="typ">&rarrow;</span> Any<span class="typ">\</span>&lt;a>Any)) =
+      function
     | <span class="pat">&lt;a class="style1" href=<u>h</u> ..&gt; <u>l</u></span> &rarrow; &lt;a href=<u>h</u>&gt;[ &lt;b&gt;<u>l</u> ]
     | <span class="pat">x</span> &rarrow; x
 
@@ -281,7 +280,7 @@
          + 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>
@@ -380,14 +379,14 @@ t &leq; s   &Lrarrow;   &lbrack;t&rbrack; &subseteq;  &lbrack;s&rbrack;
     |  [ _* (<u>x</u> &amp; Int) ]                  &rarrow;  (<u>x</u>, `false)
     |  [ ]                               &rarrow;  (0, `false)
 </code>
-<ol>
-<li><dfn>&lbag;<tt>[ _* (<u>x</u> &amp; Int) Bool* (<u>y</u> &amp; Bool) ]</tt>&rbag;    <span style="display:inline-block;width:5em;text-align:center"> ≡</span>     <tt>[ &top;* Int Bool+ ]</tt></dfn><br/>
+<ol style="list-style-position:inside;">
+<li class="sws-pause"><dfn>&lbag;<tt>[ _* (<u>x</u> &amp; Int) Bool* (<u>y</u> &amp; Bool) ]</tt>&rbag;    <span style="display:inline-block;width:5em;text-align:center"> ≡</span>     <tt>[ &top;* Int Bool+ ]</tt></dfn><br/>
  <span style="text-align:right;display:inline-block;width:94%;">{ x &mapsto; <tt>Int</tt>, y &mapsto; <tt>Bool</tt> }</span>
 </li>
-<li><dfn>&lbag;<tt>[ _* (<u>x</u> &amp; Int) ]</tt>&rbag; <span style="display:inline-block;width:5em;text-align:center"> ≡</span> <tt>[ &top;* Int ]</tt></dfn><br/>
+<li class="sws-pause"><dfn>&lbag;<tt>[ _* (<u>x</u> &amp; Int) ]</tt>&rbag; <span style="display:inline-block;width:5em;text-align:center"> ≡</span> <tt>[ &top;* Int ]</tt></dfn><br/>
   <span style="text-align:right;display:inline-block;width:58%;"> { x &mapsto; <tt>Int</tt> }</span>
 </li>
-<li>Since <dfn><tt>[Int+ Bool* ]</tt> &setminus; ( <tt>[ &top;* Int Bool+ ]</tt> &lor;  <tt>[ &top;* Int]</tt>) ≡ &bottom;  </dfn><br/>
+<li class="sws-pause">Since <dfn><tt>[Int+ Bool* ]</tt> &setminus; ( <tt>[ &top;* Int Bool+ ]</tt> &lor;  <tt>[ &top;* Int]</tt>) ≡ <s>&bottom;</s>  </dfn><br/>
     the third case is unreachable.
 </li>
 
@@ -415,13 +414,13 @@ t &leq; s   &Lrarrow;   &lbrack;t&rbrack; &subseteq;  &lbrack;s&rbrack;
 <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">
@@ -444,9 +443,9 @@ t &leq; s   &Lrarrow;   &lbrack;t&rbrack; &subseteq;  &lbrack;s&rbrack;
 <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>&lt;a&gt;_</tt>:</span>
-    p ≡ <tt id="test">&lt;a&gt;_</tt>   &lor;   <tt>&lt;_&gt;[ _* <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>&lt;a&gt;_</tt>:</span>
+     p ≡ <tt id="test">&lt;a&gt;_</tt>   &lor;   <tt>&lt;_&gt;[ _* <dfn>p</dfn> _* ]</tt>
  
   <span style="font-family:'Open Sans';">Deos not have an ancestor <tt>&lt;b&gt;_</tt>:</span>
     &tau; ≡ &bcirc;   &lor;   &right;(&top;&setminus; <tt>&lt;b&gt;_</tt>) · &tau;   &lor;   &left;(&top;&setminus; <tt>&lt;b&gt;_</tt>) · &tau; </pre>
@@ -483,7 +482,7 @@ nodes in special variables
 </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/>
@@ -498,7 +497,7 @@ nodes in special variables
   &sigma; &vdash; v / p &rleadsto; &gamma;, &sigma;'
 </pre>
 <p style="font-size:90%"><dfn><u>&sigma;</u>, <u>&sigma;'</u></dfn>: mapping from accumulators to
-  values<br/>
+  values. &nbsp;  Initially: <dfn> &sigma; = { ẋ &mapsto; Init(ẋ) | ẋ &in; p }</dfn><br/>
   <dfn><u>v</u></dfn>: input value<br/>
   <dfn><u>p</u></dfn>: pattern<br/>
   <dfn><u>&gamma;</u></dfn>: mapping from capture variables to
@@ -678,16 +677,22 @@ which is not a type.</p>
   <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>