The Guarantees Your Type System Makes

Sound languages

If you search for type safety, one of the first results will be something talking about the concept of a “safe language”, so let’s start there. I found two popular definitions for what a safe language is.

The first from “The Practical Foundations of Programming Languages” book by Robert Harper:

From here, we roughly learn that:

• Processing a language can be divided into two stages: 1) the statics, it derives typing judgments to check if what you said is of a certain type actually is that type and 2) the dynamics, which is concerned with the evaluation of those programs.

• Types are there to predict aspects of the execution and ensure they make sense at runtime.

• The idea of a well-formed program: one that has passed parsing and type checking. We’ll refer to it as well-typed program, otherwise it is ill-typed which means that we know it is ill-behaved or can’t be proven to be well-behaved.

Now we know the first thing about type safety: it guarantees that the predictions made by the types are right.

But now I have more doubts! What are typing judgements? What is all of that well and ill behaved jargon?

Well, luckily for us, Harper defines a language as “safe language” if all well-typed programs are well-behaved, meaning they exhibit only behaviors predicted by the statics. The fulfillment of this property is what marks a language as safe or unsafe.Which I found often called sound or unsound because they don’t allow programs that break the rules of the language semantics. We’ll use both terms interchangeably.

The second one comes from the “Type Systems” paper by Luca Cardelli:

Here, he introduces the concept of trapped and untrapped errors: trapped errors stop computation immediately while untrapped errors don’t.For example, indexing an array outside of its bounds with runtime checks not available or jumping to a wrong address, where the memory there may not represent an instruction.

He also defines type safety and type soundness as separate:

Where forbidden errors are a set that includes all the untrapped errors and a previously defined subset of trapped errors.

Which is essentially the same idea seen from another perspective of the well-behaved programs that Harper talks about.

Let’s play with some examples to illustrate what we have introduced so far. Imagine this function defined in a fictitious language which has the property of being sound, meaning that well-typed programs are well-behaved at runtime.

fn add(a: Int, b: Int) Int {
    return a + b;
}

// This would result in a well-typed program.
let res = add(10, 314);

// This would result in an ill-typed program.
let res = add(10, "Some");

The expression add(10, 314) is sound because add requires its arguments to be of type Int and both 10 and 314 satisfy this requirement in our language; therefore the program is well-typed. The statics for Int would guarantee that the + operator will not get stuck and because of this, the program is thought of as not breaking the guarantees of the language.

By comparison, add(10, "Some") is ill-typed because "Some" does not have type Int nor it can be coerced to it, so it doesn’t satisfy the “context”. If we allowed this program to be executed it would fail to uphold the guarantees of the language and will get stuck in some unknown state. Another example would be:

fn add(a: Int, b: Str) Int {
    return a + b;
}

let res = add(10, "Some");

The program may or may not be well-typed depending on the statics of the language. There are two possibilities:

• There is a rule defined for + operator with Int and Str as operands, the program is well-typed and guaranteed not to get stuck.
• No such rule exists: the program is ill-typed and executing it would break the language guarantees represented by the types.

Let’s look at another example, think that the language is no longer sound:

fn div(a: Int, b: Int) : Int {
    return a / b
}

let res = div(10, 0);

This program is clearly well-typed, but to state that the language is sound we need to check the dynamics. We can determine if it is sound by how it handles this division by zero error:

• The dynamics do not define what happens in this failure case, it is an untrapped error: the language is unsound.
• This kind of error is accounted for in the dynamics of the language, it is a trapped error: the language is considered sound.

In practice, this is done with static and/or dynamic checks, with the latter being the most commonly found because it’s easier to implement: throwing errors, errors as values, crash-recovery, exceptions, panicking, choose your favourite.

There are more expressive type systems where it’s possible to detect errors like the example before at compile time, such as the ones that have dependent types like in Idris or F*, but the languages aren’t as adopted and I know little of about them.

It’s not easy to prove type soundness. Even if the language has a reduced set of keywords and features, it’s more of a combinatorial problem between each possible combination and how they interact.

In the process, the Preservation and Progress theorems are involved and the proofs for them obviously change depending on the language.

Division by zero strikes back

