Type-level Arithmetic in TypeScript: Part 1 - Type Safe Time Intervals


TypeScript is a statically typed language that allows you to define your own types. This is useful for many reasons, but one of the most powerful features of TypeScript is the ability to manipulate types in a similar way to how we manipulate values, known as type-level programming. In this article, we will explore the power of type-level arithmetic in TypeScript by implementing some type-level date arithmetic.
A lot of articles about type-level arithmetic in TypeScript already exist, but they often focus on operations like addition, subtraction, multiplication, and division. Some funny articles even show how to derive the parity (odd or even) of an integer at compile time, for example using a type-level subtraction operation.
In this article, we will rather focus on comparing numbers at the type-level, which can be useful in a variety of situations. We will use this to write a type that can validate the chronology of two times in a day at compile time. We will also cover a more "philosophical" aspect of type-level programming in TypeScript, which is the importance of writing clear and concise types that are easy to understand and maintain and do not cause the TypeScript transpiler to crash.
A simple type for a subset of natural numbers
As almost every type-level arithmetic in TypeScript, we will enjoy the power of conditional types along with the fact that TypeScript allows us to define recursive types. Moreover, the golden jewel of the type derivation is the fact that in TypeScript, given a type-level array T extends Array<unknown>
, the literal type T["length"]
is a valid numeric literal type that represents the length of the array. This allows to accumulate and iterate over numbers at compile time, since classical arithmetic operations are not available at the type level.
Without any further ado, let's define a type that represents a natural number between 0
and N-1
using this technique:
type NaturalLessThan<
N extends number,
Result extends Array<unknown> = [],
> = Result["length"] extends N
? Result[number]
: NaturalLessThan<N, [...Result, Result["length"]]>;
This type is a recursive type constructor that takes two type parameters: N
and Result
. The first parameter, N
, is the type that represents the upper bound of the range of natural numbers we want to represent. The second parameter, Result
, is an array that will contain the numbers from 0
to N-1
. Recursively, starting from an empty array, it will add a new number to Result
, namely its length, until this length is equal to N
. At this point, the Result
type is returned as Result[number]
, which evaluates to the union of all the numeric literals in the array.
To make it more clear, let's see how this type works in practice:
type ZeroToFour = NaturalLessThan<5>; // 0 | 1 | 2 | 3 | 4
Let's now decompose the type ZeroToFour
, by writing down the value of the return type at each iteration of the recursive type:
// iteration 1
NaturalLessThan<5, []> // Result[number]: never
// iteration 2
NaturalLessThan<5, [0]> // Result[number]: 0
// iteration 3
NaturalLessThan<5, [0, 1]> // Result[number]: 0 | 1
// iteration 4
NaturalLessThan<5, [0, 1, 2]> // Result[number]: 0 | 1 | 2
// iteration 5
NaturalLessThan<5, [0, 1, 2, 3]> // Result[number]: 0 | 1 | 2 | 3
// iteration 6, achieving convergence
NaturalLessThan<5, [0, 1, 2, 3, 4]> // Result[number]: 0 | 1 | 2 | 3 | 4
Simple, right? Now that we have a type that can represent a range of natural numbers between 0
and N-1
, we can use it to define a type that represents natural number between Min
and Max
, simply by excluding the numbers between 0
and Min-1
from the numbers between 0
and Max-1
thanks to the Exclude
utility type:
// TypeScript reminder: type Exclude<T, U> = T extends U ? never : T;
type NaturalWithin<Min extends number, Max extends number> = Exclude<
NaturalLessThan<Max>,
NaturalLessThan<Min>
>;
Comparing numbers at compile time
Great! Now that we have a type that can represent a range of natural numbers between Min
and Max
, we can use it to compare numbers at compile time.
type IsLessThanOrEqualTo<
X extends number,
Y extends number,
Result extends Array<unknown> = [],
> = Result["length"] extends X
? true
: Result["length"] extends Y
? false
: IsLessThanOrEqualTo<X, Y, [...Result, unknown]>;
This type is a recursive type constructor that takes three type parameters: X
, Y
, and Result
. The first two parameters, X
and Y
, are the numbers we want to compare. The third parameter, Result
, is an array that will contain X
elements. Recursively, starting from an empty array, it will add a new element to Result
until the length of Result
is equal to X
or Y
. At this point, the type will return true
if the length of Result
is equal to X
(in which case X
is less than or equal to Y
), false
if the length of Result
is equal to Y
(in which case X
is greater than Y
), or continue the recursion otherwise.
Let's see how this type works in practice:
type IsThreeLessThanOrEqualToFive = IsLessThanOrEqualTo<3, 5>; // true
type IsFiveLessThanOrEqualToThree = IsLessThanOrEqualTo<5, 3>; // false
type IsThreeLessThanOrEqualToThree = IsLessThanOrEqualTo<3, 3>; // true
I encourage you to decompose the type IsLessThanOrEqualTo
by writing down the value of the return type at each iteration of the recursive type, as we did for the NaturalLessThan
type in the previous section.
This type is actually the more complex of the article. The rest is just a matter of combining the types we defined so far to unlock the complete machinery. For example, we can now easily write the following type for strict inequality:
type IsLessThan<X extends number, Y extends number> =
IsLessThanOrEqualTo<X, Y> extends true ? (X extends Y ? false : true) : false;
or even these types for opposite inequality:
type IsGreaterThanOrEqualTo<
X extends number,
Y extends number,
> = IsLessThanOrEqualTo<Y, X>;
type IsGreaterThan<X extends number, Y extends number> = IsLessThan<Y, X>;
Note that in all these types, we are using number
as a type parameter. In order to make it more type-safe, we could use the NaturalLessThan
type to restrict the type parameter to a natural number, which would moreover avoid very deep recursion in the type derivation, since this type is bounded by design.
A type for a time in a day
Now that we have got the hang of it, let's use our basic arithmetic types to represent time! The first bricks we need are the types that represent the hours and the minutes in a day:
type Hour = NaturalWithin<0, 24>; // 0 | 1 | 2 | ... | 23
type Minute = NaturalWithin<0, 60>; // 0 | 1 | 2 | ... | 59
Now that we have the types that represent the hours and the minutes in a day, we can define a type that represents a time in a day:
type Time = {
hour: Hour;
minute: Minute;
};
Wonderful! Now that we have a type that represents a time in a day, we can use it to define a type that represents a time interval in a day:
type TimeIntervalNaive = {
start: Time;
end: Time;
};
As its name suggests, this type is naive. Can you notice the problem with it? Indeed, the start
time can be after the end
time, which is not what we want. To fix this, we can define a type that represents a time interval in a day where the start
time is before the end
time.
Let's start by building a type that checks if a time is before another time:
type IsTimeLessThan<Start extends Time, End extends Time> =
Start["hour"] extends End["hour"]
? IsLessThan<Start["minute"], End["minute"]>
: IsLessThan<Start["hour"], End["hour"]>;
This type is a conditional type that checks if the hour
of the start
time is equal to the hour
of the end
time. If it is, it checks if the minute
of the start
time is less than the minute
of the end
time. If it is not, it checks if the hour
of the start
time is less than the hour
of the end
time.
Now, we can write our chronology-safe Holy Grail type for time intervals in a day:
type TimeInterval<Start extends Time, End extends Time> =
IsTimeLessThan<Start, End> extends true ? { start: Start; end: End } : never;
Let's test our brand new type with some examples:
type TimeInterval1 = TimeInterval<{ hour: 12; minute: 30 }, { hour: 13; minute: 0 }>;
// { start: { hour: 12; minute: 30 }; end: { hour: 13; minute: 0 } }
type TimeInterval2 = TimeInterval<{ hour: 13; minute: 0 }, { hour: 12; minute: 30 }>;
// never
type TimeInterval3 = TimeInterval<{ hour: 12; minute: 30 }, { hour: 12; minute: 30 }>;
// never
type TimeInterval4 = TimeInterval<{ hour: 12; minute: 30 }, { hour: 12; minute: 29 }>;
// never
type TimeInterval5 = TimeInterval<{ hour: 12; minute: 30 }, { hour: 12; minute: 31 }>;
// { start: { hour: 12; minute: 30 }; end: { hour: 12; minute: 31 } }
The type works as expected! We have successfully implemented a type that can validate the chronology of two times in a day at compile time, only by combining small composable building blocks. Beautiful, isn't it?
Bonus: every time interval of a day
Now we have our super magic type for time intervals in a day, we can play a little bit and use it to define a type that contains every time interval in a day.
type TimeIntervalsOfDay = {
[StartHour in Hour]: {
[StartMin in Minute]: {
[EndHour in Hour]: {
[EndMin in Minute]: TimeInterval<
{ hour: StartHour; minute: StartMin },
{ hour: EndHour; minute: EndMin }
>;
};
};
};
};
This apparently simple type is actually very heavy for the TypeScript compiler, since it has to iterate over all the possible time intervals in a day. This is why it is important to be careful when writing complex types, as we will see in the next section. A first optimisation would be to rewrite it like this:
type TimeIntervalsOfDay = {
[StartHour in Hour]: {
[StartMin in Minute]: {
[EndHour in NaturalWithin<StartHour, 24>]: {
[EndMin in EndHour extends StartHour
? NaturalWithin<StartMin, 60>
: Minute]: TimeInterval<
{ hour: StartHour; minute: StartMin },
{ hour: EndHour; minute: EndMin }
>;
};
};
};
};
This way, we eliminate almost every impossible time intervals at an early stage, like the ones where the end
hour is before the start
hour.
Let's now play with our new type:
type TimeIntervalOfDay1 = TimeIntervalsOfDay[12][30][13][0];
// { start: { hour: 12; minute: 30 }; end: { hour: 13; minute: 0 } }
type TimeIntervalOfDay2 = TimeIntervalsOfDay[13][0][12][30];
// does not compile since property 12 does not exist in part of the type under the path 12 -> 30
type TimeIntervalOfDay3 = TimeIntervalsOfDay[12][30][12][29];
// does not compile since property 29 does not exist in part of the type under the path 12 -> 30 -> 12
type TimeIntervalOfDay4 = TimeIntervalsOfDay[12][30][12][30];
// interesting case: compiles but returns never
The last case is interesting: the type TimeIntervalsOfDay[12][30][12][30]
compiles, but it evaluates to never
. This is because the type TimeIntervalsOfDay
, in the fourth level of nesting, we used NaturalWithin<StartMin, 60>
instead of something like NaturalWithin<Add<StartMinute, 1>, 60>
. By the way, this raises two interesting exercices for the reader: first, write the type Add
that adds two (natural) numbers at compile time (easy), and second, to avoid repeating 24 and 60 in the type TimeIntervalsOfDay
, write the arithmetic Max
type that derives the maximum number of a union of natural numbers (harder, not sure it's even possible).
However, this type is still very complex for the TypeScript compiler, and it is not recommended to use it in a real-world application (imagine if we also had to consider the seconds in a day!). Use the type TimeInterval
we defined earlier instead, or, if you really need hours and minutes "decomposed" in a type, use the following type instead:
type TimeIntervalOfDay<
StartHour extends Hour,
StartMin extends Minute,
EndHour extends NaturalWithin<StartHour, 24>,
EndMin extends EndHour extends StartHour
? NaturalWithin<StartMin, 60>
: Minute,
> = TimeInterval<
{ hour: StartHour; minute: StartMin },
{ hour: EndHour; minute: EndMin }
>;
// Usage
const timeInterval: TimeIntervalOfDay<12, 30, 13, 0> = {
start: { hour: 12, minute: 30 },
end: { hour: 13, minute: 0 },
};
Avoid the trap of excessive complexity
The type system of TypeScript is (accidentally) Turing complete (meaning it can simulate any theoretically calculable computation, as it possesses the capabilities for conditional checks and recursive types necessary to emulate any Turing machine), which means that it is possible to write types that result in computations that do not terminate. This is why it is important to be careful when writing complex types. In this article, we have used recursion to define types that represent natural numbers and compare numbers at compile time. We have also used conditional types to define types that represent times in a day and time intervals in a day. These types are simple and should not cause any issues. However, it is important to be aware of the limitations of the type system and to proceed with caution.
As a type-level developer in TypeScript, you undoubtedly have ever encountered the error message Type instantiation is excessively deep and possibly infinite
. This error message is a clear sign that the type system is not able to terminate the type derivation.
Moreover, when writing complex conditional and mapped types, the compiler is not able to inform you that the type is not in its simplest form. For example, while writing this article, I came up writing the following type:
type IsEqualDummy<X extends number, Y extends number> =
IsLessThanOrEqualTo<X, Y> extends true
? IsGreaterThanOrEqualTo<X, Y> extends true
? true
: false
: false;
whereas the type IsEqualDummy
is equivalent to the following type (note that this type is generalisable to any type T
, not only numbers, but with precautions, like checking the extends
relation in both directions):
type IsEqual<X extends number, Y extends number> = X extends Y ? true : false;
Another example of unnecessary complexity is the following type:
type IsTimeLessThan<Start extends Time, End extends Time> =
IsLessThan<Start["hour"], End["hour"]> extends true
? true
: IsEqual<Start["hour"], End["hour"]> extends true
? IsLessThan<Start["minute"], End["minute"]>
: false;
whereas it can be simplified, as we did previously in the article.
Finally, not every developer is familiar with advanced type-level programming in TypeScript, and it can be difficult to understand complex types. It is important to write clear and concise types that are easy to understand (and document them precisely). This will make it easier for other developers to work with your code and will help prevent errors (and ease debugging) in the future. Anyway, type safety should never be sacrificed for the sake of over-simplification: everything is a matter of balance. Moreover, with the meteoric rise in the use of artificial intelligence in programming, it's all the more important to pay attention to this complexity, given that it's easier than ever to write complex, unoptimised code that sometimes isn't reread sufficiently, and can lead to unprecedented chaos.
A note about runtime validation
The types we have defined in this article are used to validate the chronology of two times in a day at compile time. However, in a real-world application, you will also need to validate the chronology of two times at runtime. Since TypeScript types are erased at runtime (even worse: they are not even emitted due to transpilation to JavaScript), you will need to write runtime validation code to ensure that the chronology of two times is correct. If you are using libraries such that io-ts, zod, or class-validator, you can use them and not worry about boilerplate code. If you are not using any of these libraries, you can write your own validation code. Here is an example of such code:
function createTimeInterval<Start extends Time, End extends Time>(
start: Start,
end: End,
): TimeInterval<Start, End> | null {
return start.hour < end.hour ||
(start.hour === end.hour && start.minute < end.minute)
? ({ start, end } as TimeInterval<Start, End>)
: null;
}
Further challenges
This article is just a starting point for type-level arithmetic in TypeScript with time intervals. Here are some challenges that could be interesting to tackle:
When the interval spans over two days, the
end
hour can be less than thestart
hour. We could write a type that validates the chronology of two times, taking into account the day.Since this article is focused on time intervals, it only involves natural numbers. However, the types for asserting inequalities between numbers can be generalized to integers. This is a completely different challenge, as it involves negative numbers and the arithmetic operations that go with them, implying complex type matching to infer the sign of the result and its digits. Two incredible articles on the topic by Mieszko Sabo can be found on the SoftwareMill blog: Implementing Advanced Type-Level Arithmetic in TypeScript: part 1 and part 2.
Usability: the
TimeInterval
type is great and works well when modelizing and instanciating standalone time intervals. However, imagine you have a typeEvent
that contains astart
and anend
time. We can write it like this, leveraging theTimeInterval
type:type Event<Start extends Time, End extends Time> = { name: string; interval: TimeInterval<Start, End>; };
This type looks great. However, imagine now contains multiple intervals and becomes:
type EventWithMultipleIntervals = { name: string; intervals: TimeIntervalAdvanced<Time, Time>[]; };
In this situation, the type of
intervals
isnever
, can you see why ? The same problem was actually already present with theEvent
type. This value is not instantiable:// compilation error { ... } is not assignable to type never const events: Event<Time, Time>[] = [ { name: "Event 1", interval: { start: { hour: 10, minute: 15 }, end: { hour: 11, minute: 15 }, }, }, { name: "Event 2", interval: { start: { hour: 11, minute: 20 }, end: { hour: 12, minute: 20 }, }, }, ];
Solving this issue is a great challenge and could be explored in a future article.
Finally, we could think about writing more types for manipulating time intervals, like a type that checks if a time is within a time interval, a type that checks if two time intervals overlap or are adjacent, a type that calculates the duration of a time interval and ensures it is within a specific range, a type that splits a time interval into smaller intervals of a given duration, a type that merges overlapping time intervals, some types for complex time manipulations such as shifting a time interval by a given duration, considering time zones, etc. The possibilities are endless!
Conclusion
As a convinced Scala developer until the end times, I have to admit that TypeScript is a powerful language that allows to perform a quite advanced form of type-level programming. In this article, we've somehow built the same kind of basic blocks that we can find in amazing type constraints libraries like Scala Refined or Iron. However, the TypeScript type system is not at the level of power and expressiveness of Scala's type system (which is able to compute derivatives of functions at compile-time, or even solve a Tic-Tac-Toe game or a Sudoku at compile-time). But TypeScript is a language that is gaining in popularity, and it is important to understand its type system in order to take full advantage of it.
I took a lot of pleasure writing this article. I use TypeScript in my daily work, and I am always amazed by the things you can do with it. I hope this article has given you a taste of the power of type-level arithmetic in TypeScript and that you will be inspired to use it in your own projects. If you liked this article, don't hesitate to share it with your friends and colleagues. You can also train your skills by trying to solve the challenges I mentioned in the previous section along with the amazing TypeScript type challenges that can be found on the internet.
I look forward to writing the next article in this series, in which we'll delve deeper into this fascinating topic.
If you have any questions or comments, please feel free to leave them below. Thank you for reading, and happy coding! And never forget: Let the compiler do the work for you! Life is too short to waste time on runtime errors.
Subscribe to my newsletter
Read articles from Brieuc Kaisin directly inside your inbox. Subscribe to the newsletter, and don't miss out.
Written by
