Pattern Matching With a Typechecker

I've been doing the 2015 Advent of Code puzzles, and today I came across Day 16 - Aunt Sue. The premise of the problem is you have a bunch of aunts named Sue, each of which you know some facts about, and you are searching for the aunt that matches a set of predetermined facts. The second part of the problem adds additional constraints that make the fact matching conditional rather than singleton.

This is a pretty simple pattern matching problem. While I was thinking about about it, I realized that it could be solved entirely within TypeScript's type system!

In this cc, we will cover how to do so - part 1 is pretty straightforward, part 2 requires some construction and is more interesting. The article will not attempt to assume you are previously familiar with TypeScript's type system, introducing semantics where needed. Understanding of subtyping is assumed.

The basis for this construction is TypeScript's treatment of primitive literals as subtypes of their primitive type (i.e. 1 <: number), a feature I am not aware any other mainstream programming languages haveThis feature is not strictly needed (i.e. you could form a similar construction in other languages by creating fresh types for the natural numbers), but it makes application of the approach much easier..

Prelude

As a quick note on notation, we use S <: T to mean S is a subtype of T and S </: T to mean S is not a subtype of T.

TypeScript intersection types are of the form T&U and are inhabited by values that have type T and U. For example, {a: number}&{b: number} is inhabited by all records with fields a and b, each of which is a number. T&U <: T, T&U <: U, and T </: T&U and U </: T&U.

Part 1

If you would like to follow along with this solution, I have provided a TypeScript playground with all the code. To see what types have been instantiated, simply hover over their name; for example, hovering on MatchingSue should yield 40.

For the full problem statement, please refer to the AoC (not AOC) link above. In short, we have a list of facts about the exact aunt Sue we are looking for, which we can express a record type:

ts
type TheSue = {
  children: 3,
  cats: 7,
  samoyeds: 2,
  pomeranians: 3,
  akitas: 0,
  vizslas: 0,
  goldfish: 5,
  trees: 3,
  cars: 2,
  perfumes: 1,
};

Observe that in children: 3, 3 is a type, not a value. It is a subtype of number inhabited by exactly one value, namely the number 3.

We are given 500 candidate aunt Sues, each of which we know a subset of facts about. We can express them all in a record type whose keys are the numbers 1-500 and whose entries are the facts of the corresponding Sue. 500 Sues are a lot, so the code block below hides the record type; to see part of it, hover over the Sues type.

ts
type Sues = SuesList;

The record of facts for each aunt Sue is indexed by a numeric reference (Sue 1, Sue 2), etc. Observe that the fields of facts known for each Sue is a subset of facts we know about the TheSue. Only one of these candidates' facts exactly match the corresponding facts associated with TheSue.

This means that not every Sue is a supertype of TheSue; for example, Sues[1], which has type {goldfish: 9, cars: 0, samoyeds: 9}, is not a subtype of TheSue because (for one) TheSue['goldfish'] = 5 </: 9 = Sues[1]['goldfish'].

To check the subtype relation, we can query TypeScript's typechecker via conditional types. The conditional type

typescript
S extends T ? A : B

Means if S is a subtype of (extends) T yield A; else, yield B. We define a Subtype predicate that yields true or false types based on the existence of subtyping relations. We use this to write subtyping tests checked by the compiler.

ts
type Subtype<S, T> = S extends T ? true : false;
const subtype_test1: Subtype<{a: 1, b: 2}, {a: 1}> = true;
const subtype_test2: Subtype<{a: 1}, {a: 1, b: 2}> = false;
const subtype_test_bad: Subtype<{a: 1}, {a: 1, b: 2}> = true;
Type 'true' is not assignable to type 'false'.2322Type 'true' is not assignable to type 'false'.

Back to the Sues. if there is an Sue that matches TheSue, their facts will be a supertype of TheSue, or said another way, their facts will be a subtype of TheSue with respect to only those facts (in fact, when only common fields are considered the types must be equal). So, for each Sue CandSue, we're going to "pick out" fields from TheSue just enough to match the fields of CandSue, producing a new type TheSueMatcher. Then, we check the subtype relation CandSue <: TheSueMatcher, and if it holds, CandSue is the Sue we seek.