We’ll look at two snippets in Rust and C and compare what their specifications define the behaviour to be in front of this error and what ultimately ends up happenning when we execute implementations of the spec. This happens because type soundness is a property of the language and not the implementation!

fn div(a: u32, b: u32) -> u32 {
    a / b
}

fn main() {
    let res = div(10, 0);
    println!("{res}");
}

Here, we are use rustc, and executing the output results in a panic:

$ rustc -o main main.rs; ./main

thread 'main' (432991) panicked at main.rs:2:5:
attempt to divide by zero
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
with a full backtrace in:

If run it again with RUST_BACKTRACE=1 we can see the language’s built-in error handling machinery at work:

$ rustc -o main main.rs; RUST_BACKTRACE=1 ./main

thread 'main' (433803) panicked at main.rs:2:5:
attempt to divide by zero
stack backtrace:
   0: __rustc::rust_begin_unwind
             at /rustc/2286e5d224b3413484cf4f398a9f078487e7b49d/library/std/src/panicking.rs:690:5
   1: core::panicking::panic_fmt
             at /rustc/2286e5d224b3413484cf4f398a9f078487e7b49d/library/core/src/panicking.rs:80:14
   2: core::panicking::panic_const::panic_const_div_by_zero
             at /rustc/2286e5d224b3413484cf4f398a9f078487e7b49d/library/core/src/panicking.rs:175:17
   3: main::div
   4: main::main
   5: core::ops::function::FnOnce::call_once

Rust does not yet have a formal specification. The closest thing is the Rust Reference, in there we see that this behavior is defined by the language, it is a trapped error: division by zero does not result in undefined behavior but instead transitions the program to a specified error state where computation is stopped immediately Recovering from a panic like this can be done by using catch_unwind or avoided by using more idiomatic approaches, such as checked_div or encoding the invariants in the function’s type signature. .

Now with the C program, we first use GCC:

#include <stdio.h>

int div(int a, int b) {
    return a / b;
}

int main() {
    int res = div(10,0);
    printf("%d", res);
}

$ gcc -Wall -Wextra -Wpedantic -O0 -o main main.c && ./main

Floating point exception   (core dumped) ./main

We can use gdb to learn more about what happened:

$ gdb -q ./main -ex run -ex "set disassembly-flavor intel" \
     -ex disassemble -ex quit
...
Program received signal SIGFPE, Arithmetic exception.
0x0000555555555147 in div (a=10, b=0) at main.c:4
4           return a / b;
Dump of assembler code for function div:
   0x0000555555555139 <+0>:     push   rbp
   0x000055555555513a <+1>:     mov    rbp,rsp
   0x000055555555513d <+4>:     mov    DWORD PTR [rbp-0x4],edi
   0x0000555555555140 <+7>:     mov    DWORD PTR [rbp-0x8],esi
   0x0000555555555143 <+10>:    mov    eax,DWORD PTR [rbp-0x4]
   0x0000555555555146 <+13>:    cdq
=> 0x0000555555555147 <+14>:    idiv   DWORD PTR [rbp-0x8]
   0x000055555555514a <+17>:    pop    rbp
   0x000055555555514b <+18>:    ret
End of assembler dump.

We see that the fault came from our div function. Notice how at address 0x0000555555555147 the division is performed with the idiv instruction on x86_64. Since the divisor is zero, the CPU raises a #DE (Division Error) exception. The OS handles it by sending a SIGFPE signal to the program.

The latest publicly available C language specification defines this as undefined behavior (UB), which is to say anything could happenIt must have been fun debugging this. . Whether the program crashes, hangs, or produces unpredictable results depends on the implementation, the target architecture and the operating system running at the time. To be fair, Rust is not free of UB, although it is a lot less pervasive than in C since it’s largely confined to unsafe blocks.

This illustrates one reason why C is considered unsafe: even well-typed programs can reach runtime states that the language does not account for.

This behavior is a design decision, arguably influenced by the time and the purpose of the language. This allows compilers more freedom to do optimizations, which is great and makes your program faster, but it can end up changing the behavior of your program in ways you don’t expect.

To showcase this, let’s see three different implementations of C: GCC, Clang and Fil-C:

