</table>
</div>
<p style="font-size:80%;position:absolute;bottom:2.5em;left:4em;">
- CNRS, PPS, Université Paris-Diderot, Paris, France <br/>
- Kangwon National University, Chuncheon, Rep. of Korea<br/>
- LRI, Université Paris-Sud, Orsay, France
+ 1 CNRS, PPS, Université Paris-Diderot, Paris, France <br/>
+ 2 Kangwon National University, Chuncheon, Rep. of Korea<br/>
+ 3 LRI, Université Paris-Sud, Orsay, France
</p>
</div>
<div class="sws-slide">
+ compact (and efficient) type and value pattern-matching
</li>
<li>Cons<br/>
- - <s>complex navigation encoded through recursion</s>
+ - <s>complex navigation encoded through recursion</s><br/>
- no type inference for functions
</li>
</ul>
<ol style="margin-left:1em; margin-right:0.25em;list-style-position:inside;">
<li id="tobox" style="padding:1em 0em 1em 0em;"><span class="lh">Add support for path navigation to
&cduce;</span>
- <ul id="toshow" style="margin-top:2em;display:none;">
+ <ul style="margin-top:2em;">
<li>Enrich the type algebra with <em>zippers</em> (à la Huet)</li>
<li>Extend pattern-matching construct to <em>zipped values and types</em></li>
<li>Encode path expressions as recursive patterns</li>
</ul>
</li>
- <li style="padding:1em 0em 1em 0em;">Perform a type-directed translation from XQuery to
+ <li class="ll" style="padding:1em 0em 1em 0em;">Perform a type-directed translation from XQuery to
&cduce;</li>
-
</ol>
<script type="text/javascript">
- reg ("0", col_change(".lh",""));
- reg ("1", col_change(".lh", "#f80"));
-
- reg ("2", function (canvas) { $("#toshow").show(); });
- reg ("3", function (c) { $("#tobox").css (
- { 'background' : '#dfd', 'border-radius': '1em' });});
+ reg (1, col_change(".lh", "#f83"));
+ reg (1, col_change(".ll", "#bbb"));
</script>
</div>
<div class="sws-slide">
<h1>&cduce;'s type algebra</h1>
<pre>
- t ::= b | c | t × t | t &rarrow; t | t &lor; t | t &land; t | t ∖ t | ⊤ | ⊥ | α
+ 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
(<tt>`A</tt>, <tt>42</tt>, …)<br/>
+ <u>Type constructors</u> <br/>
+ <mark>Boolean connectives</mark> <br/>
<dfn>α</dfn> : type variables<br/>
- types are interpreted co-inductively (recursive types) and regular
+ types are interpreted co-inductively: recursive types and regular
expression types<br/>
</p>
-<pre>
- t<sub>1</sub> ≡ (<tt>Int</tt> × t<sub>1</sub>) &lor; t<sub>2</sub>
- t<sub>2</sub> ≡ (<tt>Bool</tt> × t<sub>2</sub>) &lor; (<tt>Bool</tt> × <tt>`nil</tt>)
-
- <span class="sws-pause">t<sub>1</sub> ≡ <tt>[ Int* Bool+ ]</tt></span>
-
+<div style="vertical-align:top;">
+<pre style="width:50%;display:inline-block;"> t<sub>1</sub> ≡ (<tt>Int</tt> × t<sub>1</sub>) &lor; t<sub>2</sub>
+ t<sub>2</sub> ≡ (<tt>Bool</tt> × t<sub>2</sub>) &lor; (<tt>Bool</tt> × <tt>`nil</tt>)
</pre>
+<pre style="width:30%;display:inline-block;"> <span class="sws-pause">t<sub>1</sub> ≡ <tt>[ Int* Bool+ ]</tt></span></pre>
+</div>
</div>
<div class="sws-slide">
<h1>Semantic subtyping</h1>
<tt>[ Int* (Int | Bool*)? ]</tt> &land; <tt>[ Int+ (Bool+ | Int)* ]</tt> ≡ <tt>[Int+ Bool*]</tt>
</pre>
</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>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>
+</div>
<div class="sws-slide">
<h1>&cduce; patterns</h1>
-<pre style="text-align:center;"> p ::= t | p | p | p & p | (p, p) | x </pre>
+<p><i>(a.k.a. the left-hand side of an arrow in a match … with)</i></p>
+<pre style="text-align:center;"> p ::= t | x | <u>(p, p)</u> | <mark>p | p</mark> | <mark>p & p</mark> </pre>
<p><dfn>t</dfn> ranges over types<br/>
<dfn>x</dfn> ranges over capture variables<br/>
+ <u>Pair patterns</u><br/>
+ <mark> Alternation |, Intersection &</mark><br/>
patterns are also co-inductively interpreted (recursive patterns)
</p>
<p><dfn><u>v / p</u></dfn> : matching a value against a pattern yields a
</ol>
</div>
-<div class="sws-slide">
-<h1>&cduce; data-model</h1>
-<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>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>Ususal lisp-like encoding of trees, how to perform navigation
- (including upward ?)</p>
-</div>
+
<div class="sws-slide">
<h1>Zippers (1/2)</h1>
<ul>
<li>Introduced in 1997 by Gérard Huet</li>
- <li>Stack of visited</li>
- <li>Push the current node on the stack when descending</li>
- <li>Put the top of the stack and pop it to go backward</li>
- <li>Tag the elements of the stack to remember which of a node we
- have visited</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>Tag the elements of the stack to remember which component of a
+ pair we have visited</li>
</ul>
<pre style="text-align:center;"> v ::= … | v<sub>δ</sub>
δ ::= &bcirc; | &left;v · δ | &right;v · δ
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>
</pre>
-<p><tt><u>up</u></tt> pops returns the head of the zipper: </p>
+<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>
</div>
<pre style="text-align:center;"> t ::= … | t<sub>τ</sub>
τ ::= &bcirc; | &left;t · τ | &right;t · τ | τ &lor; τ | τ ∖ τ | &ztop;
</pre>
-<p><dfn>&bcirc;</dfn>: singleton type denoting the empty zipper<br/>
- <dfn>&ztop;</dfn>: the top zipper types<br/>
- Zipper types are interpreted co-inductively (regular expressions on
- zippers)<br/><br/>
- <dfn><tt>Int</tt><sub>(&left;⊤)* &bcirc;</sub></dfn>: type of
- integers that are the leftmost descendant of a tree.<br/>
- <dfn><tt><![CDATA[<html>[ <head>[…] <body>[…] ]]]></tt><sub>&bcirc;</sub></dfn>: type of
- HTML documents<br/>
- <dfn><tt><![CDATA[<a href=String>[ … ]]]></tt><sub>&ztop;</sub></dfn>: types of links in any context
+<p><dfn>&bcirc;</dfn>: singleton type denoting the empty zipper (root element)<br/>
+ <dfn>&ztop;</dfn>: the top zipper type<br/>
+ Zipper types are interpreted co-inductively<br/><br/>
+ <dfn><tt>Int</tt><sub>(&left;⊤)* &bcirc;</sub></dfn> <span style="float:right;">type of
+ 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>
</p>
</div>
<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 0pt; border-style:dashed;border-color: black;vertical-align:middle">
+<pre style="width:60%;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>
- τ ≡ &bcirc; &lor; &right;⊤ · τ &lor; &left;(⊤∖ <tt><b>_</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>
<code style="width:20%;display:inline-block;vertical-align:middle">
match <u>v</u> with
<dfn>p<sub>τ</sub></dfn> & <u>x</u> &rarrow; …
- | _ &rarrow; …
-</code>
-<p style="background:white">
-We want more, namely return <i>all</i> descendants (ancestor,
+ | _ &rarrow; …</code>
+<p style="background:white">We want more, namely return <i>all</i> descendants (ancestors,
children, siblings, …) of a node matching a particular condition
<br/><br/>
Remark: (recursive) patterns <u>already perform a recursive traversal
of the value</u>
-<br/><br/>
+<br/>
<em>Idea</em>: Piggy back on the traversal and <em>accumulate</em>
nodes in special variables
</p>
-<script type="text/javascript">
- reg (0, col_change ("#test", ""));
- reg (1, col_change ("#test", "orange"));
-</script>
</div>
<div class="sws-slide">
<h1>Operators and Accumulators</h1>
<p class="sws-pause"><img style="margin-top:-1em;margin-left:5%;width:85%;" src="rb_tree.svg" alt="rb_tree"/></p>
</div>
<div class="sws-slide">
-<h1>Downward axes</h1>
-<tt> <![CDATA[<a>[ <b>[ <c>[] <d>[] <e>[ <f> [] ] ] ]]]><sub>&bcirc;</sub></tt>
-<object id="svgRBTree" data="rb_tree.svg" type="image/svg+xml" style="margin-left:7.5%;width:85%" />
-<pre>
- <tt>self ::</tt> t ≡ (ẋ <tt>&</tt> t | _ )<sub>&ztop;</sub>
- <tt>child ::</tt> t ≡ <tt><_>[</tt> (ẋ <tt>&</tt> t | _ )<tt>* ]</tt><sub>&ztop;</sub>
+<h1>Downward XPath axes</h1>
+<pre style="background:white"> <tt>self ::</tt> t ≡ (ẋ <tt>&</tt> t | _ )<sub>&ztop;</sub> (Init(ẋ) = [], Op(ẋ) = <tt>snoc</tt>)
+
+ <span class="sws-pause"><tt>child ::</tt> t ≡ <tt><_>[</tt> (ẋ <tt>&</tt> t | _ )<tt>* ]</tt><sub>&ztop;</sub></span>
+</pre>
+<p class="sws-pause">Example: applying <tt><u>child::<b>_</u></tt> to the document</p>
+<code> <doc>[ <a>[] <b>[] <c>[] <b>[] ]<sub>&bcirc;</sub>
+ <span class="sws-pause"><_>[ <span class="sws-pause"> _</span> <mark class="sws-pause">(ẋ & <b>_)</mark> <span>_</span> <mark>(ẋ & <b>_)</mark>]<sub >&ztop;</sub></span>
+
+ <span class="sws-pause"> ẋ↦ [ <b>[]<sub>&left;… &right;… &right;… &bcirc;</sub> <b>[]<sub>&left;… &right;… &right;… &right;… &right;… &bcirc;</sub> ] </span>
+</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</tt> :: t ≡ <tt><_>[ (descendant-or-self::</tt>t<tt>)* ]</tt><sub>&ztop;</sub>
</pre>
<!--
-->
</div>
<div class="sws-slide">
-<h1>Upward axes</h1>
-<tt> <![CDATA[<a>[ <b>[ <c>[] <d>[] <e>[ <f> [] ] ] ]]]><sub>&bcirc;</sub></tt>
-<object id="svgRBTree" data="rb_tree.svg" type="image/svg+xml" style="margin-left:7.5%;width:85%" />
-<pre>
- <tt>parent ::</tt> t ≡ ⊤<sub> (&left;_) · (&right;_)* · (&right; ẋ & t) · (( (&left; _) · &ztop;) &lor; &bcirc; )</sub>
- <tt>ancestor ::</tt> t ≡ ⊤<sub> ((&left;_) · (&right;_)* · (&right; ẋ & t))* · &bcirc; </sub>
+<h1>Upward XPath axes</h1>
+<div style="position:absolute; width:80%; left:10%;top:15%">
+<object id="svgRBTree" data="rb_tree.svg" type="image/svg+xml" style="z-index:1;position:absolute;width:100%" />
+<object class="sws-onframe-1" id="svgRBTree1" data="rb_tree01.svg" type="image/svg+xml" style="z-index:1;position:absolute;width:100%" />
+<object class="sws-onframe-2" id="svgRBTree2" data="rb_tree02.svg" type="image/svg+xml" style="z-index:3;position:absolute;width:100%" />
+<object class="sws-onframe-3" id="svgRBTree3" data="rb_tree03.svg" type="image/svg+xml" style="z-index:4;position:absolute;width:100%" />
+<object class="sws-onframe-4" id="svgRBTree4" data="rb_tree04.svg" type="image/svg+xml" style="z-index:5;position:absolute;width:100%" />
+</div>
+<pre style="position:absolute;bottom:5%;z-index:1;"> <tt>parent ::</tt> t ≡ ⊤<sub> (&left;_) · (&right;_)* · (&right; ẋ & t) · (( (&left; _) · &ztop;) &lor; &bcirc; )</sub>
+
+<span class="sws-onframe-5"> <tt>ancestor ::</tt> t ≡ ⊤<sub> ( (&left;_) · (&right;_)* · (&right; ẋ & t) )* · &bcirc; </sub></span>
+
+
+
+
+</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 style="color:#1fb01b;border-color:#1fb01b;border-top-style:dashed;border-top-width:3pt;position:relative;top:0.5em;"> parent </span>
+
+
+
</pre>
</div>
<div class="sws-slide">
projects / hacks / simpleWebSlides.git / blobdiff