Dynamic and Gradual Typing

From Milestone M5, a Bridger program is checked as a whole before any of it runs. This one holds a list of named settings, each paired with a value of a different type, and prints them. to_string is the prelude’s conversion of a value to its text:

fn main() {
    let settings = [("width", 80), ("title", "Report"), ("verbose", true)];
    for s in settings {
        println(s.0 ++ " = " ++ to_string(s.1));
    }
}

The M4 evaluator prints width = 80, title = Report, and verbose = true. The M5 checker rejects the program at "Report", with expected Int, found String: a list’s elements share one type, and the first pair fixed it as (String, Int).

Before M5, a function’s signature declared types that nothing checked. In this second program, indent declares width: Int and returns that many spaces, and main passes it the second component of each setting:

fn indent(width: Int) -> String =
    if width > 0 { " " ++ indent(width - 1) } else { "" };

fn main() {
    let settings = [("width", 4), ("title", "Report")];
    for s in settings {
        println(indent(s.1) ++ s.0);
    }
}

On the M4 evaluator it prints width and then stops with expected Int, found String at width > 0, inside indent. The mistake is in main, which passed a string to a function whose signature asks for an Int.

The programs raise these questions:

• Can a program be checked in part? The settings program could keep its checked functions and leave the list unchecked. What would a checker do with a value whose type it has not been told?
• When an unchecked value reaches checked code, who checks it, and who is blamed? The M4 run reports the failure inside indent. What would it take to report it at the call in main, and what if the value crossing over is a function?
• What is left of the types when the program runs? Bridger’s checker hands the evaluator nothing. A check made at run time can read only what the run time keeps.

Languages without static types go back at least to Lisp. Mixing checked and unchecked code in one program is more recent.

Tags and types

Bridger’s evaluator has been dynamically typed since Part II. Each value carries a tag, the variant of Value it was built as, and each arm checks the tag of the values it receives: addition requires two Value::Ints, a call requires a Value::Closure. A tag records less than a type. The tag of |n| n + 1 says that it is a function, and nothing about what it takes or returns; the interpreter’s diagnostics print a closure’s type as fn(…), since that is all the value records. Lisp, Smalltalk, and Python check tags in the same way, which puts them in the safe and untyped cell of Cardelli’s table.

Statically typed languages sometimes needed values whose type was not known until run time: data read from a file, or a message from another program. Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin’s “Dynamic Typing in a Statically Typed Language” (1991) gave such values a type of their own: “we propose to add a type Dynamic whose values are pairs of a value v and a type tag T where v has the type denoted by T. Instances of Dynamic are built with an explicit tagging construct and inspected with a type safe typecase construct.” A program had to inspect a Dynamic value’s tag explicitly before it could use the value at any other type.

Jeremy Siek and Walid Taha’s “Gradual Typing for Functional Languages” (2006) removed the explicit inspection. “The focus of this paper is languages that literally provide static and dynamic typing in the same program, with the programmer controlling the degree of static checking by annotating function parameters with types, or not.” A parameter without an annotation got an unknown type, and the checker let a value of that type flow wherever a typed value was expected, inserting a check at run time in place of a typecase. In the same year Sam Tobin-Hochstadt and Matthias Felleisen’s “Interlanguage Migration: From Scripts to Programs” (2006) addressed programmers whose untyped scripts had grown into programs they wanted to type: “Ideally, they should port one module at a time, always leaving the overall product intact and running.” Their Typed Scheme, now Typed Racket, made that migration possible a module at a time.

A type for the unknown

Siek and Taha write the unknown type ?. Bridger already uses ? as the error-propagation operator of Part VIII, so the programs below write the type ? as Dyn; the typing rules and the prose keep Siek and Taha’s ?. Bridger has no Dyn type. The programs in this section and the next are written in a hypothetical gradual Bridger, and their behaviour is worked out from the rules; none of them will run in the version of Bridger this book builds.

In the settings program, the list could be given the type [(String, Dyn)]: each element a pair of a name and a value of unknown type.

let settings: [(String, Dyn)] =
    [("width", 80), ("title", "Report"), ("verbose", true)];