$ gcc -g -O3 -o main main.c && gdb -q ./main -ex run \
-ex "set disassembly-flavor intel" -ex disassemble -ex quit
...
Program received signal SIGILL, Illegal instruction.
main () at main.c:8
8           int res = div(10,0);
Dump of assembler code for function main:
=> 0x0000555555555020 <+0>:     ud2
End of assembler dump.

Now the fault comes from our main function. Inspecting the assembly we see that the compiler optimized the whole program to a ud2 instruction which generates a #UD (Invalid Opcode) exception. Now the program receives a SIGILL from the OS.

$ clang -O3 -o main main.c && ./main 
151705912 

$ clang -O3 -o main main.c && gdb -q ./main -ex "set disassembly-flavor intel" \
-ex "disassemble main" -ex quit
...
Dump of assembler code for function main:
   0x0000000000001150 <+0>:     push   rax
   0x0000000000001151 <+1>:     lea    rdi,[rip+0xeac]        # 0x2004
   0x0000000000001158 <+8>:     xor    eax,eax
   0x000000000000115a <+10>:    call   0x1030 <printf@plt>
   0x000000000000115f <+15>:    xor    eax,eax
   0x0000000000001161 <+17>:    pop    rcx
   0x0000000000001162 <+18>:    ret
End of assembler dump.

Without optimizations it behaves similarly to the GCC-compiled one. With optimizations enabled, Clang also deletes div; however, it doesn’t replace main’s body with a ud2 and instead continues execution normally, printing an arbitrary value!

Fil-CAt the time of writing, it is at version 0.678. is a fork of Clang 20.1.8 that adds static and runtime memory safety features to C (to explain how, I would need a series of articles):

$ ./build/bin/clang -g -O3 -o main main.c && ./main
0

This time, the Fil-C compiler ends up rewriting our program to always return 0.

What about dynamic languages?

Until now, we’ve always talked about types and static phases so it seems that we always have some kind of static analysis going on. It’s reasonable to wonder how any of this applies to dynamic languages, since we don’t have types there do we?

Dynamic languages are sometimes referred to as “untyped” languages, but the truth is that it’s types all the way down baby. Turns out, dynamic languages embrace a model of computation where multiple classes of values exist for a single recursive type. Harper addresses this:

In this kind of language, every value is tagged to indicate which class of value they belong through a process called Classification. Since the static phase only checks that the expression is well-formedHere “well-formed” only means that it passed parsing. and that there are no free variables in the expression; the dynamics must check for errors at runtime that would have never show up in a statically-typed language; this is called Class Checking and uses the tags each value has.

Knowing this, what happens to the theorems of Preservation and Progress? How do we talk about type soundness in this kind of languages?

Progress is expressed as:

$$d\ \mathrm{ok} \Longrightarrow (d\ \mathrm{val}) \lor (d\ \mathrm{err}) \lor (\exists\ d'.\ d \rightarrow d')$$

And there’s a Exclusivity lemma:

$$\forall\ d : \text{exactly one of } (d\ \mathrm{val}),\ (d\ \mathrm{err}),\ (\exists\ d'.\ d \rightarrow d')$$

Progress now reads as “If $d$ is a closed expression, then it’s either a value, results in a runtime error or it can be further evaluated”. Exclusivity states that, for any $d$ in the language, exactly one of these outcomes must be true at any given time.

In the previous model, these errors were guaranteed not to occur for well-typed programs. But, since catching those errors before evaluation requires static typing, now they have become part of the semantics of the language! This way, evaluation never becomes stuck.

Since there exists only one singular recursive type, Preservation plays lesser of a role here, there is no static type information to preserve between evaluations! The runtime, through Classification and Class Checking, enforces the discipline that guarantees safe evaluation.

It’s useful to look at an example in the wild. This single recursive type we mentioned can be found in the CPython Language Reference, where it defines a type called PyObject, where all object types are extensions of this type and one of its fields, ob_type, is a pointer to a PyTypeObject that encodes the object type which is exactly the idea of tagging a value to know which class of value they belong to.

Right now, it’s looking like the static typing bois have won: Python has static type checkers like mypy and ty. TypeScript is incredibly adopted and it’s essentially a static type system layer over Javascript. More recently, even Elixir has been working on adding a gradual type system!.

