dcreager.net

Gradual types

a theory for integrating static and dynamic typing within a single language that 1) puts the programmer in control of which regions of code are statically or dynamically typed and 2) enables the gradual evolution of code between the two typing disciplines
[Siek2015]

[Siek2015] “Refined Criteria for Gradual Typing”

A good overview paper of Castagna et al's work:

[Castagna2022] “Programming with Union, Intersection, and Negation Types”

Two papers describing type variables and specialization inference in more detail:

[Castagna2014] “Polymorphic functions with set-theoretic types: Part 1: Syntax, semantics, and evaluation”

[Castagna2015] “Polymorphic functions with set-theoretic types: Part 2: Local type inference and type reconstruction”

Implementations

CDuce is a full programming language that uses set-theoretic types directly. It is the running example / proof of concept mentioned in all of the Castagna et al papers.

CDuce source repo

sstt is an OCaml library implementing the core logic of set-theoretic types. It is largely extracted/rewritten from the CDuce source.

sstt [GitHub]

» Theory

» Languages » Python » Typing