The checker cannot require 80 and "Report" to have the same type as Dyn, since no type equals an unknown one. Siek and Taha replace equality with a weaker relation: “The intuition is that we should require the known portions of the two types to be equal and ignore the unknown parts.” Two types are consistent, written $\tau \sim {\tau }^{\prime }$, by these rules:

$$\frac{}{\tau \sim \tau }(\text{C-Refl})\frac{}{\tau \sim ?}(\text{C-DynR})\frac{}{?\sim \tau }(\text{C-DynL})\frac{{\tau }_1\sim {\sigma }_1{\tau }_2\sim {\sigma }_2}{\text{fn}({\tau }_1)\to {\tau }_2\sim \text{fn}({\sigma }_1)\to {\sigma }_2}(\text{C-Fn})$$

with lists, tuples, and reference types consistent when their parts are, as with $\text{C-Fn}$. Int is consistent with ?, and so is String, and $\text{fn}(\text{Int})\to ?$ is consistent with $\text{fn}(?)\to \text{Bool}$. Int and String are not consistent with each other, so the relation, in Siek and Taha’s words, is “reflexive and symmetric but not transitive”: $\text{Int}\sim ?$ and $?\sim \text{String}$ do not give $\text{Int}\sim \text{String}$.

The bidirectional checker of A type checker changes in one rule. Where $\text{Chk-Sub}$ required the synthesized type to equal the expected one, the gradual version requires consistency:

$$\frac{\Gamma ⊢e\Rightarrow {\tau }^{\prime }{\tau }^{\prime }\sim \tau }{\Gamma ⊢e\Leftarrow \tau }(\text{Chk-Sub-Gradual})$$

The other rules use consistency wherever they compared types. In the loop, s.1 has type ?, and indent(s.1) is accepted, since $?\sim \text{Int}$. indent("Report") is still rejected, because String and Int are both known and differ. A program with no Dyn in it is checked exactly as before, since without ? consistency is equality. A program that writes Dyn everywhere is accepted wherever M4 would have run it.

Checking at the boundary

The checker has accepted indent(s.1) without knowing that s.1 is an Int, and indent’s body was checked on the assumption that width is an Int. Something has to confirm the assumption when the value arrives. Wherever the checker used consistency between two different types, it rewrites the expression to carry a cast, a check to be made at run time. A cast is written $⟨{\tau }_{to}\Leftarrow {\tau }_{from}{⟩}^{\ell }$, read from right to left, from the type the value has to the type it is needed at:

$$⟨\text{Int}\Leftarrow ?{⟩}^{\ell }\text{s.1}$$

reads check that the value of s.1, of type ?, is an Int. Siek and Taha describe what the cast does: “When e evaluates to v, the cast will check that the type of v is consistent with τ and then produce a value based on v that has the type τ. If the type of v is inconsistent with τ, the cast produces a CastError.” The label $\ell$ records where the cast was inserted, here the argument of the call in main.

A cast to Int reads the value’s tag, the same check the evaluator’s addition arm makes. For the pair ("title", "Report"), the cast finds a Value::Str and fails before indent is entered. The error names $\ell$, the call in main, whereas M4 reported the failure at the comparison inside indent. Errors of this kind join the right-hand column of the soundness table: a gradually typed program that the checker accepts can stop with a failed cast at a boundary, while its typed parts never stop on a type error of their own.

Functions

A cast to a function type cannot be checked by reading a tag. The hypothetical program below binds a lambda to a name of type Dyn and passes it to twice, whose parameter is $\text{fn}(\text{Int})\to \text{Int}$:

fn twice(f: fn(Int) -> Int, x: Int) -> Int = f(f(x));

fn main() {
    let g: Dyn = |n| to_string(n);
    println(twice(g, 2));
}

The cast at the call is $⟨\text{fn}(\text{Int})\to \text{Int}\Leftarrow ?{⟩}^{\ell }\text{g}$, and the value of g is a closure whose tag says only that it is a function. Whether it returns an Int for every Int it is given is a question about every call it could receive, and no inspection of the closure answers it in general. Robert Bruce Findler and Matthias Felleisen’s “Contracts for Higher-Order Functions” (2002) met the problem when checking contracts: “The key observation is that a contract checker cannot ensure that g’s argument meets its contract when g is called. Instead, it must wait until proc is applied.”

So the cast checks the tag, and then wraps the closure in a new function that checks each use:

$$⟨\text{fn}(\text{Int})\to \text{Int}\Leftarrow ?{⟩}^{\ell }g=\lambda x.⟨\text{Int}\Leftarrow ?{⟩}^{\ell }(g⟨?\Leftarrow \text{Int}{⟩}^{\ell }x)$$

Because g has type ?, the wrapper treats its parameter and result types as ?. It casts the incoming Int argument to ?, which always succeeds, and casts g’s result from ? to Int, which can fail. twice calls the wrapper with 2, g returns the string "2", and the result’s cast fails, naming $\ell$: the call in main that supplied g. With the Dyn annotation removed, the M4 evaluator runs the same program to completion: the first call to g returns "2", the second passes "2" to to_string and gets "2" back, and main prints 2, a string returned by a function whose signature promised an Int.

Siek and Taha’s closures carried the types of their parameters, so their casts could reject a function at once when its declared type was inconsistent with the target. A closure built from |n| to_string(n) has no declared parameter type in Bridger, and its run-time value records none, so the wrapper is the only check available.

Blame

The label on a cast says which side of a boundary failed. Philip Wadler and Robert Bruce Findler’s “Well-Typed Programs Can’t Be Blamed” (2009) proved which side that can be: “when a program integrating less-typed and more-typed components goes wrong the blame must lie with the less-typed component.” In both examples the failure is blamed on main, where a Dyn value met a typed parameter. indent and twice are never blamed, because their types were checked. The title echoes Milner’s “well-typed programs cannot go wrong”, from Soundness, informally: a gradually typed program can go wrong, but only in the parts that are not statically typed.

Where types go after checking

A cast reads something the running program keeps. A check on Int needs a tag on every value, and a check on a function type needs a wrapper that remembers the target type. Languages differ in how much of a program’s types survive to run time, and the difference decides which of these checks a language can make.

Erased

Bridger’s checker passes the evaluator nothing, as the first chapter of this part described, and the evaluator runs an accepted program exactly as it would have run unchecked. Once checking is done, the types are gone; only the tags remain, and they were there before the checker existed. Part IX is the first place the checker gives the evaluator something it worked out from types.

TypeScript erases more. As its handbook puts it, “once TypeScript’s compiler is done with checking your code, it erases the types to produce the resulting “compiled” code. This means that once your code is compiled, the resulting plain JS code has no type information.“ Where untyped JavaScript passes a value to a TypeScript function, nothing checks it, since nothing in the compiled code records what the function’s parameter was declared to be. TypeScript is gradual in what its checker accepts, and it has a type any that is consistent with every type, but it inserts no casts. Its boundaries behave like the M4 run of indent: a wrong value travels into typed code and fails, if at all, wherever an operation finally rejects it.

Java erases part of its types. Generic classes were added in 2004 to a virtual machine that had none, and the compiler checks the type arguments and then removes them, as Function types and polymorphism described. The language specification states the consequence: “Because some type information is erased during compilation, not all types are available at run time. Types that are completely available at run time are known as reifiable types.” A List<String> and a List<Integer> are the same class when the program runs, so a cast to List<String> can check that a value is a list, but not what the list holds. The compiler warns that such a cast is unchecked.

Kept

A language can keep types where it will need them. C# keeps the type arguments of its generics at run time, so a List<int> and a List<string> remain distinguishable. Its dynamic type, added in C# 4.0 in 2010, is the reverse of Abadi and his colleagues’ typecase: “The dynamic type indicates that the variable and references to its members bypass compile-time type checking. Instead, these operations are resolved at run time.” Each operation on a dynamic value consults the value’s run-time type, which the virtual machine records for every object.

Compilers keep types longer than interpreters do, in the typed intermediate representations that A type checker described, because they choose representations and instructions by type. They usually discard them when they emit machine code. Rust and C++ compile a separate copy of a generic function for each type it is called with, so the types are fixed in the generated code and none need be recorded at run time.

What a boundary can check

Sound gradual typing needs at least Bridger’s amount of run-time information: tags for checking base types, and closures that can be wrapped. A language that erases its types and checks nothing at the boundary, as TypeScript does, can be gradual only in its checker. A cast inserted by the checker needs some part of the type to remain when the program runs.

Bridger’s types