By now I believe we’ve talked enough of what type soundness is. It’s relevant to say that most languages are not completely sound, but ones try much harder than others. That’s why, when you evaluate a language, it’s interesting to see if what you need is in it’s sound subset.

We’ll now start to talk about more applied concepts, some more common than others, that different languages offer through the type system.

Subtyping

A subtype relation between types validates the subsumption principle:

This relation essentially enlarges the set of well-typed programs, allowing the type system to consider values of one type to be treated as values of another. Since an expression doesn’t fully reveal the information about the underlying value, proving safety is more delicate and the proofs of preservation and progress have to change.

This can sound familiar if you read about the SOLID principles, since Barbara Liskov’s substitution principle is indeed one definition of this subtyping relation and is key when making sense of class hierarchies.

To understand subtyping is useful to think in matters of behaviours. We’ll use $T <: S$ to show that $T$ is a subtype of $S$.

To work some quick examples, in languages with nominal typing like Java, one often needs to declare the relation explicitly:

class Spren {
    void fly() {}
}

class Bridgeman {
   void fly() {}
  
}

// We explicitly declare Herald as subtype of Spren.
// Herald <: Spren
class Herald extends Spren {
  void fly() { }

  void do_nothing() {}
}

// This works
Spren Jezrien = new Herald();

// Bridgeman has `fly()` but because we don't declare it
// as a subtype of Spren, it will fail to compile.
Spren Rock = new Bridgeman();

In contrast, TypeScript uses structural typing because it’s meant to work around Javascript, where anonymous objects are what is commonly used, so we can do things that are invalid in Java:

type Bridgeman = {
  run(): void;
};

type Herald = {
  fly(): void;
  do_nothing(): void;
  run(): void;
};

const jezrien: Herald = {
  fly() {},
  do_nothing() {},
  run() {},
};

const run = (b: Bridgeman) => {
  b.run();
};

// This works because subtyping is based solely on the type's members.
run(jezrien);

// This also works because the point of having structural typing in TS
// is to still be able to write Javascript.
run({
  run() {},
});

You can check more examples, even where TypeScript’s features are unsound, here.

This may look the same as duck typing in Python, but it is not. Structural subtyping in typescript is verified statically, while in duck typing there is no subtyping relation taking place, the program will attempt to call the required method function at runtime, and will fail and burn if it isn’t there: Python actually supports structural subtyping (named static duck-typing) in the shape of protocols. Check PEP 544

from io import BytesIO

class FakeFile:
    def __init__(self, content: bytes, name: str):
        self._buf = BytesIO(content)
        self.name = name

    def seek(self, pos):
        self._buf.seek(pos)


# I don't really care what file_like is, as long as it has a `read()` method.
def save_file(file_like, destination: str):
    with open(destination, "wb") as out:
        out.write(file_like.read())


with open("real.txt", "wb") as f:
    f.write(b"i am a real file")

with open("real.txt", "rb") as real:
    save_file(real, "out_real.txt")

fake = FakeFile(b"i am a duck", "duck.txt")
save_file(fake, "out_duck.txt")

$ uv run main.py

Traceback (most recent call last):
  File "/home/lautaro/Documents/Development/pypypy/main.py", line 25,
 in <module>
    save_file(fake, "out_duck.txt")
  File "/home/lautaro/Documents/Development/pypypy/main.py", line 15, in
 save_file
    out.write(file_like.read())
            ^^^^^^^^^^^^^^
AttributeError: 'FakeFile' object has no attribute 'read'

Subtyping is really there to make programs easier to write, but at the same time, makes it difficult to be sure that an expression has exactly the type it declares.

// TypeScript actually tries to automatically infer the variance given the
// position where the type parameter T appears in the signatures.
//
// The `out` keyword exists to explicitly tell the compiler that the relation
// is a _covariance_, so this:
type Secret<T> = {
  //  would be equivalent to:
  // type Secret<out T>
  reveal: () => T;
  toString: () => string;
};

function makeSecret<T>(value: T): Secret<T> {
  return {
    reveal: () => value,
    toString: () => "[REDACTED]",
    [Symbol.for("nodejs.util.inspect.custom")]: () => "[REDACTED]",
  };
}

