Gradual Typing

I recently started a PhD at the Australian National University, doing research into gradually typed programming languages. Since I'm probably going to have to explain this a lot, I thought I'd write a quick explanation of what gradual typing is. In a future post I will then talk about what specifically I'm doing.

Static and Dynamic Types

In programming languages, there has long been a distinction between languages with static types, and those with dynamic types. Languages with static types want to know things about the program you're writing (e.g. x is a number, y is a Person record), and they'll refuse to run your code at all if it tries to do something that doesn't make sense (like adding a number to a Person). Languages with dynamic types, on the other hand, will happily run your program, but will fail part-way through if you do something invalid (like adding a number to a Person).

add a b = a + b
data Person = MakePerson
add MakePerson 10 -- Type checking fails, so this won't run at all

def add(a, b): return a + b
class Person:
  pass
add(Person(), 10) # Fails while the program is running, inside the add function

These each have their strengths, and their weaknesses.

Static typing is great for catching mistakes before you make them, but it forces particular structures on your programs. It's not enough to just write a correct program, you have to write a program that can be proven correct for all executions within the rules of the type system.

Dynamic typing is great for more exploratory programming, but there are a lot more ways to make mistakes. The flexibility of dynamic typing makes it possible to write programs without having to prove anything about them. During development this is particularly valuable, as it makes it easier to get rapid feedback without having to dot every "i" and cross every "t".

Gradual Types

At a high level, gradual type systems are an attempt to combine the benefits of both static and dynamic types. Systems with gradual types allow parts of your program to have static types, while other parts of your program can use dynamic types.

An example of a gradual type system is TypeScript, which has static types, but also includes an any type which behaves like a dynamic type.

const add = (a: any, b: any) => a + b // any type
class Person { }
add(new Person(), 10) // Passes the type check

const add = (a: number, b: number) => a + b // numbers now
class Person { }
add(new Person(), 10) // Type checking fails: a Person is not a number

These types are called "gradual" because these types allow you to start by using dynamic types during development, and then gradually add type annotations so the computer can help catch mistakes.

There are a few languages with gradual type systems at the moment (e.g. TypeScript; Python with mypy, pyright, or pyanalyze; Ruby with Sorbet; PHP; Dart).

In an academic setting, gradual typing is usually discussed in terms of the gradual guarantee, which I'll write about another time.