The Math of TypeScript's Types

I've been studying functional programming for a few years and in doing so I've learned a lot about types that I would not have otherwise. In particular, studying Haskell and related technology begets some interesting concepts. The one I want to talk about this time is "algebraic types".

From wikipedia:

In computer programming, especially functional programming and type theory, an algebraic data type is a kind of composite type, i.e., a type formed by combining other types.

If you've used TypeScript for a bit you've probably been exposed to some of these already.

Sum Types

Let's say we have a short list of commands that an API will support, "list" and "pop". We can use string literal types to represent the valid values:

type ListCommand = 'list'
type PopCommand = 'pop'

Each of these types only have one value--the specific string that is valid. If we want a function that can take either command we can compose these types together using the | operator.

type ValidCommand = ListCommand | PopCommand

const performCommand = (command: ValidCommand) => 

The | type operator creates a sum type of the types to the left and right of it. What you should notice is that the sum adds the potential values together, i.e. ValidCommand accepts ListCommand plus PopCommand. This may be more apparent with bigger types:

type CommandOrFlags = ValidCommand | Flags

You'll remember that Flags had four valid values and ValidCommand has two. Thus CommandOrFlags has six (4 + 2).

So we can add types, can we multiply them too? Yes, indeed!

Product Types

As you may have noticed, you can think of | operator for sum types as "or". Product types are the other half of that, the "and". So then we have to find data structures that represent a type having multiple values simultaneously. Tuple is a great candidate for that since it allows us to have different types at its indices.

type Flags = [boolean, boolean]
const flags: Flags = ?

How many potential values can be assigned to flags?

With this small set we could list them out but we can use what we know about the individual types to figure it out with math.

The type [boolean, boolean] must have exactly two values and those values must be booleans. Booleans themselves have two potential values. If you know that tuples form a product type with the types they contain you just have to multiply 2 x 2 to know that the total inhabitants of the composed type is four.

Another way of encoding product types is to use an object:

type Point = {x: number; y: number}

So in a way you're already using them!

Sum types are a monoid

Monoid is an interesting mathematical structure that is pretty simple.

• Composition: Monoid is type with a combine operation that can join to values of the same monoid. a o b = c where a b and c are same type, and o is the operation.
• Associativity: The operation must be associative (a o b) o c = a o (b o c)
• Unit: operation must have a "unit" value that doesn't change the value it's composed with. a o unit = unit o a = a

As an example Arrays form a monoid where concat is the operation and [] is the unit:

// Composition
[1,2].concat([3,4])
// is same as
[1,2,3,4]

