X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=pres-esop15%2F01.xhtml;h=d74a138f9aa51439db6ede4a8f36c5566ff6e5b1;hb=564cbcc2c27a723d2bdf12cf690a66eb7f36b813;hp=6a41862198f612ce45c0308b66e0e81d442554a7;hpb=710c794a4411203cc3d668911a869cae0923b954;p=hacks%2FsimpleWebSlides.git diff --git a/pres-esop15/01.xhtml b/pres-esop15/01.xhtml index 6a41862..d74a138 100644 --- a/pres-esop15/01.xhtml +++ b/pres-esop15/01.xhtml @@ -14,8 +14,8 @@ - - + Empty" > + Any" > @@ -196,25 +196,25 @@

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
    • @@ -306,8 +307,8 @@

    &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
@@ -340,12 +341,16 @@ t ≤ s   &Lrarrow;   [t] ⊆  [s]

    &cduce; data-model

    -

    The usual sets of values: constants, λ-abstractions, pairs, …

    -

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

    +

    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

    @@ -374,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. @@ -396,7 +401,7 @@ t ≤ s &Lrarrow; [t] ⊆ [s]
      6. Introduced in 1997 by Gérard Huet
      7. Stack of visited nodes
      8. Push the current node on the stack when traversing a pair
        9. -
      9. Take top of the stack to go backward
        10. +
      10. Take the top of the stack to go backward
      11. Tag the elements of the stack to remember which component of a pair we have visited
        12. @@ -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 returns the head of the zipper: 
        
-
            up v3 ≡ v2 ≡ (2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; 
+
              up v3 ≡ v2 ≡ (2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc;
    @@ -431,22 +436,19 @@ t ≤ s &Lrarrow; [t] ⊆ [s] integers that are the leftmost descendant of a tree

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

    - [ … ]]]>(&right; ⊤) · &ztop; types of links in any context - + [ … ]]]> &ztop; types of links nested in any context

    Tree navigation

    Since patterns contain types, we can check complex conditions:

    -
      Has a descendant <a>_:
-    p ≡ <a>_   &lor;   <_>[ _* p _* ]
+
       Has a descendant <a>_:
+     p ≡ <a>_   &lor;   <_>[ _* p _* ]
  
   Deos not have an ancestor <b>_:
-    τ ≡ &bcirc;   &lor;   &right;(⊤∖ <b>_) · τ   &lor;   &left;(⊤∖ <b>_) · τ 
-
-
    
+    τ ≡ &bcirc;   &lor;   &right;(⊤∖ <b>_) · τ   &lor;   &left;(⊤∖ <b>_) · τ
    match v with pτ & x &rarrow; … @@ -480,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''))
    
@@ -490,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; ∅, @@ -511,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.)
    @@ -564,25 +566,13 @@ 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
    • Provided the operators are sound, the whole language remains type-safe
    -
    -

    From zippers to XPath

    -

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

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

    rb_tree

    -

    Downward XPath axes

         self :: t ≡    (ẋ & t | _ )&ztop;                                (Init(ẋ) = [], Op(ẋ) = snoc)
@@ -597,7 +587,7 @@ which is not a type.
    
     
 
 
    -     descendant-or-self:: t ≡   X ≡ ((ẋ & t | _ )  & <_>[ X * ])&ztop;
+     descendant-or-self:: t ≡   X ≡ ((ẋ & t | _ )  &  (<_>[ X * ])&ztop; | _ )
 
      descendant :: t ≡ <_>[ (descendant-or-self::t)* ]&ztop;
 
    
@@ -641,6 +631,19 @@ which is not a type.
    
 
 -->
    +
    +

    Binary-tree encoding

    +

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

    + [ [ + [] + [] + [ [] ] + ] + ]]]> +ex_ntree
    +

    rb_tree

    +
    +

    Upward XPath axes

    @@ -660,9 +663,9 @@ which is not a type.

     
-                               ⬆ ⬆     ⬆     ⬆
+                                  ⬆ ⬆     ⬆     ⬆
 
-                                                   parent         
+                                                    parent         
 
 
 
@@ -672,21 +675,26 @@ which is not a type.
    
   
    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!