Union types

Motivation and Context

Discriminated union types are handled in a very fragile way in the disc_union_types.ml nanopass: {key: "A", value: int} | {key: "B", value1: string, value2: bool} is transformed into a sum type A of int | B of {value1: string, value2: bool} before typing.

Description

This MR aims at replacing this nanopass by extending the typer to make it understand union types (and singleton types were added in another MR), and turning them into sum types only after the typer. This makes the way union types are handled much more robust and uniform: there can be several keys (and they can be used in a dependent fashion), the coercions into a union or from a union are handled via the subtyping mechanism, etc.

This MR is only a first step, and does not attempt to provide all the possibilities that one could expect from union types, but only to replace the nanopass by a more solid foundations on which further improvements can be built. In particular:

• it has only been tested on disjoint unions (even though the syntax of unions has recently been extended to allow arbitrary unions), and the coercion from int | nat to nat | int may not be the one you expect; and
• in switches with fallthroughs (i.e. where not all cases finish with break or return), it may not strengthen the type of the variable even though it could be (because having fallthroughs means we can't strengthen the variables as much, computing exactly how much we can strengthen would be non-trivial, and it is unclear how the type errors resulting from weakened strengthening could be made comprehensible to the user).

Component

• compiler
• website
• webide
• vscode-plugin
• debugger

Types of changes

• Bug fix (non-breaking change which fixes an issue)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to not work as expected)
• Performance improvement (non-breaking change that improves performance)
• None (change with no changelog)

Changelog

feat(lang): Improves support for discriminant unions by adding union types.

A union type describes a value that can be one of several types. We use the vertical bar (|) to separate the types. For instance, int | string is the type of a value that can be either an int or a string.

const a = { a: 1 } as { a: int } | { b: bool };

Common Fields

When working with a union type of records, we can only access members common to all types in the union.

type Car = { 
  driver: string; 
  fuel: nat; 
}

type Bike = { 
  driver: string; 
  hasTrainingWheels: bool; 
}

const getDriver = (vehicle: Car | Bike): string => vehicle.driver;

If a value has the type Car | Bike, we can only access driver because it is the only member common to both types. We cannot access fuel or hasTrainingWheels without additional type checks, as accessing fuel on a Bike would result in a runtime error.

Discriminant Unions

A common pattern for using union types is to include a single field with a singleton type to distinguish between the types. This allows the type checker to infer the specific type in a conditional statement.

type IntValue = { typ: "INT"; x: int };
type StrValue = { typ: "STR"; s: string };

type Value = IntValue | StrValue;

All types in the Value union have a common field typ. Since typ is a singleton type, we can compare its value to determine the specific type being used. Here’s how to use a switch statement to narrow down the type:

const valueToInt = (val: Value): int => {
    switch (val.typ) {
        case "INT":
            return val.x;
        case "STR":
            return int(String.length(val.s));
    }
    return -1;
}

In this example, typ helps to discriminate between the IntValue and StrValue types, allowing us to safely access their specific fields.

Checklist:

• If a new syntax has been introduced, put a message on slack ligo-lsp
• Changes follow the existing coding style (use dune @fmt to check).
• Tests for the changes have been added (for bug fixes / feature).
• Documentation has been updated.
• Changelog description has been added (if appropriate).
• Start titles under ## Changelog section with #### (if appropriate).
• There is no image or uploaded file in changelog
• Examples in changed behaviour have been added to the changelog (for breaking change / feature).