From f731bd2558865c08d22c2bee90339ef304937c02 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Tue, 14 Apr 2015 09:09:33 +0200 Subject: [PATCH] Final version of esop talk. --- pres-esop15/01.xhtml | 127 ++++++++++++++++++++++--------------------- 1 file changed, 65 insertions(+), 62 deletions(-) diff --git a/pres-esop15/01.xhtml b/pres-esop15/01.xhtml index 6d2dee3..e1e432e 100644 --- a/pres-esop15/01.xhtml +++ b/pres-esop15/01.xhtml @@ -14,8 +14,8 @@ - - + Empty" > + Any" > @@ -195,12 +195,10 @@

-

XQuery 3.0

-

W3C standard language for querying XML - databases/documents

- - declare function get_links($page, $print) { +

The XQuery 3.0 W3C Standard

+ + declare function get_links($page, $print) { for $i in $page/descendant::a[not(ancestor::b)] return print($i) } @@ -215,6 +213,8 @@ default return $link } + + let $bold_links := get_links(document("file.html"), $pretty)
@@ -306,8 +308,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 +342,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

@@ -375,13 +381,13 @@ t ≤ s &Lrarrow; [t] ⊆ [s] | [ ] &rarrow; (0, `false)
    -
  1. &lbag;[ _* (x & Int) Bool* (y & Bool) ]&rbag; ≡ [ ⊤* Int Bool+ ]
    - yield : { x ↦ Int, y ↦ Bool } +
  2. &lbag;[ _* (x & Int) Bool* (y & Bool) ]&rbag; ≡ [ ⊤* Int Bool+ ]
    + { x ↦ Int, y ↦ Bool }
    3. -
  3. &lbag;[ _* (x & Int) ]&rbag; ≡ [ ⊤* Int ]
    - yield : { x ↦ Int } +
  4. &lbag;[ _* (x & Int) ]&rbag; ≡ [ ⊤* Int ]
    + { x ↦ Int }
    5. -
  5. Since [Int+ Bool* ] ∖ ( [ ⊤* Int Bool+ ] &lor; [ ⊤* Int]) ≡ ⊥ +
  6. Since [Int+ Bool* ] ∖ ( [ ⊤* Int Bool+ ] &lor; [ ⊤* Int]) ≡ ⊥
    the third case is unreachable.
    7. @@ -396,7 +402,7 @@ t ≤ s &Lrarrow; [t] ⊆ [s]
  7. Introduced in 1997 by Gérard Huet
  8. Stack of visited nodes
  9. Push the current node on the stack when traversing a pair
    10. -
  10. Take top of the stack to go backward
    11. +
  11. Take the top of the stack to go backward
  12. Tag the elements of the stack to remember which component of a pair we have visited
    13. @@ -410,12 +416,12 @@ t ≤ s &Lrarrow; [t] ⊆ [s]

    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; 
+    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 +437,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 _* ]
+    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; … @@ -490,9 +493,9 @@ 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
@@ -500,9 +503,8 @@ nodes in special variables p: pattern
γ: mapping from capture variables to values
- δ: current context

-
+
v ∈ [ t ] σ; δ ⊢ v / t &rleadsto; ∅, @@ -511,28 +513,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,7 +567,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
    • @@ -585,7 +588,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;
    @@ -661,9 +664,9 @@ which is not a type.

     
-                               ⬆ ⬆     ⬆     ⬆
+                                  ⬆ ⬆     ⬆     ⬆
 
-                                                   parent         
+                                                    parent         
 
 
 
@@ -673,7 +676,7 @@ 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;
      •
@@ -684,9 +687,9 @@ which is not a type.

  • 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. generalise from products to extensible records
    • +
  • Extend the approach to Json (google ``path language for json´´), i.e. generalise from products to extensible records
    • - +

    Thank you!

    -- 2.17.1