Shows (1) a way to group ``gradually typed'' languages by their
semantics --- in particular how they enforce types at the boundary
between typed and untyped code --- and (2) results from an evaluation
comparing the three semantics as three ways of running a set of
Typed Racket programs.
Reticulated is an implementation of sound gradual typing for Python.
This talk explains two points: (1) the soundness guarantee is very weak compared to standard, strong type soundness; and (2) the run-time cost of enforcing soundness is low.
Our 2016 paper Is Sound Gradual Typing Dead? introduced a graphical shorthand for describing the performance of a gradual type system.
These slides explain the practical experience that led us to the shorthand.
Presented at a little ECOOP'16 PC weekend of talks.
Sound gradual typing is not about catching more run-time errors at compile-time.
Rather, the goal is to provide the minumum safety guarantees for a trustworthy type system in the presence of unchecked code.
If the types are not protected at runtime, there is a risk for silent errors.
Presentation at STOP 2015 (co-located workshop at ECOOP 2015).
Performance evaluation needs to be a priority for gradual type systems.
We recommend measuring the performance of all configurations on example programs, and reporting the proportion of configurations with acceptable performance (for example, under 200% slowdown).
This paper combines two very different worlds, Scheme and System F, and proves that the resulting multi-language system has something very much like parametricity.
The only caveats are that mixed programs might diverge or raise exceptions -- that's all!
Talk given to the Cornell PL club.
Ben Carriel and I gave this presentation to the Cornell PL club.
The original POPL 2014 paper by Robert Atkey is here.
We included Dijkstra to wake up the audience for our main point: that viewing types as geometries helps give insight into when you can and can't extract a free theorem.