type Credential = {
  owner: string;
};

type AccessToken = Credential & {
  scopes: string[];
};

const token: Secret<AccessToken> = makeSecret({
  owner: "service-account",
  scopes: ["read", "write"],
});

// Here, we see the constructor is _covariant_ because
// the subtyping "direction" remains the same:
//
// AccessToken <: Credential
//              |
//              V
// Secret<AccessToken> <: Secret<Credential>
const credential: Secret<Credential> = token;

console.log(credential);
// [REDACTED]

console.log(credential.reveal());
// { owner: "service-account", scopes: ["read", "write"] }

// The `in` keyword exists to explicitly tell the compiler that the relation
// is a _contravariance_, so this:
type Logger<T> = {
  //  would be equivalent to:
  // type Logger<in T>
  log: (a: T) => void;
};

type Event = {
  timestamp: number;
  source: string;
};

type Login = Event & {
  username: string;
  ip: string;
};

type Crash = Event & {
  signature: string;
  count: number;
};

const default_logger: Logger<Event> = {
  log(event) {
    const date = new Date(event.timestamp)
      .toISOString();

    console.log([date, event]);
  },
};

// Here, the constructor is _contravariant_ because the subtyping
// "direction" gets reversed:
//
// Login <: Event
//        |
//        V
// Logger<Event> <: Logger<Login>
const login_logger: Logger<Login> = default_logger;

// Crash <: Event
//        |
//        V
// Logger<Event> <: Logger<Crash>
const crash_logger: Logger<Crash> = default_logger;

login_logger.log({
  timestamp: Date.now(),
  source: "auth-service",
  username: "johnny",
  ip: "10.0.0.42",
});

crash_logger.log({
  timestamp: Date.now(),
  source: " ",
  count: 2040,
  signature: "JS::Value::isGCThing",
});

/// Since now we both produce and consume `V`, we have an _invariant_.
// This:
type KVStore<V> = {
  //  would be equivalent to:
  // type KVStore<in out V>

  data: Map<string, V>;
  get: (key: string) => V | undefined;
  set: (value: V) => string;
};

// This works just fine
const login_store: KVStore<Login> = {
  data: new Map<string, Login>(),

  get(key) {
    return this.data.get(key);
  },

  set(value) {
    const uuid_key = randomUUID();
    this.data.set(uuid_key, value);

    return uuid_key;
  },
};

// But this _will_ fail.
const event_store: KVStore<Event> = login_store;

$ deno check main.ts

# I cleaned it up a little bit:
TS2322 [ERROR]: Type 'KVStore<Login>' is not assignable to
type 'KVStore<Event>'.
  Types of property 'set' are incompatible.
    Type 'Event' is not assignable to type 'Login'.
# We can see that we no longer can do what we did when it was covariant:
     Type 'Event' is missing the following properties from type
     '{ username: string; ip: string; }': username, ip

type KVReader<out V> = {
  get: (key: string) => V | undefined;
};

type KVWriter<in V> = {
  set: (value: V) => string;
};

// KVStore remains invariant, but now we read and write on the
// same mutable state, but without having type errors by creating
// Readers and Writers!
type KVStore<V> = KVReader<V> & KVWriter<V> & {
  data: Map<string, V>;
};

const event_store: KVStore<Event> = {
  data: new Map<string, Event>(),

  get(key) {
    return this.data.get(key);
  },

  set(value) {
    const uuid_key = randomUUID();
    this.data.set(uuid_key, value);

    return uuid_key;
  },
};

function recordLogin(writer: KVWriter<Login>): string {
  return writer.set({
    timestamp: 0,
    source: "",
    username: "",
    ip: "",
  });
}

// Remember that Login <: Event and here we have:
//
// function registerLogin(writer: KVWriter<Login>): string
//
// KVWriter<Event> <: KVWriter<Login>
//
// We have Contravariance!
const key = recordLogin(
  event_store,
);

function debugEvent(key: string, reader: KVReader<Event>) {
  console.log(reader.get(key));
}

const login_store: KVStore<Login> = {
  data: new Map<string, Login>(),

  get(key) {
    return this.data.get(key);
  },

  set(value) {
    const uuid_key = randomUUID();
    this.data.set(uuid_key, value);

    return uuid_key;
  },
};

