Transitioning from Structural to Nominal Code with Gradual Typing

Transitioning from Structural to Nominal Code with Efficient Gradual Typing Fabian Muehlboeck and Ross Tate

Gradual Typing fun zorp(){ : dyn return new { fun foo(x return x * x; } ; : dyn ) { : dyn } } 2 Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing

Gradual Typing fun zorp() return new { : dyn { fun foo(x : dyn): dyn { return x * x; } ; int) int Run-Time Type Check } } 3 Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing

Gradual Typing fun zorp(): dyn { ? { foo : int int } return new { fun foo(x : dyn): dyn { Bar() class Bar int) int return x * x; } ; } } 4 Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing

fun main() { twice(zorp()); } fun zorp() : dyn { return new { fun foo(x : dyn) : dyn { return x * x; }; }; } fun twice(f : dyn) : dyn { return f.foo(f.foo(0)); } fun zorp() : dyn { return new { fun foo(x : int) : int { return x * x; }; }; } fun twice(f : dyn) : dyn { Foo F = f; return F.foo(F.foo(0)); } class Bar() implements Baz { fun foo(x : int) : int { return x * x; }; } fun zorp() : dyn { return new Bar(); } fun twice(f : Baz) : int { return f.foo(f.foo(0)); } class Bar() implements Baz { fun foo(x : int) : int { return x * x; }; } fun zorp() : Baz { return new Bar(); } interface Baz { fun foo(x : int) : int; } Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing 5

MonNom Fabian Muehlboeck and Ross Tate

MonNom Objects Nominal Types new C(e1, ) : C dyn instead of Structural Types : dyn new (x1 : 1, ) : e : dyn new x := {f1 := e1; | m1(x1 : 1, ) : e1 ; } method this/self field (can be field name or ) 7 Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing

MonNom Casts Casts to classes C succeed for instances of C Casts to interfaces I succeed for instances of classes explicitly implementing I succeed for all lambda objects succeed for all record objects unless I requires a method and the record has no method fail for structural values Monotonic 8 Transitioning from Nominal to Structural Code with Efficient Gradual Typing Fabian Muehlboeck and Ross Tate

Migration Fabian Muehlboeck and Ross Tate

Cross-Discipline Guarantees then e type-checks If e type-checks e e then so does e If e executes successfully Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing 10

Cross-Paradigm Guarantees If e type-checks in the context defined by program P then its relaxation e type-checks in the context of the relaxed program P P P e e then so does its relaxation e using the relaxed program P If e executes successfully using the implementation defined by program P Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing 11

Cross-Paradigm Guarantees Types in more relaxed expression must be valid in the more relaxed program P ? P P ?? ?? P P ?[? ? ] ? ? ? P P let? : := ??in ? let? : := ?? in ? Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing 12

Cross-Paradigm Guarantees The more relaxed program does not have class ? P ? ?1:?1 ?1; ?1 } P ? ? P P ?? ?? P P ? ?1 ?1; ?1 } ? P P new? ?? let? : := ?? class? ? ? P ? in? Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing 13

Performance

Representation Typed Untyped 64-bit values Pointers Pointers 64-bit aligned 62-bit Integers 64-bit Integers +2 Tag Bits Doubles with 10-bit Exponents IEEE-754 Doubles 15 Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing

Call Tags Interface-Method Table IMT Entry 1 IMT Entry 2 IMT Entry 13 ?(callTag, receiver, args ) { if(callTag == [Baz.foo]) { return Bar.foo(receiver, args); } } ?(callTag, receiver, args ) { return callTag(receiver, args ); } 16 Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing

Call Tags Call Tag: Function Pointer = Identifier for Interface/Method Pair [Baz.foo](receiver, args ) { 1.) look up foo in receiver 2.) pack/box integer argument 3.) call foo with (converted) args 4.) check return value is int 5.) convert int representation } 17 Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing

Experimental Setup Excessive overheads Fully Typed/Nominal Add Type Annotation Add Interface Distance to fully typed Running time Turn Record Into Class Distance to fully typed Fully Untyped/Structural 18 Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing

intersort 0.20 0.18 RUNNING TIMEIN SECONDS 0.16 0.14 0.12 0.10 0.08 0.06 0.04 0.02 0.00 5 4 3 2 1 0 NUMBEROF STEPSTO FULLY TYPED JAVA MONNOM HIGGSCHECK C# JAVASCRIPT RETICULATED PYPY Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing 19

sieve & float 25 0.1 0.09 RUNNING TIMEIN SECONDS RUNNING TIMEIN SECONDS 20 0.08 0.07 15 0.06 0.05 10 0.04 0.03 5 0.02 0.01 0 0 10 9 8 7 6 5 4 3 2 1 0 5 4 3 2 1 0 NUMBEROF STEPSTO FULLY TYPED GRIFT MONO GRIFT SIEVE NUMBEROF STEPSTO FULLY TYPED JAVA MONO GRIFT FLOAT MONNOM NOM JAVA JAVASCRIPT C# TYPED RACKET MONNOM GRIFT C# RETICULATED JAVASCRIPT PYPY Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing 20

Summary Gradual migration not only between typing disciplines MonNom: co-design for gradual guarantees and efficient implementation In the paper/technical report: Formalization; Gradual Guarantees, Safety More details on Benchmarks In the artifact: Complete source code (MonNom + Benchmarks) Invariant Generics, Static Methods, Ints/Floats/Null, Top/Bottom, Fabian Muehlboeck and Ross Tate Transitioning from Nominal to Structural Code with Efficient Gradual Typing 21