// Associativity
[1,2].concat([3,4]).concat([5,6)
// is the same as
[1,2].concat([3,4].concat([5,6]))

// Unit
[1,2].concat([])
// same as 
[].concat([1, 2])
// same as
[1, 2]

The thing I actually wanted to share is that types themselves form a monoid with | as the operation and never as the unit!

// Composition
type Foo = 1 | 2

// Associativity
type Bar = 1 | (2 | 3)
type Bar = (1 | 2) | 3

// Unit
type Baz = 1 | never
type Baz = never | 1
type Baz = 1

Mathematically there is also a monoid for product types but I haven't found a way to make it work in TypeScript.

Getting more mileage out of sum types in TypeScript

In exploring usage of sum types you may run into some challenge in writing functions that use them:

type Error = string
type Message = string

type Response = Error | Message

const handleResponse = (resp: Response) => {
  // wait. How do I actually have different behavior
  // since both cases are strings at run-time???
}

A trick to make this work is to provide some extra data at runtime so that your code can discriminate between the members of the sum. This is called a discriminated union.

type Error = {kind: 'Error'; message: string}
type Message = {kind: 'Message'; message: string}

type Response = Error | Message

const handleResponse = (resp: Response): string => {
  switch(resp.kind){
    case 'Error': {
      console.error(resp.message)
      return 'Fail'
    }
    case 'Message':
      return resp.message
  }
}

Switch is used here as poor man's pattern matching. TypeScript has good support for this technique and will make sure you have your cases covered if you leave off the default case.

You can even have empty types to union with states that have no other data:

type Error = {kind: 'Error'; message: string}
type Message = {kind: 'Message'; message: string}
type Pending = {kind: 'Pending'}

type Response = Error | Message | Pending

const handleResponse = (resp: Response): string => {
  switch (resp.kind) {
    case 'Error': {
      console.error(resp.message)
      return 'Fail'
    }
    case 'Message':
      return resp.message
  }
  // TS ERROR: Function lacks ending return statement and return type does not include 'undefined'.ts(2366)
}

Then to fix it you can just handle the case:

const handleResponse = (resp: Response): string => {
  switch (resp.kind) {
    case 'Error': {
      console.error(resp.message)
      return 'Fail'
    }
    case 'Message':
      return resp.message
    case 'Pending':
      return 'Pending'
  }
}

That's all for now. I hope this gives you new things to think about and you get a chance to use Sum types to better model your applications.

Edit note: I'd like to give a special thanks to @Phantz for the extra knowledge they dropped in the comments!

Comments

[Phantz]

Nice interesting article! Something unique around here is very refreshing. But I had a few friendly nitpicks :P

Arrays are not product types

Ok so, let's talk about arrays. An array is not a product type. Is it a sum type? Well, it's complicated. The truth is that traditional arrays (C arrays - pointers to contiguous memory - same as JS) don't encode well in type algebra. In haskell, the traditional array is a GHC primitive. It's really neither a sum type nor a product type. It's a primitive that you build algebraic data types with. Similar to Int (except there is a way to represent numbers in type algebra, using a union type of literally all numbers in the set, but it is completely impractical and only conceptual)

Now, let's stretch the definition a bit. An array, at the high level, is a "variable length collection of homogenous elements". The type that pertains to this definition and encodes in type algebra very nicely is, of course, the cons list-

data List a = Nil | Cons a (List a)

I'm not going to even try to encode that in typescript since the bread and butter of algebraic data types is missing - pattern matching (you need this to make a sensible cons list implementations without relying on arrays).

I think you did a fine job on explaining why they are called "sum types" and "product types". But I'd suggest also emphasizing that the notion of the algebra pertains to the domain the types represent. Specifically, how many elements the domain has.

The answer to the question "How many values can this sum type represent?" is "Just add the individuals up!", and similarly for product types. Someone may be confused as to what this phrase means-

So we can multiply types, can we add them too? Yes, indeed!

We're not multiplying/summing types, we're multiplying/summing their domain sizes.

Is it correct to say type constructors convey composition?

I think this is a bit misleading-

In the above case the Array type is being composed with the string type to produce Array

I think it'd be better to say-

The Array type constructor is being instantiated/constructed with the type parameter string

I wouldn't use the word composition here since that seems a bit uncommon. I've never quite seen that used in the context of type constructors (or data constructors, in the case of Haskell)

Promise is not a product type

Similar to the other nitpick. It's difficult to encode javascript promises in type algebra. You could stretch the actual definition of the Promise class to make it a sum type......sort of? At a very, very basic level, it'd be the most typical sum type of all - the Either type.

data Promise e a = Failure e | Success a

The Promise type itself does not encode async behavior, that's a runtime thing - abstracted over callbacks. A Promise type simply wraps either failure or success. The catamorphism (haha fancy names) on this would be either. It is equivalent to a .then that handles both failure and success. Left and Right would be reject and resolve respectively.

At a higher, more useful level that truly models async behavior - we probably wouldn't use promises at all.

Records are not necessarily product types

Ok so records are more or less just maps. An idiomatic Map in Haskell looks like this-

type Map k v = [(k, v)]

Isn't it funny how that isn't even a map, just an association list.

That was a half joke, half not. This is the thing about type algebra that bothers me. Encoding actually practical stuff is not idiomatic. Ok, so the Data.Map generally used by Haskell (from containers) is implemented a size balanced tree. This is a low level detail and doesn't actually say much about type algebra. When we're concerned about type algebra - we just pretend that a map is an association list.

Anyway, an assoc list is a sum type of product types. Since list is a sum type and its elements are pairs, a classic product type. This gives a much, much clearer notion on how to calculate the domain size of a record/map. Except you know, a list is a recursive sum type with one branch as a product type anyway, so good luck with that.

By the way I totally see the rationale behind calling records product types. But the key detail we're missing here is that records don't look like this (singleton)-

{ k: t }

(where k is a value of type K and t is a value of type T.)

Instead, it looks something like this-

{ k0: t0, ..., kn: tn }

that is, it may not hold a singular value - but many, in completely variable length.

Notice how the domain size intuition of K x T only makes sense in the first case. Where one of the Record<K, T> is exactly { k: t }, another value of that type could be { k1: t1 } and so on for all combinations of K and T.

But in the actual case, the Record<K, T> is not like that. Product types must give a notion about the domain size. That's all broken when variable length types are involved. In reality, the domain Record<K, T> has infinitely more values than K x T.

Monoids are really cool, thanks for including them!

Great observation on monoids. Requoting something I've heard many others say- "Monoids are gentle sea creatures that appear everywhere in programming, you just have to notice them!". You could expand the definition by introducing semigroups first too! It's even more common to stumble upon semigroups in one's daily venture into coding, monoids are just semigroups with an identity element.

[Jethro Larson]

We're not multiplying/summing types, we're multiplying/summing their domain sizes.

A good point!

You're probably right about these generic types not being product types, there does seem to be an essence of domain multiplication for certain things which is why I was led astray. I might have just gotten confused after falling asleep listening to Bartoz's category theory lecture series

I'll try to incorporate your suggestions when I can find time. Thanks!

[Phantz]

Speaking of category theory, check out Philip Wadler's Category theory for the working hacker if you haven't already!

[Phantz]

By the way, are you interested in the monoidal properties of type algebra? You made a spot on observation on sum types. It's such an elegant detail and I love it.

It makes perfect sense that sum types form a monoid. Because sum/addition forms a monoid. And it's exactly the same too. In basic arithmetic, the identity element of addition is 0. Notice the similarity? Void is our zeroth type. The type with no inhabitants. Precisely equivalent to never. A type that represents some value that doesn't even exist.

Let's extend the intuition a bit. You asked the equivalent for product types. What arithmetic operation do product types represent? Multiplication. What's the identity element of multiplication? 1. In the category of types, what would be the equivalent to 1? (By the way, Haskell programmers lovingly call the category of types "Hask", so I will too :))

