Gradual Typing

Pros of static typing:

• Detects errors at compile time/gives early feedback
• Documents behavior of code
• Guaranteed absence of certain errors
• Faster execution because dynamic checks are unnecessary

Pros of dynamic typing:

• Expressiveness: not all correct programs are well-typed
• Concision: type annotations are more code to maintain
• Code changes require type changes/makes code harder to evolve
• Sometimes type of value depends on runtime information (e.g. deserialization)

• Key Idea: Allow mixing typed and untyped code
  • Use types for error detection, documentation, code navigation
  • Allow dynamically typed code as well
• Type system produces warnings, not errors
  • Maybe the program is correct
  • Maybe we didn’t encode enough of the types
• Depending on your perspective:
  • combines the error prevention power of static types with the flexibility of dynamic types
  • combines the type annotation overhead of static types with the runtime performance of dynamic types
• Increasing in popularity, particularly for dynamic languages
  • Maybe this means that static typing is better? Even dynamic languages want it?
  • On the other hand, people aren't switching away from Python and JavaScript

let x : number = 0;
let y : number = 1;
console.log(x + y);

1

let x : number = 0;
let y : string = "string";
console.log(x - y);

../../../../../tmp/babel-1qn5Ml/ts-src-DLsw4Z.ts(3,17): error TS2363: The right-hand side of an arithmetic operation must be of type 'any', 'number', 'bigint' or an enum type.
NaN

let x : number = 0;
let y : any = "string";
console.log(x - y);

NaN

function add(a: number, b: number): number {
    return a + b;
}
let x : number = 0;
let y : any = "string";
console.log(add(x, y));

0string

• When the types are annotated, we get a warning (note that the code still ran) when we violate the type discipline
• any tells the type system that a particular variable is always of the "right type", no matter the context
• This leads to strange behavior when an any value passes through a typed interface

function add(a: number, b: number): number {
    return a + b;
}
function sub(a: number, b: number): number {
    return a - b;
}
let x : number = 0;
let y : any = "string"; // upcast string to any
console.log(sub(add(x, y), 2)); // downcast any to number

NaN

1. This behavior (the code executing and returning NaN with no warnings) is fine.
2. We should raise an exception when sub returns?
3. We should raise an exception when add is called?

Jeremy Siek (inventor of gradual typing) describes 3 levels:

1. No checking.
2. Simple types are checked at implicit downcasts.
3. Complex types (functions, objects, etc) are "checked" at implicit downcasts. (We actually keep track of casts on complex objects until a simple type violation occurs, then we assign blame to the appropriate complex cast.)

• what does it mean for a gradually typed program to be sound?
  • clearly it can still experience type errors
• we say that a gradually typed program is sound if typed components can assume that their types accurately describe the values that they receive

• Start with simply typed lambda calculus (but we can extend these ideas to handle subtyping, references, etc)
• Add any type ?
• Examples of types:
  • \(\mathsf{Int} \rightarrow \que\)
  • \((\que \rightarrow \mathsf{Bool}) \rightarrow \mathsf{Int}\)
  • \(\mathsf{Int} \rightarrow (\que \rightarrow \que) \rightarrow \mathsf{Bool}\)

The grammar of types is as follows:

Note that the only addition (on top of simple types) is the any type, which we denote as \(\que\).

• Consider a function \(f : (\que \rightarrow \mathsf{Bool}) \rightarrow \mathsf{Int}\)
  • What types can we pass as an argument to \(f\)?
    • \(\que \rightarrow \mathsf{Bool}\) (yes)
    • \(\mathsf{Int} \rightarrow \mathsf{Bool}\) (yes)
    • \(\mathsf{Int} \rightarrow \mathsf{Int}\) (no)
    • \(\mathsf{Int} \rightarrow \que\) (yes)
