From: Kim Nguyễn Date: Tue, 14 Apr 2015 09:32:27 +0000 (+0200) Subject: . X-Git-Url: http://git.nguyen.vg/gitweb/?p=hacks%2FsimpleWebSlides.git;a=commitdiff_plain;h=c3072e9daada0a8f3d4ec882b064011316191bb1 . --- diff --git a/pres-esop15/01.xhtml b/pres-esop15/01.xhtml index e1e432e..fe24755 100644 --- a/pres-esop15/01.xhtml +++ b/pres-esop15/01.xhtml @@ -309,7 +309,7 @@

&cduce;'s type algebra

A set &mathT; of types

-
    t ::=  b  |  c  |  t × t  |  t &rarrow; t  |  t &lor; t  |  t  &land; t  |  t ∖ t  |    |    |  α
+
    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 diff --git a/pres-esop15/notes.txt b/pres-esop15/notes.txt new file mode 100644 index 0000000..9c726d7 --- /dev/null +++ b/pres-esop15/notes.txt @@ -0,0 +1,69 @@ +1 Thank you, Hello, Joint work with … + +2 XQuery (3.0) looks like that: 2 functions … + Path expressions to navigate + List comprehension syntax + type-switch case + switch case + +3 Pros and Cons of XQuery + +4 CDuce : Syntax similar to OCaml + Patterns (in part. XML constructs with tag, attributs, list of children) + Types! (with constructors, intersections, …) + List comprehension too. + +5 Pros and Cons of CDuce + +6 This work (support for path navigation, using zippers …) Can be used to typecheck XQuery programs + I'm gonna focus on 1 in this talk + +7 Type algebra + Allows to encode regular expression types + +8 Semantic subtyping + +9 CDuce DataModel + +10 CDuce patterns ( Unify typecase and value case, capture variables, destructors, alternation, intersection) + Semantics is to return a set of bindings + CDuce patterns are typed very precisely + +11 Patterns examples : like types but with capture variables + Exhaustiveness check + So we have this nice functional languages, how to navigate (with upward axes) + +12 What are zippers + +13 Example of zippers and basic operations + +14 Zipper types recursive too, which allows to write reg exps. + +15 Already we can check complex conditions + +16 Operators & Accumulators + +17 Some operators, we'll see why we want them to be built-in + +18 Simplified, pattern matching semantics. Only a few rules. + +19 Typing patterns with accumulators need approximation + +20 Typing patterns with accumulators using accumulators + +21 Results + +22 Encoding XPath Downward + Self + Child applied to some document (root, unfold regular expression and try alternatives) + Returns this binding, with zippers inside! + descendant-or-self (recursively apply child). We update zippers + but we dont use them! + +23 Binary tree coding + +24 Upward Axis + Parent : current node is e + First walk up and check that it's someone's left child + Then walk backwards to skip the previous siblings + Then finaly capture the parent