What does this subtype check look like? Thanks to TypeScript's optional field syntax, wherein {a?: number} means "a record with field a of type string, or no field a at all", we can write a Partial type constructorPartial is generally provided directly by the TypeScript standard library. that given a record type T, will yield a supertype of T where all fields are optional:

ts
type Partial<T> = {
  [F in keyof T]?: T[F];
};
type PartialAnimal = Partial<{noise: string}>;
          type PartialAnimal = {
    noise?: string | undefined;
}

[F in keyof T]?: T[F] is a mapped type that means "for every key K of (the record type) T, make it an optional field whose value pair has the same type the value pair corresponding to K had in T".

Now, we can check if a candidate Sue is the one that we are looking for by checking whether it is a subtype of Partial<TheSue>. For example, we will have that

ts
const subtype_test3
  : Subtype<{trees: 9, cars: 4}, Partial<{trees: 9, cars: 4, akitas: 2}>>
  = true;

because all fields of the subtype match the fields of the supertype, and the unmatched fields of the supertype (namely akitas) are optional, so they do not have to be present in the subtypeNotice that it is also the case that Partial<{trees: 9, cars: 4, akitas: 2}> <: {trees: 9, cars: 4}. What does this say about the set properties of the TypeScript type system?. MoreoverA natural question is, why is trees not completely elided during the subtype comparison, forcing {trees: 1} <: {}? The reason is that the optional syntax (tries to be) structure preserving; informally, the checking algorithm for {a?: T} is "if a is not present, OK; else the type of a present must match T". Note that this is distinct from {a: T|undefined}, which has no type relationship with {a?: T}.,

ts
const subtype_test4
  : Subtype<{trees: 1, cars: 4}, Partial<{trees: 9, cars: 4, akitas: 2}>>
  = false;

because, in particular,

ts
const subtype_test5
  : Subtype<{trees: 1}, {trees?: 9}>
  = false;

So for a single Sue, we can define a type constructor

ts
type IsTheSue<Sue> = Sue extends Partial<TheSue> ? true : false;

that will yield true when passed the Sue we're looking for.

But we need a way to perform this check over 500 (!) candidates, so some control flow or parallel evaluation mechanism is required. We can get the latter using TypeScript's distributive conditional types. The idea is that when using a union type in a conditional type, the typechecker will distribute the conditional type over the union's variants. For exampleunknown is TypeScript's Top type - the type inhabited by every value. never is TypeScript's Bottom type - the type inhabited by no value. T|never = T because nothing can fit in never, so the values inhabited in T|never are only those inhabited in T., consider AFields below:

ts
type PickFieldA<T> = T extends {a: unknown} ? T['a'] : never;
 
type AFields = PickFieldA<{a: 1}|{b: 2}|{a: 's'}>;
const afields_test: Equals<AFields, 1|'s'> = true;

The construction of AFields proceeds roughly as follows:

text
AFields = (1 | 's') due to the expansion:
    PickFieldA<{a: 1}|{b: 2}|{a: 's'}>
  =   ({a: 1} extends {a: unknown} ? {a: 1}['a'] : never)
    | ({b: 2} extends {a: unknown} ? {b: 2}['a'] : never)
    | ({a: 's'} extends {a: unknown} ? {a: 's'}['a'] : never)
  = 1 | never | 's'
  = 1 | 's'

So we just need to feed a union of the 500 Sues into a conditional subtype check against Partial<TheSue> (for example, the IsTheSue constructor above), and we'll get the Sue we're looking for!

We can extract such a union from our Sues record type by mapping over all the keys of Sues:

ts
type SueCandidates = Sues[keyof Sues];

This says "index Sues by every key of Sues, and give be back all of those results". Clearly, this must be a union type, since we are extracting all of 500 individual types.

To understand how this works, let's perform a small expansion. Recall Sues is of the form

typescript
type Sues = {
  1: {goldfish: 9, cars: 0, samoyeds: 9},
  2: {perfumes: 5, trees: 8, goldfish: 8},
  /// 498 more Sues
};

Now, Sues[keyof Sues] becomes

typescript
  Sues[1|2|...|500]
=   {goldfish: 9, cars: 0, samoyeds: 9}
  | {perfumes: 5, trees: 8, goldfish: 8}
  | ...
  | Sues[500]

