X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=pres-esop15%2F01.xhtml;h=d74a138f9aa51439db6ede4a8f36c5566ff6e5b1;hb=564cbcc2c27a723d2bdf12cf690a66eb7f36b813;hp=845513e7568c65d663f0afa0221547d9bbcd7236;hpb=6306d8f84361082e8e5cb250f0d503e26d04b23f;p=hacks%2FsimpleWebSlides.git diff --git a/pres-esop15/01.xhtml b/pres-esop15/01.xhtml index 845513e..d74a138 100644 --- a/pres-esop15/01.xhtml +++ b/pres-esop15/01.xhtml @@ -14,8 +14,8 @@ - - + Empty" > + Any" > @@ -189,32 +189,32 @@

- CNRS, PPS, Université Paris-Diderot, Paris, France
- Kangwon National University, Chuncheon, Rep. of Korea
- LRI, Université Paris-Sud, Orsay, France + 1 CNRS, PPS, Université Paris-Diderot, Paris, France
+ 2 Kangwon National University, Chuncheon, Rep. of Korea
+ 3 LRI, Université Paris-Sud, Orsay, France

XQuery 3.0

-

W3C standard language for querying XML - databases/documents

- +

W3C standard to query XML documents

+ declare function get_links($page, $print) { - for $i in $page/descendant::a[not(ancestor::b)] - return print($i) + return $print($i) } declare function pretty($link) { typeswitch($link) - case $l as element(a) - return switch ($l/@class) - case "style1" + case $l as element(a) + return switch ($l/@class) + case "style1" return <a href={$l/@href}><b>{$l/text()}</b></a> - default return $l + default return $l - default return $link + default return $link } + + let $bold_links := get_links(document("file.xhtml"), $pretty)
@@ -279,7 +280,7 @@ + compact (and efficient) type and value pattern-matching
  • Cons
    - - complex navigation encoded through recursion + - complex navigation encoded through explicit recursion
    - no type inference for functions
    • @@ -290,44 +291,40 @@
    1. Add support for path navigation to &cduce; -

    &cduce;'s type algebra

    -
    -    t ::=  b  |  c  |  t × t  |  t &rarrow; t  |  t &lor; t  |  t  &land; t  |  t ∖ t  |  ⊤  |  ⊥  |  α
+
    A set &mathT; of types
    
+
        t ::=  b  |  c  |  t × t  |  t &rarrow; t  |  t &lor; t  |  t  &land; t  |  t ∖ t  |  ⊤  |  ⊥  |  α
 
    
 
    b : ranges over basic types (Int, String, …)
    
    c : ranges over singleton types
    (`A, 42, …)
    
+   Type constructors 
    
+   Boolean connectives 
    
    α : type variables
    
-   types are interpreted co-inductively (recursive types) and regular
+   types are interpreted co-inductively: recursive types and regular
    expression types
    
 
    
-
    -    t1 ≡ (Int × t1) &lor; t2
-    t2 ≡ (Bool × t2) &lor; (Bool × `nil)
-
-    t1 ≡ [ Int* Bool+ ]
-
+
    
+
          t1 ≡ (Int × t1)    &lor;    t2
