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 union types are of the form `T|U`

and are inhabited by values that
have type `T`

or `U`

. For example, `number|string`

is inhabited by all string
and numbers. Clearly, `T <: T|U, U <: T|U`

, and `T|U </: T`

and `T|U </: U`

.

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

typeTheSue = {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

typeSues =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

typeSubtype <S ,T > =S extendsT ? true : false;constsubtype_test1 :Subtype <{a : 1,b : 2}, {a : 1}> = true;constsubtype_test2 :Subtype <{a : 1}, {a : 1,b : 2}> = false;constType 'true' is not assignable to type 'false'.2322Type 'true' is not assignable to type 'false'.: subtype_test_bad Subtype <{a : 1}, {a : 1,b : 2}> = true;

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 constructor`Partial`

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

typePartial <T > = {[F in keyofT ]?:T [F ];};typePartialAnimal =Partial <{noise : string}>;

`[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

constsubtype_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

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

because, in particular,

ts

constsubtype_test5 :Subtype <{trees : 1}, {trees ?: 9}>= false;

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

ts

typeIsTheSue <Sue > =Sue extendsPartial <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 example`unknown`

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

typePickFieldA <T > =T extends {a : unknown} ?T ['a'] : never;typeAFields =PickFieldA <{a : 1}|{b : 2}|{a : 's'}>;constafields_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

typeSueC andidates = 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

typeAllT heSues = 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 `never`

s 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

typeSues WithNames = {[S in keyof Sues]: {name: S}&Sues[S];// produces rows of form "1: {name: 1, cats: 10, goldfish: 5, ...}" };typeAllTheSues = 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 complicatedHaving 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 `number`

s 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

typeTupToNum <T extends unknown[]> =T extends {length : inferN } ?N : never;consttup_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

typeNumToTup <N extends number,Tup extends unknown[] = []> =Tup extends {length :N } ?Tup :NumToTup <N , [...Tup , unknown]>;constnum_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

typeSubtract <A extends number,B extends number> =NumToTup <A > extends [...inferDiff , ...NumToTup <B >] ?TupToNum <Diff >: never;constsubtract_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

typeGreaterThan <A extends number,B extends number> =A extends 0 ?false :B extends 0 ? true :GreaterThan <Subtract <A , 1>,Subtract <B , 1>>;constgt_test1 :GreaterThan <2, 1> = true;constgt_test2 :GreaterThan <1, 1> = false;constgt_test3 :GreaterThan <1, 2> = false;typeLessThan <A extends number,B extends number> =B extends 0 ?false :A extends 0 ? true :LessThan <Subtract <A , 1>,Subtract <B , 1>>;constlt_test1 :LessThan <1, 2> = true;constlt_test2 :LessThan <1, 1> = false;constlt_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

typeCheckGreaterThan <F extends keyofTheSue ,T extends {[f inF ]?: number}> =T [F ] extends number ? {[f inF ]:GreaterThan <T [F ],TheSue [F ]>}&Omit <T ,F >:T ;typeCheckLessThan <F extends keyofTheSue ,T extends {[f inF ]?: number}> =T [F ] extends number ? {[f inF ]: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

typeExclude <T ,U > =T extendsU ? never :T ;typeOmit <T ,U > = {[F inExclude <(keyofT ),U >]:T [F ];};constomit_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

typePartialUnconstrained <T > = {[P in keyofT ]?: any;};typeSueCheckFieldsGreater <T extendsPartialUnconstrained <TheSue >> =CheckGreaterThan <'trees',CheckGreaterThan <'cats',T >>;typeSueCheckFieldsLesser <T extendsPartialUnconstrained <TheSue >> =CheckLessThan <'pomeranians',CheckLessThan <'goldfish',T >>;typeSueCheckFields <T extendsPartialUnconstrained <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* type`any`

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

typeSueCheckFieldsGreater <T extendsPartialUnconstrained <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

typeCheckedFields = 'trees'|'cats'|'pomeranians'|'goldfish';typeTheSueChecked =Omit <TheSue ,CheckedFields >&{[f inCheckedFields ]: 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

typeSues CheckedWith Names = {[S in keyof Sues]: {name: S}&SueCheckFields<Sues[S]>;};type AllTheSues =Sue sChecke dWithNames[keyof Sue sCheckedWithNames];type MatchingSue = Extract<AllTheSues, Partial<TheSueCh ecked >>['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

typeInit <T > =T extends [...inferI , infer_ ] ?I : never;functioninit <T extends unknown[]>(arr :T ) {returnarr .slice (0, -1) asInit <T >;}consta1 =init ([1, 'b'] as [1, 'b']);constaempty =init (a1 );constanever =init (aempty );

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

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

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.