We could immediately do IsTheSue<Sues[keyof Sues]>, but this actually is not very useful! Thanks to distributive conditional types, IsTheSue<Sues[keyof Sues]> would yield false | false | ... | true | ... | false = boolean, and this gives us no information about who the actual Sue we were looking for is.

What we can do is something like this:

ts
type AllTheSues = Sues[keyof Sues];
type MatchingSue = Extract<AllTheSues, Partial<TheSue>>;

and MatchingSue would be a union of all Sues whose fields match corresponding ones in TheSue. To see why, let's expand this a bit:

typescript
type Extract<T, U> = T extends U ? T : never;
type AllTheSues = Sues[keyof Sues];
                = {goldfish: 9, cars: 0, samoyeds: 9}|{perfumes: 5, trees: 8, goldfish: 8}|...
type MatchingSue = Extract<AllTheSues, Partial<TheSue>>;
                 = never|never|...|{/* some sue that matches */}|...|never|never
                 = {/* some sue that matches */}

The nevers all collapse because they cannot be inhabited by a value and hence do not contribute to the union type; in the end we have just the Sue(s) we're looking for.

Well actually, we're not quite done, because part 1 of the problem asks us for the index number of the Sue in Sues that MatchingSue corresponds to. I am not aware of a way of to perform an inverse lookup of a non-primitive type in a record type, so we can't find the index of a Sue in Sues after it's been extracted. However, we can propagate the index of each Sue by adding it as an extra field on the info we know about each Sue before constructing their union and performing the matching:

ts
type SuesWithNames = {
   [S in keyof Sues]: {name: S}&Sues[S];
   // produces rows of form "1: {name: 1, cats: 10, goldfish: 5, ...}"
};
type AllTheSues = SuesWithNames[keyof SuesWithNames];
type MatchingSue = Extract<AllTheSues, Partial<TheSue>>['name'];
const matching_sue: MatchingSue = 40;

Finally, we have the name of the Sue we were looking for!

Part 2

If you would like to follow along with this solution, I have provided a TypeScript playground with all the code. To see what types have been instantiated, simply hover over their name; for example, hovering on MatchingSue should yield 241.

Hopefully Part 1 gave you a feel for the power and expressiveness of TypeScript's type system, and the relative ease by which we can perform singleton pattern matching with the TypeScript typechecker.

Part 2 of the problem is a bit more complicated⊕Having built familiarity with the type system and with more work to do in this part, we will move faster in our constructions.. Copying the problem statement (not visible unless you have correctly answered Part 1):

the cats and trees readings indicates that there are greater than that many ..., while the pomeranians and goldfish readings indicate that there are fewer than that many ...

Clearly, we can't compare singularly-inhabited primitive types anymore, as, for example, the value of cats in the Sue we wish to find can be any value greater than the value inhabited by TheSue['cats'] = 7. There is no way to formulate a type GT_N <: number where GT_N is inhabited only by numbers greater than some N -- not directly, anyway. Our approach will be to find a way to mark relevant fields (e.g. cats, pomeranians) in information known about each Sue as greater or less than the corresponding field in TheSue, and then perform the same subtype comparison as we did in Part 1 to find the matching Sue(s).

First, let's think about how we could perform greater/less than comparisons in the type system. In general, this comparison can be done between two integers by subtracting them and comparing the result to 0. There is no idea of numeric subtraction in the TypeScript type system itself, so we need to find some encoding for numbers on which we can perform an operation corresponding to subtraction.

With some thought, the most natural idea is to encode natural numbers with tuples. In TypeScript, a tuple type of the form [T_1, T_2, ..., T_N] holds N values where the t_i^th value has type T_i. Each tuple type has a length property whose type the number of type fields; in this case, N. We will use the length property to encode natural numbers; shortly, we will see how to exploit tuples for arithmetic operations.

To extract the natural number encoded in a tuple's length property, we define a type constructor:

ts
type TupToNum<T extends unknown[]> = T extends {length: infer N} ? N : never;
const tup_to_num_test : TupToNum<['a', true, 0.5]> = 3;