Bridger has no Dyn. Through M4 it is untyped, and from M5 it is statically typed, with every declaration checked before main starts. It never mixes the two in one program. The evaluator keeps its tag checks throughout, which is what lets the same evaluator run the untyped milestones and backs up the checker in the typed ones.

For values of several types in one list, Bridger’s answer arrives in Part VIII. A sum type names the possibilities, and match takes a value apart according to which one it is:

type Setting = Num(Int) | Text(String) | Flag(Bool);

fn show(v: Setting) -> String = match v {
    Num(n) => to_string(n),
    Text(s) => s,
    Flag(b) => to_string(b),
};

fn main() {
    let settings = [("width", Num(80)), ("title", Text("Report")),
                    ("verbose", Flag(true))];
    for s in settings {
        println(s.0 ++ " = " ++ show(s.1));
    }
}

This prints the three lines the M4 evaluator printed for the original program, and the checker accepts it. Num, Text, and Flag are tags the program declares itself, and match inspects them, much as typecase inspects a Dynamic value’s tag. The sum type lists the types a setting may have. Dyn would allow any, and would leave the checking to the casts.

The design space

How much a boundary checks

Gradually typed languages differ in what happens where an unchecked value meets a type.

• Nothing. TypeScript’s checker uses any the way the rules above use ?, and its compiled code contains no casts. Python’s annotations are checked by separate tools such as mypy, and, as PEP 484 says, not when the program runs. This is often called optional typing. A program runs at full speed, and an annotation is a claim nothing enforces at run time.
• The value’s own tag, and no wrapper. Reticulated Python, described by Michael Vitousek, Andrew Kent, Jeremy Siek, and Jim Baker in “Design and Evaluation of Gradual Typing for Python” (2014), offers a transient semantics: “In the transient semantics, a cast checks that the value has a type consistent with the target type of the cast, but it does not wrap the value in a proxy.” A function is checked to be callable, and its arguments and results are checked where it is used. The checks are cheaper, and when one fails, the paper notes, the implementation “is unable to report the location of the original cast that caused the error to occur”.
• Tags and wrappers, with blame. Typed Racket, the descendant of Tobin-Hochstadt and Felleisen’s Typed Scheme, checks every value that crosses from an untyped module into a typed one, wraps functions and other values whose types cannot be checked at once, and blames the module at fault. The guarantee is the one Wadler and Findler proved.

What sound boundaries cost

The wrappers run on every call that crosses a boundary, and a wrapped function passed back and forth gathers a wrapper at each crossing. Asumu Takikawa and colleagues’ “Is Sound Gradual Typing Dead?” (2016) measured Typed Racket programs with every combination of typed and untyped modules. Earlier publications, their abstract notes, gave few measurements: “Worse, a few report disastrous numbers.” Their own conclusion: “We find that Typed Racket’s cost of soundness is not tolerable.” The slow configurations were mixtures, in which values crossed many boundaries: the state a program is in while it is being migrated one module at a time. The transient design, which predates the paper, accepts weaker checks and less precise error reports in exchange for cheaper boundaries.

Dynamic values in a static language

Abadi and his colleagues’ Dynamic and C#’s dynamic start from a statically typed language and let some values be checked late. The first requires the program to inspect the tag before using the value; the second resolves each operation on the value at run time. Gradual typing starts from the other side, a dynamically typed program, and lets types be added to it in place. The rules for ? serve both directions, and the choice between them is about which programs a language’s users already have.

Further reading

Gradual typing: Siek and Taha’s “Gradual Typing for Functional Languages” (2006) defines ?, consistency, and the cast-inserting translation for a small functional language, and gives the run-time semantics of the casts. Tobin-Hochstadt and Felleisen’s “The Design and Implementation of Typed Scheme” (2008) describes a type system designed for programs first written without types, including the checks at module boundaries.

Contracts and blame: Findler and Felleisen’s “Contracts for Higher-Order Functions” (2002) introduces the wrappers and the assignment of blame, for contracts written by programmers. Wadler and Findler’s “Well-Typed Programs Can’t Be Blamed” (2009) connects them to casts between more and less precise types and proves the blame theorem.

Cost: Takikawa and colleagues’ “Is Sound Gradual Typing Dead?” (2016) gives the method for measuring every mixture of typed and untyped modules along with the Typed Racket results.

Concept checks