<!ENTITY land "∧" >
<!ENTITY lor "∨" >
<!ENTITY setminus "∖" >
- <!ENTITY bottom "𝟘" >
- <!ENTITY top "𝟙" >
+ <!ENTITY bottom "<tt>Empty</tt>" > <!-- 𝟘 -->
+ <!ENTITY top "<tt>Any</tt>" > <!-- 𝟙 -->
<!ENTITY subseteq "⊆" >
<!ENTITY leq "≤" >
<!ENTITY Lrarrow "⟺">
</p>
</div>
<div class="sws-slide">
- <h1>XQuery 3.0</h1>
- <p>W3C standard language for querying XML
- databases/documents</p>
-<code style="background:white">
- declare function <u>get_links</u>(<u>$page</u>, <u>$print</u>) {
+ <h1>The XQuery 3.0 W3C Standard</h1>
+<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="ts">default return</span> <u>$link</u>
}
+
+ let $bold_links := get_links(document("file.html"), $pretty)
</code>
<script type="text/javascript">
reg ("0", col_change(".xpath, .for, .ts, .sw",""));
</div>
<div class="sws-slide">
<h1>&cduce;</h1>
- <p>A polymorphic functional language (ML-style) equipped with
+ <p>A polymorphic functional language equipped with
semantic subtyping</p>
-<code>
- let <u>pretty</u> (<a>_ -> <a>_ & Any\<a>_ &rarrow; Any\<a>_)
+<code style="font-size:90%"> <i>(* Here _ is an alias for the top type Any *)</i>
- | <a class="style1" href=<u>h</u> ..> <u>l</u> &rarrow; <a href=<u>h</u>>[ <b><u>l</u> ]
- | x &rarrow; x
-
-
- let <u>get_links</u> (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)
- | _ -> [ ]
+ 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)
+ | <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
+ let <u>get_links</u> (page: <(Any)>Any) (print: <a>Any <span class="typ">&rarrow;</span> <a>Any) : <span class="typ">[ <a>Any * ]</span> =
+ match page with
+ <span class="pat"><a>_ & x</span> &rarrow; [ (print x) ]
+ | <span class="pat">< (_\‘b) > l</span> &rarrow;
+ (<span class="lc">transform l with</span> <span class="pat">(i & <_>_)</span> &rarrow; get_links i print)
+ | <span class="pat">_</span> &rarrow; [ ]
</code>
-
+ <script type="text/javascript">
+ reg ("0", col_change(".pat,.typ,.lc",""));
+ reg ("1", col_change(".pat", "#f80"));
+ reg ("2", col_change(".typ", "#290"));
+ reg ("3", col_change(".lc", "#80f"));
+ </script>
</div>
<div class="sws-slide">
</div>
<div class="sws-slide">
<h1>&cduce;'s type algebra</h1>
-<pre>
- 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> | α
+<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>
<p><dfn>b</dfn> : ranges over basic types (<tt>Int</tt>, <tt>String</tt>, …)<br/>
<dfn>c</dfn> : ranges over singleton types
</div>
<div class="sws-slide">
<h1>&cduce; data-model</h1>
-<p>The usual sets of values: constants, λ-abstractions, pairs, …</p>
-<p>Sequences are nested pairs: <dfn><tt>[</tt> v<sub>1</sub> … v<sub>n</sub> <tt>]</tt> ≡ (v<sub>1</sub>, (…, (v<sub>n</sub>, <tt>`nil</tt>)))
-</dfn></p>
+<p>The usual sets &mathV; of values:</p>
+<pre style="text-align:center"> v ::= <tt>1</tt> | … | <tt>`Foo</tt> | (v, v) | λx.e
+</pre>
+<p>Sequences are nested pairs (<i>à la</i> Lisp):</p>
+<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>)))
+</pre>
<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>
</p>
<p>(Sometimes we write <tt>[ ]</tt> for the variant <tt>`nil</tt>)</p>
+<p>Everything is built on top of products and variants</p>
</div>
<div class="sws-slide">
<h1>&cduce; patterns</h1>
| [ ] &rarrow; (0, `false)
</code>
<ol>
-<li><dfn>&lbag;<tt>[ _* (<u>x</u> & Int) Bool* (<u>y</u> & Bool) ]</tt>&rbag; ≡ <tt>[ ⊤* Int Bool+ ]</tt></dfn><br/>
- yield : { x ↦ <tt>Int</tt>, y ↦ <tt>Bool</tt> }
+<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/>
+ <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; ≡ <tt>[ ⊤* Int ]</tt></dfn><br/>
- yield : { x ↦ <tt>Int</tt> }
+<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/>
+ <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>
+<li>Since <dfn><tt>[Int+ Bool* ]</tt> ∖ ( <tt>[ ⊤* Int Bool+ ]</tt> &lor; <tt>[ ⊤* Int]</tt>) ≡ ⊥ </dfn><br/>
the third case is unreachable.
</li>
<li>Introduced in 1997 by Gérard Huet</li>
<li>Stack of visited nodes</li>
<li>Push the current node on the stack when traversing a pair</li>
- <li>Take top of the stack to go backward</li>
+ <li>Take the top of the stack to go backward</li>
<li>Tag the elements of the stack to remember which component of a
pair we have visited</li>
</ul>
<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> ≡ fst v<sub>1</sub> ≡ 1<sub>&left;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
- v<sub>2</sub> ≡ snd v<sub>1</sub> ≡ (2, (3, (4, `nil)))<sub>&right;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
- v<sub>3</sub> ≡ snd v<sub>2</sub> ≡ (3, (4, `nil))<sub>&right;v<sub>2</sub> · &right;v<sub>1</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> up 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">
integers that are the leftmost descendant of a tree</span><br/><br/>
<dfn><tt><![CDATA[<html>[ <head>[…] <body>[…] ]]]></tt><sub>&bcirc;</sub></dfn> <span style="float:right;">type of
HTML documents</span><br/><br/>
- <dfn><tt><![CDATA[<a href=String>[ … ]]]></tt><sub>(&right; ⊤) · &ztop;</sub></dfn> <span style="float:right;">types of links in any context</span>
-
+ <dfn><tt><![CDATA[<a href=String>[ … ]]]></tt><sub> &ztop;</sub></dfn> <span style="float:right;">types of links nested in any context</span>
</p>
</div>
<div class="sws-slide">
<h1>Tree navigation</h1>
<p>Since patterns contain types, we can check complex
conditions:</p>
-<pre style="width:60%;display:inline-block;border-width:0pt 1pt 0pt
+<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><_>[ _* p _* ]</tt>
+ 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>
+ τ ≡ &bcirc; &lor; &right;(⊤∖ <tt><b>_</tt>) · τ &lor; &left;(⊤∖ <tt><b>_</tt>) · τ </pre>
<code style="width:20%;display:inline-block;vertical-align:middle">
match <u>v</u> with
<dfn>p<sub>τ</sub></dfn> & <u>x</u> &rarrow; …
<u>accumulates</u> that node in sequence (in reverse or in-order).</p>
</div>
<div class="sws-slide">
-<h1>Pattern matching semantics (v/p)</h1>
+<h1>Pattern matching semantics (simplified)</h1>
<pre style="text-align:center;">
- σ; δ ⊢ v / p &rleadsto; γ, σ'
+ σ ⊢ v / p &rleadsto; γ, σ'
</pre>
<p style="font-size:90%"><dfn><u>σ</u>, <u>σ'</u></dfn>: mapping from accumulators to
values<br/>
<dfn><u>p</u></dfn>: pattern<br/>
<dfn><u>γ</u></dfn>: mapping from capture variables to
values<br/>
- <dfn><u>δ</u></dfn>: current context
</p>
-<div style="padding:0em 1em 0em; text-align:justify;font-size:85%;background:white;">
+<div style="padding:0em 1em 0em; text-align:justify;background:white;">
<div class="infer">
<span> v ∈ [ t ]</span>
<span>σ; δ ⊢ v / t &rleadsto; ∅,
<div class="infer">
<span></span>
- <span>σ; δ ⊢ v / ẋ &rleadsto; ∅,
- σ[ ẋ := Op(ẋ) (v<sub>δ</sub>, σ(ẋ)) ]</span>
+ <span>σ ⊢ v / ẋ &rleadsto; ∅,
+ σ[ ẋ := Op(ẋ) (v, σ(ẋ)) ]</span>
</div><span>(acc)</span>
<div class="infer">
<span></span>
- <span>σ; δ ⊢ v / x &rleadsto; { x ↦ v },
+ <span>σ ⊢ v / x &rleadsto; { x ↦ v },
σ</span>
</div><span>(var)</span>
<div class="infer">
- <span>σ; &left;v · δ ⊢ (fst v)/p<sub>1</sub>
+ <span>σ ⊢ (fst v)/p<sub>1</sub>
&rleadsto; γ<sub>1</sub>, σ' </span>
- <span>σ'; &right;v · δ ⊢ (snd v)/p<sub>2</sub>
+ <span>σ' ⊢ (snd v)/p<sub>2</sub>
&rleadsto; γ<sub>2</sub>, σ''
</span>
- <span>σ; δ ⊢ v /
+ <span>σ ⊢ v /
(p<sub>1</sub>, p<sub>2</sub>) &rleadsto;
γ<sub>1</sub>∪ γ<sub>2</sub>,
σ''</span>
</div><span>(pair)</span> <span class="fill"></span>
-<span>… and some other rules for alternation, failure, recursion, <i>etc.</i></span>
+<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/>
+(some other rules for alternation, failure, recursion, <i>etc.</i>)</span>
</div>
</div>
<div class="sws-slide">
</div>
<div class="sws-slide">
<h1>Results</h1>
-<p>Zippers (in values, types, patterns) are orthogonal to the rest of the language</p>
+<p>Zippers (in values, types, patterns) are a conservative extension</p>
<ul>
<li><u>Subtyping and typechecking</u> are extended straightforwardly</li>
<li>Typing of patterns introduces <u>sound approximations</u> only for accumulators</li>
</code>
<pre class="sws-pause">
- <tt>descendant-or-self::</tt> t ≡ X ≡ ((ẋ <tt>&</tt> t | _ ) <tt> & <_>[</tt> X <tt>* ]</tt>)<sub>&ztop;</sub>
+ <tt>descendant-or-self::</tt> t ≡ X ≡ ((ẋ <tt>&</tt> t | _ ) <tt> & </tt> (<tt><_>[</tt> X <tt>* ]</tt>)<sub>&ztop;</sub> | _ )
<tt>descendant</tt> :: t ≡ <tt><_>[ (descendant-or-self::</tt>t<tt>)* ]</tt><sub>&ztop;</sub>
</pre>
</pre>
<pre style="position:absolute;bottom:5%;z-index:2;">
- <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>
+ <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>
- <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>
+ <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>
<h1>Other results</h1>
<ul>
<li>Encoding of paths is compositional</li>
- <li>Once we have path, translation from XQuery to &cduce; is straightforward</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>
</ul>
</div>
<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>Extend the approach to Json (google ``path language for json´´), i.e. generalise from products to extensible records</li>
</ul>
-
+<p class="sws-pause" style="text-align:center;"><b><u>Thank you!</u></b></p>
</div>
</body>
projects / hacks / simpleWebSlides.git / commitdiff