Well, let's see here. The equivalent to 0, in Hask, is Void. The equivalent to 1 is, of course, Unit aka (). The type that represents a singular value - (). In all programming languages, this is generally void. Same in typescript. Yeah I know, confusing. Void is never, Unit is void....? Ok, well it's not the type theorists' fault this time :P

So that gives you, product types as monoids- x is the associative binary operation and Unit is the identity element.

Good luck actually using this in programming languages though. In languages like typescript, union types collapse (as you have noticed) - so the intuition about monoids seems somewhat practical. But typescript doesn't really have an explicit product type concept. And I refuse to call intersection types the equivalent to product types. This is probably as close as it gets.

Meanwhile, in Haskell - neither union types nor product types collapse, so neither intuition is practical.

But who cares about practical when you can learn fun things about notions of type theory!

[Jethro Larson]

Thanks for the insight and additional explanation!

Yeah, tuple seems to be a close as it gets to a raw product type in TS but I didn't figure out a way to make monoid make sense to me for it. void is a great candidate for unit but what's the operation and how would that operation be commutative on the unit? [void, 1] seems a lot different than [1, void]

I'm with you on intersection types, they don't apply to enough cases to feel right to me either. I think there's some interesting mathematical structure to learn about with them but it hasn't bubbled to the front of my brain yet.

I considered trying to make this post talk about practical application but like you say, the fun insights are reward enough.

[Phantz]

Yes, the monoidal operations for ADTs are usually not implemented in the type system. Typescript is, surprisingly, an exception here. The monoidal operation for sum types is perceivable here. But not for product types. In haskell, neither can be perceived.

I think the best abstract intuition that can be made is that the type T x Unit (or Unit x T) only really needs a value of type T to be constructed. And in all its usages, that's the value that matters. The Unit can be filled in and out implicitly. Ultimately, it will only make full sense in pure type algebra, where they're concerned about just the domain size, not representation (that'd be abstract data type).