// KVReader<Login> <: KVReader<Event>
//
// Here we have Covariance!
debugEvent(key, login_store);

trait Rollable {
    fn roll(&self) -> u32;
}

struct Dice {
    name: &'static str,
    faces: u32,
}

impl Rollable for Dice {
    fn roll(&self) -> u32 {
        rand::random_range(1..=self.faces)
    }
}

// The trait object `dyn Rollable` is an _opaque_ value of a type that
// implements a certain set of traits. Because of its unknown size
// at compile time it is considered a _dinamically sized type_ and
// has to be used behind some type of pointer, in this case a `Box`.

// Each pointer of a trait object includes a pointer to an instance
// of the type `T` implementing the trait and a virtual method table
// (vtable) containing, for each method of `T`, a function pointer
// to `T`s implementation.
// Roughly something like this:

//                        HEAP
//   ┌────────────────────┐
//   │  data pointer      ├────────▶ ┌──────────────────┐
//   ├────────────────────┤           │   T instance     │
//   │  vtable pointer    ├─┐         │                  │
//   └────────────────────┘ │         │  (concrete data) │
//                          │         └──────────────────┘
//                          ▼
//     ┌─────────────────────────────┐
//     │    vtable for T: Rollable   │
//     ├─────────────────────────────┤
//     │  size                       │
//     ├─────────────────────────────┤
//     │  align                      │
//     ├─────────────────────────────┤
//     │  drop_in_place fn ptr       │
//     ├─────────────────────────────┤
//     │  ...                        │
//     ├─────────────────────────────┤
//     │  roll()  fn ptr ────────────┼─┐
//     └─────────────────────────────┘ │
//                                     ▼
//                       ┌───────────────────────┐
//                       │ Rollable::roll(&self) │
//                       └───────────────────────┘
//
fn roll(r: Box<dyn Rollable>) -> u32 {
    // Using a Trait object like `dyn Rollable` allows a late binding
    // of methods.

    // Calling `roll()` results in a function pointer being loaded from the trait object vtable and executed (dynamic dispatch).
    r.roll()
}

// Not to be confused with the `impl Trait` syntax, which works on _concrete_
// types so the usual static dispatch is used and causes no overhead.
fn roll_impl(r: impl Rollable) -> u32 {
    r.roll()
}

fn main() {
    for _ in 0..=3 {
        let dice = Dice {
            name: "D6",
            faces: 6,
        };
        let name = dice.name;
        println!("{} rolled: {}", name, roll(Box::new(dice)));
        // D6 rolled: 2
        // D6 rolled: 5
        // D6 rolled: 6
        // D6 rolled: 3
    }
}

Traits: Send/Sync

This is more Rust-specificIf unfamiliar, a trait describes an abstract interface that types can implement. It’s somewhat similar to a interface if you come from Java/C#. , but it’s a nice example of how we can use the type system to constraint what programs can be built.

If you’ve ever tried to do anything involving concurrency, you surely heard of both. The Nomicon tells us that Send and Sync are two special traits that govern how types are handled between threads.

Send declares that a type T can be transferred across thread boundaries (meaning it is acceptable for another thread to have a mutable reference &mut T), and T is Sync if and only if a reference to it (&T) is Send (meaning it’s okay for another thread to hold a reference &T).

Mix that with Rust’s ownership system that prevents a mutable reference to have more than one owner at once, and you have a recipe to make data races impossible. The compiler isn’t able to prevent resource races product of the preemptive schedulers of the underlying operating system.

Most types from the standard library are automatically Send, the exception being ones that can’t cross thread boundaries safely. A textbook example: Rc<T>, a reference-counting pointer, is !Send and !Sync because the count for how many references are there for T is non-atomic, so the compiler doesn’t allow you to use it across threads boundaries because it could cause data races.

fn main() {
    let bank_account = 10_000_000;
    let rc_bank = Rc::new(bank_account);

    // Trying to share a reference betweem threads
    // will cause a compile-time error because `Rc` is `!Sync` !
    thread::spawn(|| {
        do_something(&rc_bank);
    });
}