infer is arguably the most powerful construct provided by the TypeScript typechecker; it instructs the typechecker to construct a constraint to resolve an uninstantiated type (in this case, N), and to solve the constraint transparently. The typechecker is basically solving the type of N "for us"; it's like type reflection inside the type system! infer will be our best friend for this part.

To encode a number in a tuple, we can define a recursive type constructor that builds up a tuple until its length is that of the number we wish to encode:

ts
type NumToTup<N extends number, Tup extends unknown[] = []> =
    Tup extends {length: N} ? Tup : NumToTup<N, [...Tup, unknown]>;
const num_to_tup_test
  : Equals<NumToTup<3>, [unknown, unknown, unknown]> = true;

Now, we can define subtraction between A and B via a type constructor that queries the typechecker for the elements missing between the elements of A and B (let's call this Diff), and returns the length of Diff:

ts
type Subtract<A extends number, B extends number> =
    NumToTup<A> extends [...infer Diff, ...NumToTup<B>] ? TupToNum<Diff>: never;
const subtract_test: Subtract<5, 2> = 3;

Clearly, this only works with natural numbers and when A >= B, but that is good enough for our purposes of building greater than/less than comparators. Let's do that now, in both cases performing the comparison between two numbers by "walking them down" until one hits 0.

ts
type GreaterThan<A extends number, B extends number> = A extends 0 ?
    false :
    B extends 0 ? true : GreaterThan<Subtract<A, 1>, Subtract<B, 1>>;
 
const gt_test1: GreaterThan<2, 1> = true;
const gt_test2: GreaterThan<1, 1> = false;
const gt_test3: GreaterThan<1, 2> = false;
 
type LessThan<A extends number, B extends number> = B extends 0 ?
    false :
    A extends 0 ? true : LessThan<Subtract<A, 1>, Subtract<B, 1>>;
 
const lt_test1: LessThan<1, 2> = true;
const lt_test2: LessThan<1, 1> = false;
const lt_test3: LessThan<2, 1> = false;

Okay, now we're ready to apply all this to the problem. First, let's define type constructors that take a record type of facts we know about a Sue, a field to verify is greater than/less than that of the corresponding field in TheSue, and yield an updated record type with a boolean flag indicating the result of the verification on the checked field name. If the field we wish to verify against TheSue isn't present on the Sue record type we pass, we can just return the record type as it is, since that field can't be matched against TheSue for this Sue anyway.

ts
type CheckGreaterThan<F extends keyof TheSue, T extends {[f in F]?: number}> =
    T[F] extends number ? {[f in F]: GreaterThan<T[F], TheSue[F]>}&Omit<T, F>
                        : T;
 
type CheckLessThan<F extends keyof TheSue, T extends {[f in F]?: number}> =
    T[F] extends number ? {[f in F]: LessThan<T[F], TheSue[F]>}&Omit<T, F>
                        : T;

We use [f in F] to extract the properties we want to compare against TheSue. Since F <: keyof TheSue, in theory we could pass in a union type as F and get multiple fields to match against (e.g. if F = 'a'|'b', we have T extends {1?: number, 2?: number}), but in practice we will use single-union types here (like just one string variant). We cannot say {F?: number} directly, as then the field we are trying to match would be named F rather than the instantiated type of F.

Omit<T, U> is a type constructor that removes from the record type T those fields that are a subtype of U. Formally,

ts
type Exclude<T, U> = T extends U ? never : T;
type Omit<T, U> = {
  [F in Exclude<(keyof T), U>]: T[F];
};
const omit_test
  : Equals<Omit<{a: 1, b: 2, c: 3}, 'a'|'c'>, {b: 2}> = true;

The Omit provided by the TypeScript standard library has a differently-written definition, but the behavior is the same.

We perform {[f in F]: LessThan<T[F], TheSue[F]>}&Omit<T, F> (and similarly for GreaterThan) because once we have determined whether the checked field is indeed LessThan that of TheSue, we would like to return a fresh type with that data and all other data we already know about this Sue, sans the exact numeric type we knew about the field we just checked. In constructing CheckLessThan<'cats', {trees: 2, cats: 5}>, if the less than check yields false, the constructor yields {cats: false}&{trees: 2} (a type equivalent to {cats: false, trees: 2}). Keeping the checked field's numeric type would yield {cats: false}&{trees: 2, cats: 5} = never, as there is no value that can have a field cats whose value inhabits both false and 5.

Next, we define type constructors to take a record type of some Sue facts, compare its fields against those of TheSue for which we need to know greater than/less than relations, and yield a record type with that data.

ts
type PartialUnconstrained<T> = {
  [P in keyof T]?: any;
};
type SueCheckFieldsGreater<T extends PartialUnconstrained<TheSue>> =
    CheckGreaterThan<'trees', CheckGreaterThan<'cats', T>>;
type SueCheckFieldsLesser<T extends PartialUnconstrained<TheSue>> =
    CheckLessThan<'pomeranians', CheckLessThan<'goldfish', T>>;
 
type SueCheckFields<T extends PartialUnconstrained<TheSue>> =
    SueCheckFieldsLesser<SueCheckFieldsGreater<T>>;

The any type is inhabited by all values, but is more flexible than the unknown type in that values of any also inhabit every other typeany is an "escape hatch" from the type system, usually used to deal with the fact that variables are untyped in JavaScript. Here, our purpose is a little more sinister..

I leave as an exercise to the reader why the PartialUnconstrained bound is needed for the above type constructors, and why SueCheckFieldsGreater cannot be defined as

ts
type SueCheckFieldsGreater<T extends PartialUnconstrained<TheSue>> =
    CheckGreaterThan<'trees', T>&CheckGreaterThan<'cats', T>;

and what extra work would need to be done in order to define it in this way.

Next, we need to rewrite TheSue in a manner that it can be matched against the greater than/less than field constraints we recorded on each Sue record type via the SueCheckFields constructor. Since for the Sue that we want to find those greater than/less than field constraints should all be typed as true, let's redefine TheSue that way:

ts
type CheckedFields = 'trees'|'cats'|'pomeranians'|'goldfish';
type TheSueChecked = Omit<TheSue, CheckedFields>&{[f in CheckedFields]: true};

Finally, we perform the checking on each Sue, extract a union of them all, and yield a subtype comparison against TheSueChecked as in Part 1.

ts
type SuesCheckedWithNames = {
  [S in keyof Sues]: {name: S}&SueCheckFields<Sues[S]>;
};
type AllTheSues = SuesCheckedWithNames[keyof SuesCheckedWithNames];
type MatchingSue = Extract<AllTheSues, Partial<TheSueChecked>>['name'];
const matching_sue: MatchingSue = 241;

All done, without leaving the type checker!

Epilogue

I hope this cc provided you with a demonstration of the power of TypeScript's type system, and maybe gave you some ideas of how to exploit it in your own work.

I am not aware of other type systems in popular programming languages similar to those of TypeScript's in terms of reflection and the typing of primitive literals. Our treatment of tuples above was nice for encoding naturals, and can also give way to a weak kind of dependent typing.

ts
type Init<T> = T extends [...infer I, infer _] ? I : never;
 
function init<T extends unknown[]>(arr: T) {
    return arr.slice(0, -1) as Init<T>;
}
 
const a1 = init([1, 'b'] as [1, 'b']);
      
const a1: [1]
const aempty = init(a1);
        
const aempty: []
const anever = init(aempty);
        
const anever: never

While intriguing, it is unlikely that this kind of use case will ever make it as a first-class citizen in the type system.

The behavior of distributive conditional types may appear to be a little bit odd, as raw union types certainly don't distribute over type operationsValues inhabited by Obj include {b: 2}, so Obj cannot have a property a. In fact, values of type Obj have no typed properties until narrowed to know they have a field a or b.:

ts
type Obj = {a: 1}|{b: 2}|{a: 3};
type AsFromRaw = Obj['a'];
Property 'a' does not exist on type 'Obj'.2339Property 'a' does not exist on type 'Obj'. 
type PickA<T> = T extends {a: number} ? T['a'] : never;
type AsFromPick = PickA<Obj>;
         
type AsFromPick = 1 | 3

There are ways to get around this distributive behavior in conditional types, but they are outside the scope of this cc. Just know they are out there, and check them out if you're interested .

And don't worry - as all good things do, the TypeScript type system has holes. See raTS! for some; see the TypeScript issue tracker for many more.

Anyway, I hope you enjoyed this. Please email me if you have any comments.