Nested Refinements:A Logic for Duck Typing

"Nested Refinements present a logical approach to Duck Typing by Ravi Chugh, Pat Rondon, and Ranjit Jhala, addressing dynamic languages, lack of static types, and designing a type system. The content discusses control flow, first-class functions, inheritance, and the challenges in dynamically typed languages."

• Logic
• Duck Typing
• Dynamic Languages
• Type System
• Control Flow

jaye_un Follow

Uploaded on Mar 08, 2025 | 1 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

Presentation Transcript

1. Nested Refinements: A Logic for Duck Typing Ravi Chugh, Pat Rondon, Ranjit Jhala (UCSD)

2. What are Dynamic Languages? d._onto = function(arr,obj,fn) { if (!fn) { arr.push(obj); } else if (fn) { var func = (typeof fn == string ) ? obj[fn] : fn; arr.push(function() { func.call(obj); }); } } affect control flow tag-tests indexed by arbitrary string keys dictionary objects can appear inside objects first-class functions mutation affects object lookup inheritance 2

3. What are Dynamic Languages? Lack of static types makes rapid prototyping / multi-language applications easy makes reliability / performance / maintenance hard Goal: Design a type system for these features affect control flow tag-tests These alone are hard! indexed by arbitrary string keys dictionary objects can appear inside objects first-class functions mutation affects object lookup inheritance 3

4. if tagof f = Str then d.n + d[f](0) else d.n + f(0) affect control flow tag-tests These alone are hard! indexed by arbitrary string keys dictionary objects can appear inside objects first-class functions 4

5. Approach: Refinement Types tag-tests Type environment tracks control flow predicates { | tag( )= Bool } x :: { | tag( )= Int } x :: if tagof x = Int then 0 - x else not x { | tag( )= Int tag( )= Bool } x :: 5

6. Approach: Refinement Types tag-tests d.n + d[m] dictionaries { | tag( )= Dict tag(sel( , n ))= Int tag(sel( ,m))= Int } d :: McCarthy axioms d,k,k ,x. k k sel(upd(d,k,x),k) = x sel(upd(d,k,x),k ) = sel(d,k ) sel(empty,k) = bot 6

7. Approach: Refinement Types tag-tests 1 + f (0) dictionaries first-class functions x:{ | tag( )= Int } { | tag( )= Int } f :: x:{ | tag( )= Int } { | = x } x.x :: Clear separation of base and arrow types T ::= { | p } | x:T1 T2 7

8. Approach: Refinement Types tag-tests 1 + f (0) dictionaries first-class functions 8

9. Approach: Refinement Types tag-tests 1 + d[f](0) dictionaries first-class functions { | tag( )= Dict d :: sel( ,f) ??? } Key Challenges 1. How to describe arrow inside formula? 2. How to keep type checking decidable? 9

10. Approach: Refinement Types Reuse refinement type architecture Find a decidable refinement logic for * Tag-tests Dictionaries Lambdas Define nested refinement type architecture 10

11. Nested Refinements 1 + d[f](0) { | tag( )= Dict d :: sel( ,f):: { | tag( )= Int } { | tag( )= Int } } uninterpreted constant in the logic uninterpreted predicate x::U says x has-type U but syntactic arrow in the type system! 11

12. Nested Refinements Refinement formulas over a decidable logic uninterpreted functions, McCarthy arrays, linear arithmetic Only base values refined by formulas All values T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U T ::= { | p } | x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | traditional refinements 12

13. Nested Refinements Refinement formulas over a decidable logic uninterpreted functions, McCarthy arrays, linear arithmetic Only base values refined by formulas All values has-type allows type terms in formulas T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U T ::= { | p } | x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | traditional refinements 13

14. Nested Refinements Refinement formulas over a decidable logic uninterpreted functions, McCarthy arrays, linear arithmetic Only base values refined by formulas All values has-type allows type terms in formulas T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U 14

15. let foo f d = if tagof f = Str then d.n + d[f](0) else d.n + f(0) f:{ | Str( ) ::Int Int} d:{ | Dict( ) Int( .n) Str(f) [f]::Int Int} Int foo :: T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U 15

16. let foo f d = if tagof f = Str then d.n + d[f](0) else d.n + f(0) f:{ | Str( ) ::Int Int} d:{ | Dict( ) Int( .n) Str(f) [f]::Int Int} Int foo :: T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U 16

17. let foo f d = if tagof f = Str then d.n + d[f](0) else d.n + f(0) { | tag( )= Int } { | tag( )= Int } f:{ | Str( ) ::Int Int} d:{ | Dict( ) Int( .n) Str(f) [f]::Int Int} Int foo :: tag( )= Str T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U 17

18. let foo f d = if tagof f = Str then d.n + d[f](0) else d.n + f(0) f:{ | Str( ) ::Int Int} d:{ | Dict( ) Int( .n) Str(f) [f]::Int Int} Int foo :: T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U 18

19. let foo f d = if tagof f = Str then d.n + d[f](0) else d.n + f(0) sel( , n ) sel( ,f) f:{ | Str( ) ::Int Int} d:{ | Dict( ) Int( .n) Str(f) [f]::Int Int} Int foo :: T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U 19

20. let foo f d = if tagof f = Str then d.n + d[f](0) else d.n + f(0) f:{ | Str( ) ::Int Int} d:{ | Dict( ) Int( .n) Str(f) [f]::Int Int} Int foo :: T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U 20