error[E0277]: `Rc<i32>` cannot be shared between threads safely
 --> src/main.rs:7:19
  |
7 |       thread::spawn(|| {
  |  _____-------------_^
  | |     |
  | |     required by a bound introduced by this call
8 | |         let _ = &rc_bank;
9 | |     });
  | |_____^ `Rc<i32>` cannot be shared between threads safely
  |
  = help: the trait `Sync` is not implemented for `Rc<i32>`
  = note: required for `&Rc<i32>` to implement `Send`

And if we tried to move the variable to another thread instead of sharing it, we would get the error:

error[E0277]: `Rc<i32>` cannot be sent between threads safely
 --> src/main.rs:7:19
  |
7 |       thread::spawn(move || {
  |       ------------- ^------
  |       |             |
  |  _____|_____________within this `{closure@src/main.rs:7:19: 7:26}`
  | |     |
  | |     required by a bound introduced by this call
8 | |         let _ = &rc_bank;
9 | |     });
  | |_____^ `Rc<i32>` cannot be sent between threads safely
  |
  = help: within `{closure@src/main.rs:7:19: 7:26}`, the trait
  `Send` is not implemented for `Rc<i32>`

A type being !Send doesn’t imply it is !Sync, remember that it only needs that a shared reference &T implements Send. MutexGuard is one type that is !Send and Sync because, for historical reasons, in platforms that use pthreads there is the requirement to release the lock on the same thread that first acquired it, so reading a reference to the lock is fine but giving ownership to another thread would break that guarantee.

fn main() {
    let bank_account = Arc::new(Mutex::new(10_000_000));
    let guard = bank_account.lock().unwrap();

    thread::scope(|s| {
        // This is fine because we are just passing around a shared reference
        s.spawn(|| read_or_something(&guard));

        // But the moment we try to give away ownership of the guard
        // we will have a compile error because the closure needs to be
        // `Send`
        s.spawn(|| {
            update_value(guard);
        });
    });
}

Would in turn, give you this error message:

error[E0277]: `std::sync::MutexGuard<'_, u32>` cannot be sent between threads safely
  --> src/main.rs:24:17
   |
24 |           s.spawn(|| {
   |             ----- ^-
   |             |     |
   |  ___________|_____within this `{closure@src/main.rs:24:17: 24:19}`
   | |           |
   | |           required by a bound introduced by this call
25 | |             update_value(guard);
26 | |         });
   | |_________^ `std::sync::MutexGuard<'_, u32>` cannot be sent between threads safely
   = help: within `{closure@src/main.rs:24:17: 24:19}`, the trait `Send` is not implemented for `std::sync::MutexGuard<'_, u32>`

In other languages Go, Java, etc.), the mutex and the protected data are different things, so correct usage relies on us having discipline (don’t try to unlock a free mutex!)If you want to read more why they look like that, read here . Here we can let the compiler do the work for us!

The opposite is also possible, the Cell<T> types are Send but !Sync since they provide “interior mutability” and can be mutated through a shared reference &T, contrary to the usual borrowing rules. So it’s okay to give away ownership of it, but the idea of multiple writers with no synchronization is not fun.

If you’ve used a multi-threaded work-stealing runtime like tokio, I’m sure you’ve seen the error demanding that every Future you await has to be Send. First, let’s see the signature of the Future trait:

pub trait Future {
    type Output;

//            Keep this in mind!
//                  │
//                  v
fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Self::Output>;
}

The reason behind that demand is that, at a high level, tokio uses a thread pool, starting worker-threads to execute tasks and assigning a local queue filled with them to each worker, all while maintaining one global queue.

When all the tasks in the worker’s queue were resolved, it will either attempt to pick more tasks from the global queue or will steal from the local queue of another worker. In both cases, the future will need to cross a thread boundary and later be polled. If we check the signature for the poll() function above, we see that it takes an exclusive reference &mut, that means we are giving away ownership of everything inside that future to another thread, exactly the purpose of the Send trait! This behaviour is according to tokio’s multi-threaded runtime, for !Send futures, tokio offers alternative runtimes.

ADTs

