A glimpse into the algebra of type systems

I just saw this very interesting video about writing programs which inherently make invalid state unrepresentable. This might be a very important concept to understand, specially if you are still learning or you have a background in languages which do not provide strong typing.

An "algebraic type system" in computer programming refers to a system that allows the construction of complex types from simple types using algebraic operations. These operations typically include sum (union) and product (combination) of types. Algebraic type systems are a powerful tool for modeling data in a way that leverages the type system of a programming language to enforce constraints and invariants about the data, thus making programs more robust and easier to reason about. Rust and TypeScript are two languages that utilize algebraic type systems in different ways.

Sum Types (Union Types)

Sum types, also known as union types or variants, allow a value to be one of several different types. This is analogous to an "or" operation in algebra. In programming, this is useful for modeling situations where a value can come from disparate types and the program needs to handle each type differently.

• Rust: Rust uses enum to define sum types. An enum in Rust can have variants, and each variant can optionally carry data of different types. This allows Rust to model complex data structures and patterns like state machines or optional values (e.g., the Option<T> type) in a type-safe manner.
• TypeScript: TypeScript has union types that are denoted by the | operator. This allows a variable to hold a value of one of several types, enabling the programmer to write flexible code while still maintaining type safety. For example, a variable could be defined to hold either a string or a number.

Product Types (Structural Types)

Product types allow the combination of several values into one compound value, where the "product" part comes from the idea of multiplying the possibilities of each component type to get the total possibilities for the compound type. This is useful for bundling related data together.

• Rust: Rust has structs that are used to create complex data types by combining values of multiple types. Each field of a struct can have a different type, allowing for the construction of rich, typed data structures.
• TypeScript: TypeScript uses interfaces and classes as its primary means of creating compound types. Interfaces in TypeScript are used to define the shape that objects should conform to, including the types of their properties and methods. Classes can implement interfaces and provide concrete implementations.

Algebraic Data Types in Programming

Algebraic Data Types (ADTs) in programming languages like Rust and TypeScript enhance type safety and expressiveness. They allow developers to model data in a way that makes invalid states unrepresentable, significantly reducing runtime errors. For example, in Rust, the compiler checks match expressions for exhaustiveness, ensuring that all possible variants of an enum are handled. In TypeScript, union types and type guards can be used to ensure that code correctly handles different types at runtime.

Both Rust and TypeScript leverage their type systems to provide compile-time guarantees about the behavior of the code, making the software development process more reliable and efficient. While the specifics of how they implement these features differ, the underlying principle of using types to enforce constraints and model complex data is a shared strength of both languages.

Let's go through an example that showcases the use of TypeScript's union types along with type guards to handle different types at runtime safely.

Example: Handling Different Shapes

Imagine you are working on a graphics application that can render different kinds of shapes. Each shape type (like Circle, Square) has its own set of properties. We want to write a function that takes a shape and prints its area, using union types for the shapes and type guards to distinguish between them at runtime.

Step 1: Define Shape Types with Union

First, we define the types for the shapes we are handling: Circle and Square. We then define a Shape type that is a union of these types.

type Circle = {
    kind: 'circle';
    radius: number;
};

type Square = {
    kind: 'square';
    sideLength: number;
};

// Union type for any shape
type Shape = Circle | Square;

Step 2: Implement Type Guards

TypeScript allows us to use user-defined type guards to check the type of a union type at runtime. A type guard is a function that returns a boolean and has a type predicate as the return type (arg is Type).

For our shapes, we can use the kind property to distinguish between them:

function isCircle(shape: Shape): shape is Circle {
    return shape.kind === 'circle';
}

function isSquare(shape: Shape): shape is Square {
    return shape.kind === 'square';
}

Step 3: Write a Function to Handle Shapes

Now, we write a function that takes a Shape and prints its area. We'll use the type guards to safely access the properties specific to each shape type.

function printArea(shape: Shape) {
    if (isCircle(shape)) {
        // TypeScript knows `shape` is a Circle here
        const area = Math.PI * shape.radius ** 2;
        console.log(`Area of the circle: ${area}`);
    } else if (isSquare(shape)) {
        // TypeScript knows `shape` is a Square here
        const area = shape.sideLength ** 2;
        console.log(`Area of the square: ${area}`);
    }
}

// Example usage
const circle: Circle = { kind: 'circle', radius: 2 };
const square: Square = { kind: 'square', sideLength: 3 };

printArea(circle); // Area of the circle: 12.566370614359172
printArea(square); // Area of the square: 9

This example shows how TypeScript's union types and type guards can be used to write safe, type-checked code that handles multiple types at runtime. By checking the kind property, we can tell TypeScript which type we are dealing with inside the if blocks, allowing us to access the properties unique to each type without risking a runtime error.