21. let foo f d = if tagof f = Str then d.n + d[f](0) else d.n + f(0) { | tag( )= Str :: } Int Int { | :: foo :: f: { | :: { | tag( )= Dict d: tag(sel( , n ))= Int tag(f)= Str Int Int sel( ,f):: } } T ::= { | p } U ::= x:T1 T2 p ::= p q | | x = y | x < y | | tag(x) = Int | | sel(x,y) = z | | x :: U Int } 21

22. Nested Refinements Type Language Subtyping Extensions Recap 22

23. Subtyping Subtyping tag( )= Int true Implication Int <: Top SMT Solver T ::= { | p } | x:T1 T2 { | tag( )= Int } Int { | true} Top traditional refinements 23

24. Subtyping Subtyping Implication tag( )= Int tag( )= Int tag( )= Int true SMT Solver Int <: Top Int <: Int Top Int <: Int Int T ::= { | p } | x:T1 T2 { | tag( )= Int } Int { | true} Top traditional refinements 24

25. Subtyping Subtyping Arrow Rule Implication tag( )= Int tag( )= Int tag( )= Int true SMT Solver Int <: Top Int <: Int Top Int <: Int Int T ::= { | p } | x:T1 T2 { | tag( )= Int } Int { | true} Top traditional refinements 25

26. Subtyping Subtyping Arrow Rule Decidable if: Only values in formulas Underlying theories decidable Implication SMT Solver With nested refinements: No new theories But implication is imprecise! T ::= { | p } | x:T1 T2 traditional refinements 26

27. Subtyping with Nesting Subtyping Implication ::Top Int ::Int Int SMT Solver Invalid, as these are distinct uninterpreted constants 27

28. Subtyping with Nesting When goal is base predicate: p q When goal is has-type predicate: p x::U Subtyping Subtyping Arrow Rule Implication Implication U <:U p x::U p q SMT Solver SMT Solver 28

29. Subtyping with Nesting Uninterpreted Reasoning Syntactic Reasoning + p ::Top Int Top Int <: Int Int p ::Int Int Normalize formulas to subdivide obligations appropriately 29

30. Nested Refinements Type Language Subtyping Extensions Recap 30

31. Extensions Simple to add additional type constructors Extend the grammar of type terms U ::= x:T1 T2 | A | List[T] | Null Add additional syntactic subtyping rules Arrow Rule Syntactic Rules Covariant List Rule Null List Rule 31

32. Map A,B. { | ::A B} { | ::List[A]} { | ::List[B]} let map f xs = if xs = null then null else f xs[ hd ] :: map f xs[ tl ] encode recursive data as dictionaries 32

33. Filter let filter f xs = if xs = null then null else if f xs[ hd ] then xs[ hd ] :: filter f xs[ tl ] else filter f xs[ tl ] usual definition, but an interesting type A,B.{ | ::x:A { | =True x ::B}} { | ::List[A]} { | ::List[B]} 33

34. Dispatch let dispatch d f = d[f] d A,B.d:{ | Dict( ) ::A} { | Str( ) d[ ]::A B} { | ::B} a form of bounded quantification since d::A but additional constraints on A 34

35. Recap Refinement types are a compelling approach Dynamic dictionaries require dependency Tag-tests require path sensitivity But, not enough for lambdas in dictionaries Nested refinement types are a clean solution Natural way to describe dynamic idioms Novel subtyping remains decidable and automatic Interesting soundness proof 35

36. Future Work Extend to imperative JavaScript setting Employ strong update techniques Track prototype chain for inheritance Better inference Untyped programmers allergic to annotations Perhaps utilize run-time information Applications JavaScript benchmarks (e.g. SunSpider) JavaScript frameworks (e.g. Dojo) 36

37. Thanks! D :: http://cseweb.ucsd.edu/~rchugh/research/nested/ 37

38. Extra Slides 38

39. Constants x:Top { | =tag(x) } tagof :: d:Dict k:Str { | Bool( ) =True has(d,k) } d:Dict k:{ | Str( ) has(d, ) } { | =sel(d,k) } mem :: get :: d:Dict k:Str x:Top { | =upd(d,k,x) } set :: d:Dict k:Str { | =upd(d,k,bot) } rem :: 39

40. Macros { | tag( )= Int } Types Int { | :: } x:T1 T2 x:T1 T2 Formulas Str(x) has(d,k) tag(x) = Str sel(d,k)!=bot EqMod(d,d ,k) k . k !=k sel(d,k)!=sel(d ,k) Logical Values x.k x[k] sel( , k ) sel( ,k) 40

41. Functional Onto let onto callbacks f obj = if f = null then new List(obj,callbacks) else let cb = if tagof f = Str then obj[f] else f in new List(fun () -> cb obj, callbacks) A. callbacks:List[Top Top] onto :: f:{ | Str( ) ::A Top} obj:{ | ::A (f = null ::A Int) (Str(f) [f]::A Int)} List[Top Top] 41

42. Functional Onto (2) let onto (callbacks,f,obj) = if f = null then new List(obj,callbacks) else let cb = if tagof f = Str then obj[f] else f in new List(fun () -> cb obj, callbacks) callbacks:List[Top Top] onto :: *f:{ g | Str(g) g ::{ x | x =obj } Top} *obj:{ o | (f = null o::{ x | x =o } Int) (Str(f) o[f]::{ x | x =o } Int)} List[Top Top] 42

43. Normalization TODO 43

44. Related Work TODO 44