Algebraic Data Types (ADTs) is the name given to a composite data type(a type created by combining other types) where the building blocks are sum types and product types. Product types are the easier ones to understand because they are often the first ones any programmer encounters, be it in the shape of structs in C or dataclasses in Python.

Let’s say you are trying to build a service following the twelve factors and you have to model a config declaring where to store images locally:

type storage_settings = { base_path : string; base_url : string option }

Simple enough right? base_path tell us where the image is in the file system and base_url has the associated url to expose the asset if we wanted to. This is the simples product type because it expresses the product between the string and string option types, storage_settings could hold any combination of the two.

As it turns out, the requirements changed and we now need to also support storing images in the cloud:

type storage_settings = {
  base_path : string option;
  base_url : string option;

  (* Cloudflare's R2 information *)
  account_id : string option;
  secret_access_key : string option;
  auth_token : string option;
  bucket_name : string option;
  public_url : string option;
}

Now, the number of value combinations grew and every field is also an option because we don’t have any other way of expressing that some values aren’t needed if we choose to store images locally or in the cloud. We need a way to represent a value that could hold many different types at a time.

That’s where sum types come in. They are given a wide variety of names, from disjoint unions to tagged unions and variant types, but in our context are better understood as a data structure used to hold a value that can take one of several shapes at a given time. Reworking our example:

type r2_backend = {
  account_id : string;
  secret_access_key : string;
  auth_token : string;
  bucket_name : string;
  public_url : string option;
}

type filesystem_backend = {
  base_path : string;
  base_url : string option
}

type storage_settings =
  | Local of filesystem_backend
  | R2 of r2_backend

Now storage_settings can only ever be one of the two explicitly listed types at any given time, and we can stop abusing the option type!

ADTs are at their most useful when combined with pattern matching + exhaustiveness checks, which basically runs an algorithm that checks whether every variant in a sum type is taken care of:

let load_storage (settings : storage_settings) =
  match settings with
  | Local { base_path; base_url } -> ...
  | R2 { account_id; secret_access_key; auth_token;
   bucket_name; public_url } -> ...

Here the code will only compile if we make sure to consider every possible value settings can take! If in the future we add a third backend that isn’t handled we will get an error like:

File "main.ml", lines 33-37, characters 2-22:
33 | ..match settings with
34 |   | Local { base_path; base_url } -> ...
35 |   | R2 { account_id; secret_access_key; auth_token;
        bucket_name; public_url } -> ...
Error (warning 8 [partial-match]): this pattern-matching is not exhaustive.
  Here is an example of a case that is not matched: GoogleCloud

I can’t express enough how much I can miss this features. Currently I’m writing a fair amount of Go and I wish I had this.

Before, I didn’t elaborate on what the option type was because it was in fact a sum type! It’s often used as the replacement of the concept of nullability that many other languages still have:

(*
  The `'a` annotation is called alpha and is virtually the same as the `T`
  used in the examples using TypeScript above!
*) 
type 'a option =
  | None
  | Some of 'a

let get_env name =
  match Sys.getenv_opt name with
  | Some value -> Some value
  | None -> None

let port =
  match get_env "PORT" with
  | Some value -> value
  | None -> "8080"

let () =
  Printf.printf "Listening on port %s\n" port

Researching about ADTs was how I found the notion of Propositions as Types which was really interesting to learn:

On the surface, it describes a one-to-one correspondence between each proposition in a given logic and a type in the language, arguing that for each proof of a proposition, a corresponding program exists. Evaluating said program would be equivalent to simplifying the proof. In this model, sum types and product types would have the roles of logic OR and AND.Examples in OCaml

This is it! There are still a lot of things I didn’t cover, but I focused on those I’ve had experience with (that’s why I don’t give more examples using dynamic languages!).

I’m sure there are more interesting applications of types from languages like Haskell, Elixir, and Lisps like Clojure but I haven’t used them.

If you want to keep learning how to use types to write efficient software I can’t recommend enough to read the archive of Ted Kaminski, especially “The One Ring Problem”!

References

• Harper, Robert. (2016) Practical Foundations for Programming Languages. 2nd ed. Cambridge University Press.
• Cardelli, Luca. (1996) “Type Systems.” In The Computer Science and Engineering Handbook, edited by Allen B. Tucker, chapter 140.