+      t2 ≡ (Bool × t2)  &lor; (Bool × `nil)
 
    
+
     t1 ≡ [ Int* Bool+ ]
    
+

    Semantic subtyping

    @@ -342,11 +339,27 @@ t ≤ s &Lrarrow; [t] ⊆ [s] [ Int* (Int | Bool*)? ] &land; [ Int+ (Bool+ | Int)* ] ≡ [Int+ Bool*]
    +
    +

    &cduce; data-model

    +

    The usual sets &mathV; of values:

    +
           v ::= 1  |  …  |  `Foo  |   (v, v)  |  λx.e
+
    +

    Sequences are nested pairs (à la Lisp):

    +
    [ v1  … vn ] ≡ (v1, (…, (vn, `nil)))
+
    +

    XML documents are tagged sequences: 

    <foo>[ v1  … vn ] ≡ (`foo, [ v1  … vn ])
    +

    +

    (Sometimes we write [ ] for the variant `nil)

    +

    Everything is built on top of products and variants

    +

    &cduce; patterns

    -
        p ::=  t  |  p | p  |  p & p  | (p, p) |  x
    +

    (a.k.a. the left-hand side of an arrow in a match … with)

    +
        p ::=  t  | x | (p, p) |  p | p  |  p & p

    t ranges over types
    x ranges over capture variables
    + Pair patterns
    + Alternation |, Intersection &
    patterns are also co-inductively interpreted (recursive patterns)

    v / p : matching a value against a pattern yields a @@ -366,14 +379,14 @@ t ≤ s &Lrarrow; [t] ⊆ [s] | [ _* (x & Int) ] &rarrow; (x, `false) | [ ] &rarrow; (0, `false) -

      -
    1. &lbag;[ _* (x & Int) Bool* (y & Bool) ]&rbag; ≡ [ ⊤* Int Bool+ ]
      - yield : { x ↦ Int, y ↦ Bool } +
        +
      1. &lbag;[ _* (x & Int) Bool* (y & Bool) ]&rbag; ≡ [ ⊤* Int Bool+ ]
        + { x ↦ Int, y ↦ Bool }
        2. -
      2. &lbag;[ _* (x & Int) ]&rbag; ≡ [ ⊤* Int ]
        - yield : { x ↦ Int } +
      3. &lbag;[ _* (x & Int) ]&rbag; ≡ [ ⊤* Int ]
        + { x ↦ Int }
        4. -
      4. Since [Int+ Bool* ] ∖ ( [ ⊤* Int Bool+ ] &lor; [ ⊤* Int]) ≡ ⊥ +
      5. Since [Int+ Bool* ] ∖ ( [ ⊤* Int Bool+ ] &lor; [ ⊤* Int]) ≡ ⊥
        the third case is unreachable.
        6. @@ -381,24 +394,16 @@ t ≤ s &Lrarrow; [t] ⊆ [s]
    -
    -

    &cduce; data-model

    -

    Sequences are nested pairs: [ v1 … vn ] ≡ (v1, (…, (vn, `nil))) -

    -

    XML documents are tagged sequences: 

    <foo>[ v1  … vn ] ≡ (`foo, [ v1  … vn ])
    -

    -

    Ususal lisp-like encoding of trees, how to perform navigation - (including upward ?)

    -
    +

    Zippers (1/2)

     v ::=  …  |  vδ
  δ ::=  &bcirc;  | &left;v · δ | &right;v · δ
@@ -409,13 +414,13 @@ t ≤ s   &Lrarrow;   [t] ⊆  [s]
 
    Zippers (2/2)
    
 
    fst (resp. snd) takes the first (resp. second)
   projection of a pair and update its zipper accordingly:
    
-
        v1 ≡ (1, (2, (3, (4, `nil))))&bcirc;
-    v11 ≡ fst v1 ≡ 1&left;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; 
-    v2 ≡ snd v1 ≡ (2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; 
-    v3 ≡ snd v2 ≡ (3, (4, `nil))&right;v2 · &right;v1 · &bcirc; 
+
          v1 ≡ (1, (2, (3, (4, `nil))))&bcirc;
