TypeScript, a strongly typed superset of JavaScript, which introduces several powerful features specifically pertaining to type safety that enhance code quality and reduce errors. Among these, in this blog we look at Discriminated Unions. In this introductory blog post, we will explore Discriminated Unions in TypeScript, understand their foundation in Type Theory, and delve into how TypeScript’s compiler enforces type safety using these constructs. 

What are Discriminated Unions?

In TypeScript, unions allow you to define a type that could be one of several other types. For instance, a variable could be a number or a string.

However, Discriminated Unions take this concept a step further. They involve an object type with a common, single-field property — the discriminant. This discriminant is used to distinguish between other types in the union. 

Example of a Discriminated Union:

In the above example, have two interfaces, namely Circle and Square and a Type Union called Shape.

A simple application of Discriminated Unions

One common use case for Discriminated Unions is in function arguments. Let’s see how we can use our Shape union in a function. 

The TypeScript compiler understands the different types within the Shape union, allowing us to access the properties that are unique to each type safely. 

Why use Discriminated Unions?

Type Safety: They ensure safe usage of various types. 

Code Clarity: They provide clear insights into the types used. 

Maintainability:   Updating types in a Discriminated Union is straightforward. 

Relating Discriminated Unions to Type Theory

Type Theory, is a branch of mathematical logic which provides the theoretical underpinning for Discriminated Unions.  

Key Concepts in Type Theory:

Types: Types are the core concept of Type Theory. They are classifications that define the form and behaviour of data. 

Type Safety: This ensures that a program will not perform an operation on a type that it is not intended to handle. 

Algebraic Data Types: These are composite types, meaning they combine other types. They are fundamental in many functional programming languages. 

Discriminated Unions: A Type Theory Application

Discriminated Unions in TypeScript are an application of Algebraic Data Types, a concept from Type Theory. 

Breaking Down the Example: 

Recall our previous Shape example: 

In Type Theory, this is an example of a Sum Type (also known as a Variant or Tagged Union). Here’s why: 

Sum Types: They represent a choice between different types (in our case, Circle or Square). Each type in the union (Sum Type) can be distinguished using a tag (kind). 

Safety and Expressiveness: The TypeScript compiler uses the discriminant (kind) to safely determine the correct type. This ensures operations on these types align with their definitions, adhering to the principles of type safety. 

Pattern Matching: The switch statement in our getArea function is a form of pattern matching. It operates differently based on the type of the shape passed to it. 

The use of Type Theory concepts like Discriminated Unions in languages like TypeScript demonstrates how theoretical concepts are applied in real-world programming. It enhances code robustness and readability, which are critical for large-scale application development. TypeScript’s implementation of such concepts is a testament to how modern programming languages continue to evolve, bridging the gap between theory and practice. 

Type Guarding 

Discriminated Unions work seamlessly with TypeScript’s type guards, allowing the compiler to infer the correct type within a block of code. 

In the above example, the compiler understands the type of myShape in each branch of the if statement, eliminating the risk of accessing properties that don’t exist on the given type. 

The examples we’ve seen demonstrate a paradigm shift towards compiler-driven development. By utilizing TypeScript’s robust type system, developers are not just coding but also communicating with the compiler, ensuring that the intent of the code is clear and consistent with its behavior.