Gradual Typing for Functional Languages

I hope to present one of the earliest papers on Gradual Typing.
We will start with the basics.

• Various approaches of typing and the differences.

• Static, Gradual, Optional etc

• Contrast static and run time guarantees/behavior of untyped and typed lambda calculus

• Learn the Notation in Programming Language Theory

We will also look into other candidates in this space and what they do differently - like flowtype for js, typed racket, mypy etc.

Paper: http://ecee.colorado.edu/~siek/pubs/pubs/2006/siek06_gradual.pdf

Supplementary reading:

• http://wphomes.soic.indiana.edu/jsiek/what-is-gradual-typing/

• http://siek.blogspot.in/2012/07/crash-course-on-notation-in-programming.html

• http://samth.github.io/gradual-typing-bib/

Abstract:

Static and dynamic type systems have well-known strengths and weaknesses, and each is better suited for different programming tasks. There have been many efforts to integrate static and dynamic typing and thereby combine the benefits of both typing disciplines in the same language. The flexibility of static typing can be improved by adding a type Dynamic and a typecase form. The safety and performance of dynamic typing can be improved by adding optional type annotations or by performing type inference (as in soft typing). However, there has been little formal work on type systems that allow a programmer-controlled migration between dynamic and static typing.

In this paper we present a solution based on the intuition that the structure of a type may be partially known/unknown at compile-time and the job of the type system is to catch incompatibilities between the known parts of types. We define the static and dynamic semantics of a λ calculus with optional type annotations and we prove that its type system is sound with respect to the simply-typed λ calculus for fully-annotated terms. We prove that this calculus is type safe and that the cost of dynamism is pay-as-you-go.