+      v11 ≡ fst v1 ≡ 1&left;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; 
+      v2 ≡ snd v1 ≡ (2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; 
+      v3 ≡ snd v2 ≡ (3, (4, `nil))&right;v2 · &right;v1 · &bcirc; 
 
    
-
    up pops returns the head of the zipper: 
    
-
        up v3 ≡ v2 ≡ (2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; 
+
    up returns the head of the zipper: 
    
+
          up v3 ≡ v2 ≡ (2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc;
    @@ -424,47 +429,39 @@ t ≤ s &Lrarrow; [t] ⊆ [s] 
     t ::=  …  |  tτ
  τ ::=  &bcirc;  |  &left;t · τ  | &right;t · τ  |  τ &lor; τ  |  τ ∖ τ  |  &ztop;
    -

    &bcirc;: singleton type denoting the empty zipper
    - &ztop;: the top zipper types
    - Zipper types are interpreted co-inductively (regular expressions on - zippers)

    - Int(&left;⊤)* &bcirc;: type of - integers that are the leftmost descendant of a tree.
    - [ […] […] ]]]>&bcirc;: type of - HTML documents
    - [ … ]]]>&ztop;: types of links in any context - +

    &bcirc;: singleton type denoting the empty zipper (root element)
    + &ztop;: the top zipper type
    + Zipper types are interpreted co-inductively

    + Int(&left;⊤)* &bcirc; type of + integers that are the leftmost descendant of a tree

    + [ […] […] ]]]>&bcirc; type of + HTML documents

    + [ … ]]]> &ztop; types of links nested in any context

    Tree navigation

    Since patterns contain types, we can check complex conditions:

    -
    -    p ≡ <a>_   &lor;   <_>[ _* p _* ]
+
       Has a descendant <a>_:
+     p ≡ <a>_   &lor;   <_>[ _* p _* ]
  
-    τ ≡ &bcirc;   &lor;   &right;⊤ · τ   &lor;   &left;(⊤∖ <b>_) · τ 
-
-
    
+  Deos not have an ancestor <b>_:
+    τ ≡ &bcirc;   &lor;   &right;(⊤∖ <b>_) · τ   &lor;   &left;(⊤∖ <b>_) · τ
    match v with pτ & x &rarrow; … - | _ &rarrow; … - -

    -We want more, namely return all descendants (ancestor, + | _ &rarrow; … +

    We want more, namely return all descendants (ancestors, children, siblings, …) of a node matching a particular condition

    Remark: (recursive) patterns already perform a recursive traversal of the value -

    +
    Idea: Piggy back on the traversal and accumulate nodes in special variables

    -

    Operators and Accumulators

    @@ -485,7 +482,7 @@ nodes in special variables

    Some operators

    - 
    +  
         v, v' &rleadsto;cons, (v, v') 
    
     v, `nil &rleadsto;snoc (v, `nil)
    
     v, (v',v'') &rleadsto;snoc (v', snoc(v,v''))
    
@@ -495,19 +492,18 @@ nodes in special variables
   accumulates that node in sequence (in reverse or in-order).
    -

    Pattern matching semantics (v/p)

    +

    Pattern matching semantics (simplified)

    -  σ; δ ⊢ v / p &rleadsto; γ, σ'
+  σ ⊢ v / p &rleadsto; γ, σ'

    σ, σ': mapping from accumulators to - values
    + values.   Initially: σ = { ẋ ↦ Init(ẋ) | ẋ ∈ p }
    v: input value
    p: pattern
    γ: mapping from capture variables to values
    - δ: current context

    -
    +
    v ∈ [ t ] σ; δ ⊢ v / t &rleadsto; ∅, @@ -516,28 +512,29 @@ nodes in special variables
    - σ; δ ⊢ v / ẋ &rleadsto; ∅, - σ[ ẋ := Op(ẋ) (vδ, σ(ẋ)) ] + σ ⊢ v / ẋ &rleadsto; ∅, + σ[ ẋ := Op(ẋ) (v, σ(ẋ)) ]
    (acc)
    - σ; δ ⊢ v / x &rleadsto; { x ↦ v }, + σ ⊢ v / x &rleadsto; { x ↦ v }, σ
    (var)
    - σ; &left;v · δ ⊢ (fst v)/p1 + σ ⊢ (fst v)/p1 &rleadsto; γ1, σ' - σ'; &right;v · δ ⊢ (snd v)/p2 + σ' ⊢ (snd v)/p2 &rleadsto; γ2, σ'' - σ; δ ⊢ v / + σ ⊢ v / (p1, p2) &rleadsto; γ1∪ γ2, σ''
    (pair) -… and some other rules for alternation, failure, recursion, etc. +Remember, if v ≡ (v1,v2)δ then fst v ≡ v1 &left;v · δ and snd v ≡ v2 &right;v · δ
    +(some other rules for alternation, failure, recursion, etc.)
    @@ -569,7 +566,7 @@ which is not a type.

    Results

    -

    Zippers (in values, types, patterns) are orthogonal to the rest of the language

    +

    Zippers (in values, types, patterns) are a conservative extension

    • Subtyping and typechecking are extended straightforwardly
    • Typing of patterns introduces sound approximations only for accumulators
      • @@ -577,25 +574,21 @@ which is not a type.

    -

    From zippers to XPath

    -

    We use regular expressions over basic &left;/&right; zippers to encode XPath

    - [ [ - [] - [] - [ [] ] - ] - ]]]> -ex_ntree
    -

    rb_tree

    -
    -
    -

    Downward axes

    - [ [ [] [] [ [] ] ] ]]]>&bcirc; - -
    -     self :: t ≡    (ẋ & t | _ )&ztop;
-     child :: t ≡  <_>[ (ẋ & t | _ )* ]&ztop;
-     descendant-or-self:: t ≡   X ≡ ((ẋ & t | _ )  & <_>[ X * ])&ztop;
+
    Downward XPath axes
    
+
         self :: t ≡    (ẋ & t | _ )&ztop;                                (Init(ẋ) = [], Op(ẋ) = snoc)
+
+     child :: t ≡  <_>[ (ẋ & t | _ )* ]&ztop;
+
    
+
    Example: applying child::<b>_   to the document
    
+      <doc>[ <a>[]    <b>[]    <c>[]    <b>[] ]&bcirc;
+        <_>[   _    (ẋ & <b>_)   _     (ẋ & <b>_)]&ztop;
+
+         ẋ↦ [ <b>[]&left;… &right;… &right;… &bcirc;    <b>[]&left;… &right;… &right;… &right;… &right;… &bcirc;   ] 
+
+
+
    +     descendant-or-self:: t ≡   X ≡ ((ẋ & t | _ )  &  (<_>[ X * ])&ztop; | _ )
+
      descendant :: t ≡ <_>[ (descendant-or-self::t)* ]&ztop;
 
    
 
 
 
    
-
    Upward axes
    
-  [ [  []  [] [  [] ]   ]  ]]]>&bcirc;
-
-
    -     parent :: t ≡   ⊤ (&left;_) · (&right;_)* · (&right; ẋ & t) · (( (&left; _) · &ztop;)  &lor;  &bcirc; )
-     ancestor :: t ≡   ⊤ ((&left;_) · (&right;_)* · (&right; ẋ & t))* · &bcirc; 
+  
    Binary-tree encoding
    
+  
    We use  regular expressions over basic &left;/&right; zippers to encode upward XPath
    
+   [ [
+          []
+          []
+          [  [] ]
+        ]
+   ]]]>
+ex_ntree
    
+
    rb_tree
    
+
+
+
    
+
    Upward XPath axes
    
+
    
+
+
+
+
+
+
+
         parent :: t ≡   ⊤ (&left;_) · (&right;_)* · (&right; ẋ & t) · (( (&left; _) · &ztop;)  &lor;  &bcirc; )
+                                             
+     ancestor :: t ≡   ⊤ ( (&left;_) · (&right;_)* · (&right; ẋ & t) )* · &bcirc; 
+
+
+
+
+
    
+
    +
+                                  ⬆ ⬆     ⬆     ⬆
+
+                                                    parent         
+
+
+
 
    
 
 
    
   
    Other results
    
 
      
   
    • Encoding of paths is compositional
      • 
-  
    • Once we have path, translation from XQuery to &cduce; is straightforward
      • 
+  
    • Once we have paths, translation from XQuery to &cduce; is straightforward
      • 
   
    • We also give a direct typing algorithm for XQuery 3.0 rather than typing the translation to &cduce;
      • 
+  
    • Accumulators in patterns allow to encode other XPath constructs (count(), position(), …)
      • 
+
    
+
    Still some problems in the on-going implementation
    
+
      
+  
    • Nice syntax to expose paths + patterns to the programmer
      • 
+  
    • Pretty printing of error messages: décompilation of regular expressions
      • 
 
    
 
    
 
    
 
    Conclusion, thoughts and future work
    
 
      
-  
    • Adding path expressions to a functional language such as &cduce; is possible 
      • 
-  
    • Semantic subtyping and regular expression types play nicely with zippers
      • 
-  
    • In terms of language design, exposing directly zippers patterns to the programmer is a big no-no
      • 
-  
    • Can also be applied to XSLT
      • 
-  
    • Implementation on-going (including a &cduce; to javascript backend)
      • 
-  
    • Extend the approach to Json (google ``path language for json''), i.e. generalise from products to extensible records
      • 
+  
    • Adding path expressions to a functional language such as &cduce; is possible 
      • 
+  
    • Semantic subtyping and regular expression types play nicely with zippers
      • 
+  
    • In terms of language design, exposing directly zippers to the programmer (still need work at the syntax level)
      • 
+  
    • Implementation on-going (including a &cduce; to javascript backend)
      • 
+  
    • Extend the approach to Json (google ``path language for json´´), i.e. generalize from products to extensible records
      • 
 
    
-
+
    Thank you!