Goal

The goal of this project is to prove that the TypeScript type system is sufficiently expressive to enable declaring types that type-check Rummikub Sets when given an array of literal tiles.

See Wikipedia - Rummikub for the rules of the game (specifically the definition of valid Runs and Groups).

// Should be ACCEPTED as a legitimate Run of tiles.
const example_runOf4StartingAt3: Set = [
    { color: red, num: 3 }
    , { color: red, num: 4 }
    , { color: red, num: 5 }
    , { color: red, num: 6 }
];

// Should be ACCEPTED as a legitimate Group of tiles.
const example_groupOf3WithTileNumber2: Set = [
    { color: red, num: 2 }
    , { color: green, num: 2 }
    , { color: blue, num: 2 }
];

// Should be REJECTED (yield compiler error)
const example_runOf4StartingAt3ButBroken: Set = [
    { color: red, num: 3 }
    , { color: red, num: 4 }
    , { color: red, num: 6 } // missing 5 breaks continuity
    , { color: red, num: 7 }
];

// Should be REJECTED (yield compiler error)
const example_groupOf3WithTileNumber2And3: Set = [
    { color: red, num: 2 }
    , { color: green, num: 2 }
    , { color: blue, num: 3 } // tiles in group need to have same number
];

// Should be REJECTED (yield compiler error)
const example_groupOf3WithRepeatedColor: Set = [
    { color: red, num: 2 }
    , { color: green, num: 2 }
    , { color: red, num: 2 } // colors in a group must be distinct
];

Using The Project

The real fun is experimeting with compile-time/IDE verification of various data declarations rather than running a program since this project is about exercising the type checker.

Open the source files under the /examples folder.

• Uncomment sections of code with INVALID and watch the failure.
• Attempt different patterns for groups and runs.
• Observe that valid Rummikub Sets pass type-checking and invalid Sets are rejected.
• If this does not give you goosebumps then one of the following is likely true
  • You already have significant experience with dependent typing.
  • You do not understand what is happening.
  • You do not care about the possibilities of static typing.
  • You are in a dark place or have lost all passion for software development. <-- Humour.
• From there move on to /models to observe the methodology.
• Only then come back and read the rest of this README.

Discussion

Overview

The experiment was a success in that the limited dependent typing (in the form of string and numeric literals as types) and conditional types of TypeScript were sufficiently expressive. The type declarations were relatively easy to write and reason about.

I did observe two shortcomings that were a natural result of the enormous unions generated by this method

• Opaque Error Messages - When a value fails to type-check assignability to a union of many types the compiler seems to have no recourse but to arbitrarily pick one of the types from the union and report the failure on that match. This is almost never helpful. As a result, compiler error messages are practically useless and the compiler output at each verification point becomes binary in usefulness (pass or fail).
• Slow Type Checking - Even with this small code base one can watch the CPU go nuts.

Number of Types

A Group consists of either 3 or 4 tiles with distinct colors and the same number. Since the colors can be in any order the number of concrete combinations

• 3 tiles = Choose 3 colors of 4 * Choose 1 number of 13 = (4 * 3 * 2) * 13 = 312
• 4 tiles = Choose 4 colors of 4 * Choose 1 number of 13 = (4 * 3 * 2 * 1) * 13 = 312

Therefore, there are 624 combinations represented as types in the union for a Group.

For a Run of tiles,

• 3 tiles = Choose 1 color of 4 * Choose 1 number of 11 = 44
• 4 tiles = Choose 1 color of 4 * Choose 1 number of 10 = 40
• 5 tiles = Choose 1 color of 4 * Choose 1 number of 9 = 36
• 6 tiles = Choose 1 color of 4 * Choose 1 number of 8 = 32
• 7 tiles = Choose 1 color of 4 * Choose 1 number of 7 = 28

Therefore, to support between 3 and 7 tile Runs requires 180 combinations as types.

Unioning Groups and Runs together yields 804 types for valid combinations of rummikub tiles. That is a lot of patterns for the type-checker to match.

Real World Trade-Off

In a real application I would likely not use this specific technique due to the compiler performance issues. While the technique allows the type system to better validate, the enormous wait introduced for the human developer is such that total quality would suffer (developers are the most important guardians of total correctness even in the presence of an awesome compiler). Furthermore, the 99% use case in an application is taking arbitrary input from the world (I/O) and validating/narrowing the understanding of the shape of that data so that it can be passed to other code that expects that refined shape i.e. not validating literals arrays.

The 99% use case of narrowing arbitrary Tile arrays to valid Rummikub Sets can be better accomplished by using a pattern of a Marker Type (similar to Marker Interfaces - used to carry compile-time type information) and Type Guards to protect/narrow unruly data into valid forms.