• Formalize this as a relation \(\tau \sim \tau'\)
  • Reflexive (just like subtyping)
  • Symmetric (not like subtyping)
  • Not transitive. Why not?
    • \(\mathsf{Int} \sim \que\) and \(\que \sim \mathsf{Bool}\) but \(\mathsf{Int} \not \sim \mathsf{Bool}\)

• very few changes from simply typed lambda calculus (STLC)—only changes appear in application rules
  1. a function of any type can be applied to anything, producing any
     • why do we have to prove that \(e'\) has a type at all? if \(e'\) does not type, then we will reject the program
  2. functions with arrow type can be applied if their argument is compatible with their type

• remember the different levels of gradual typing?
• if we erased the types, we'd get something like level 1—standard semantics for the lambda calculus, and sometimes our programs would get stuck
• can we get type errors at runtime instead of getting stuck? what would that require?
• we'll use our type system to decide where to insert runtime casts
  • a cast (written \(\langle \tau \rangle e\)) first evaluates \(e\) to \(v\), then checks that \(v\) is consistent with \(\tau\) (and potentially modifies/casts \(v\))

• Where do we need to insert runtime casts?
• We'll insert them when we perform applications
  • this is the only place in the STLC where we have a type equality constraint (between function and argument type)
• three cases of interest
  1. function is of any type: cast function so that it accepts the correct rhs type. returns any
     1. How can we check this cast? We can't determine that a function value has the right type (without precise type annotations that we don't have). Are we doing something wrong here?
        1. No. We'll see in the dynamic semantics that this cast gets pushed inside the function during evaluation
  2. function is of arrow type and argument is compatible but not equal: cast argument to correct type
  3. standard application: no casts

• Extend our syntax of values with a special error value
• Casts are checked at runtime using the type system (but we could also annotate values with their type)
• When a cast fails, we emit the error value, which propagates up

• \((\lambda f : \que \rightarrow bool.\ not\ (f 1))\ (\lambda x: int.\ iszero\ x)\)
• first, cast insertion
  • first, insert on lhs
    • \((\lambda f : \que \rightarrow bool.\ not\ (f (\langle \que \rangle 1)))\)
  • next, insert on rhs
    • nothing needs to be done
  • finally, insert on application
  • what is the type of the lhs? \(not : bool \rightarrow bool\), \(iszero : int \rightarrow bool\)
    • \((\que \rightarrow bool) \rightarrow bool\)
  • what is the type of the rhs?
    • \(int \rightarrow bool\)
  • which rule matches? I-App-2
  • therefore, insert cast \((\lambda f : \que \rightarrow bool.\ not\ (f (\langle \que \rangle 1)))\ (\langle \que \rightarrow bool \rangle (\lambda x: int.\ iszero\ x))\)
• now for evaluation
  • \((\lambda f : \que \rightarrow bool.\ not\ (f (\langle \que \rangle 1)))\ (\langle \que \rightarrow bool \rangle (\lambda x: int.\ iszero\ x))\)
  • \((\lambda f : \que \rightarrow bool.\ not\ (f (\langle \que \rangle 1)))\ (\lambda y:\que.\ \langle bool \rangle((\lambda x: int.\ iszero\ x)\ (\langle int \rangle y)))\)
  • \(not\ ((\lambda y:\que.\ \langle bool \rangle((\lambda x: int.\ iszero\ x)\ (\langle int \rangle y)))\ 1)\)
  • \(not\ (\langle bool \rangle((\lambda x: int.\ iszero\ x)\ (\langle int \rangle 1)))\)
  • \(not\ (\langle bool \rangle((\lambda x: int.\ iszero\ x)\ 1))\)
  • \(not\ (\langle bool \rangle(iszero\ 1))\)
  • \(not\ (\langle bool \rangle false)\)
  • \(not\ false\)
  • \(true\)
• \((\lambda x: \que.\ iszero\ x)\ true\)
  • cast insertion
    • \((\lambda x: \que.\ iszero\ (\langle int \rangle x))\ (\langle \que \rangle true)\)
  • eval
    • \((\lambda x: \que.\ iszero\ (\langle int \rangle x))\ (\langle \que \rangle true)\)
    • \((\lambda x: \que.\ iszero\ (\langle int \rangle x))\ true\)
    • \(iszero\ (\langle int \rangle true)\)
    • \(iszero\ CastError\)
    • \(CastError\)

• getting the soundness guarantee costs performance (sometimes a lot of performance)
• why? insertion of runtime type checks
• unsound gradual typing does not pay this cost, so this might explain why typescript chose not to check types
  • (also, the impact of type errors on dynamic languages already low)
• some of this overhead is caused by extensive runtime checks
  • can mitigate these by switching from a structural type system to a nominal one (see "Sound Gradual Typing is Nominally Alive and Well" Muehlboeck & Tate, 2017)
    • but this causes a significant loss of expressiveness (it discards parametric polymorphism, for example)

Source: "Is sound gradual typing dead?" Takikawa et al., 2016

• The formalism for gradual typing in these notes comes from "Gradual Typing for Functional Languages" Siek & Taha, 2006 (with minor changes and simplifications). This is a very readable paper from the inventor of gradual typing.