/**
 * This marker type exists only for compile-time verification. No run-time 
 * values actually have a member __kind.
 */
type GroupMarker = { __kind: "Group"; }

/** A group of tiles is an array of tiles that have been marked as a group. */
type GroupOfTiles = Tile<TileColor.Set, TileNumber.Set>[] & GroupMarker;

/** The type guard would then verify valid data and refine the type. */
function isGroupOfTiles(tiles: Tile<TileColor.Set, TileNumber.Set>[]): tiles is GroupOfTiles {
    // implementation ellided    
}

While I would not use the dependent typing pattern, the fact that TypeScript can handle this remains absolutely breathtaking.

Techniques Employed

Foundation

Union Type Mapping Behavior: Distribute Over

TypeScript Conditional Types allow for writing a type that produces another type from given type arguments. Conditional types therefore operate like type functions (taking types as arguments and producing a type as an output).

When a Union Type is applied to a Conditional Type (type function), the function is "distributed" over each member of the union i.e. applied to each memember and the results are themselves unioned together. This can behave like map or flatMap over types dependening on the output of the Conditional Type.

Please do not confused my use of the term "map" with Mapped Types which is an entirely distinct type system feature.

type UnionOfOneThruThree = 1 | 2 | 3;

/** Maps a literal number type to another data type. Observe that for a
 * single type match this yields a single type output. */
type NumberToType<Num> =
    Num extends 1 ? Date 
    : Num extends 2 ? string 
    : Num extends 3 ? boolean
    : never;

/** 
 * The result of applying the map to the union produces output with the same 
 * number of members as the input i.e. a union of three types. As such, in this case
 * the map looks like a map.
 **/
type ResultingTypes = NumberToType<UnionOfOneThruThree>;
// ResultingTypes = Date | string | boolean;

Type Flat Map Style Behavior With Unions

type UnionOfOneThruThree = 1 | 2 | 3;

/** 
 * In this case, a single literal type match produces a union type.
 */
type NumberToLetters<Num> =
    Num extends 1 ? "a" | "b" 
    : Num extends 2 ? "c" | "d" | "e"
    : Num extends 3 ? "f" | "g" | "h" | "i"
    : never;

/** 
 * When UnionOfOneThruThree is applied to the conditional type mapping NumberToLetters 
 * each of the three members is mapped to a union and that result is unioned together.
 * The number of members in the resulting typing far exceeds the number of members 
 * in the input type. This appears more like a flatMap over union types.
 **/
type ResultingLetters = NumberToLetters<UnionOfOneThruThree>;
// ResultingLetters = "a" | "b" | "c" | "d" | "e" | "f" | "g" | "h" | "i";

type UnionOfOneThruThree = 1 | 2 | 3;

/** 
 * Observe that for the case of 2 the output is _never_ which is the 0 type 
 * or empty set in set terms). 
 */
type NumberToLetters2<Num> =
    Num extends 1 ? "a" | "b" 
    : Num extends 2 ? never
    : Num extends 3 ? "b" 
    : never;

/** 
 * Building on the flatMap similarity observe that 2 produced an empty type and so 
 * did not yield any output. 
 * 
 * This then provides the ability to filter union types by having type cases that 
 * yield the empty (uninhabited) type. 
 **/
type ResultingLetters2 = NumberToLetters2<UnionOfOneThruThree>;
// ResultingLetters2 = "a" | "b";

Producing Tuples That Require The Same Value

Imagine you wanted to declare a tuple where both numeric values are the same.

The following will not work because it obviously allows for any number in the first and any number in the second position.

type FirstAttempt = [number, number];

If you had a limited set of numbers you might attempt to type parameterize the tuple.

type MyNums = 1 | 2 | 3 | 4;
type SecondAttempt<Num extends MyNums> = [Num, Num];

That will enable writing types that enforce the constraint

const myAttempt: SecondAttempt<2> = [2, 2];

However, observe that you had to provide a specific numeric type as an argument to the declaration of SecondAttempt. By attempting to make that usage more generic we lose the type safety we gained.

const myAttempt2: SecondAttempt<MyNums> = [2, 3]; // whoops

One solution is to use the distribution behavior over unions to generate the set of tuples where the value is the same.

type MyNums = 1 | 2 | 3 | 4;
type ProduceATuple<Num> =
    Num extends MyNums
    ? [Num, Num]
    : never;

type ThirdAttempt = ProduceATuple<MyNums>;
// [1, 1] | [2, 2] | [3, 3] | [4, 4]