Skip to content

Instantly share code, notes, and snippets.

@blemoine

blemoine/blog.md Secret

Created March 31, 2018 20:36
Show Gist options
  • Save blemoine/f05595d7d7888b48cce02c5b7acfee11 to your computer and use it in GitHub Desktop.
Save blemoine/f05595d7d7888b48cce02c5b7acfee11 to your computer and use it in GitHub Desktop.

Refinement type in TypeScript - Or how to specify that number should be positive.

All the code of this article has been tested with typescript 2.7.2

Sometimes, the base types offered by typescript, like number or string, are not enough to express precisely what you want. For example, you may want to represent the age of a user with a type indicating that it must be a number greater than 0. Or maybe you'd want to represent an email, which is a string that should match a certain pattern. The objective of this article is to show how to create those kind of types with refinement types.

What are refinement types?

Refinement types are types defined by two things:

  • a base type
  • a predicate over this base type to indicate which values are valid For example, you could have number and (x:number) => x > 0) to represent positive numbers, or string and (s:string) => s.indexOf('_') === 0)) to represent strings starting with _.

This would be easy to model with a wrapper type:

https://gist.github.com/f022a10fb78a8faf93544442abadf335

But using a class like this would lead to a lot of wrapping and unwrapping of the value, and this would mean some runtime overhead.

By default, TypeScript doesn't support refinement types without a runtime wrapper. But there is way to simulate refinement types through type guards.

Reminder on type guards

Type guards are functions that, by doing a runtime checks, guarantee that something is of given type in some context:

https://gist.github.com/48390ff087d09f9d5a41bf4640154f45

It's also easy to create custom type guards function:

https://gist.github.com/ec2fc3c5584011d516c95b13f53a14e9

How to refine types?

The type checker trusts blindly the type guard function, even though they are only a runtime checks. That means that it's really easy to write a type guard that lie to the compiler:

https://gist.github.com/07c72a73e73149d7af16de5d35cd03d8

This is the property that we will use simulate refinement types.

Going back to our initial problem, we want to define a type that is "a number where all valid values are positive".

First we will define a type PositiveNumberTag representing a tag indicating that the number IS positive.

https://gist.github.com/5d2dd0b852a9ed6c2c5f75a707c9a3cc

We're using declare here because we don't want this class to exists at runtime. It also means that we will not be able to do new PositiveNumberTag().
We're using a private property named __kind because that way TypeScript will refuse to type checks things like: const a: PositiveNumberTag = {__kind:'positiveNumber'}. The only way to create a PositiveNumberTag will be through the new operator, and as we've seen previously, this will not be possible.

Then we'll define the type PositiveNumber simply as a number with the previously defined tag:

https://gist.github.com/699565b12baf58f164675fe52ed6f33b

Now, we'll need to create a type guard function that will say to the compiler "trust me, what you're using right now is really a PositiveNumber", even though this type cannot be build.

https://gist.github.com/99308ab02cc9433c3fd81efdb30baafb

How do we use that? Let's say you want to write a function that needs a timeout, which must be a positive number.

https://gist.github.com/099d2255fe861b98cbdc2674902ffff3

Other examples

RangeValue

This pattern is usable in a lot more contexts than positive numbers. We can, for example, extend the previous code to create a numeric type indicating that the number is in a specified range.

https://gist.github.com/46fe19b1e544d981a605a5b5fa5dedcb

Email string

Sometimes you'll want to validate that a string is an email. Refinement types can also be used in this case:

https://gist.github.com/41a0e4b6d76dabd3bffcb34a0d5072b8

Tagged types

A tagged type is a type composed by an existing type and a tag. Refinement types as defined above are in fact tagged type where the tag is a "proof" that the predicate holds. But we can also use the above pattern to create simple tagged type.

This is useful, for example, when manipulating physical quantities like distance or weight. We can model units with tagged types and be sure this way that we'll never be able to add feet and meters, a things known to have lead to []some infamous martian satellite crash](https://www.wired.com/2010/11/1110mars-climate-observer-report/)

https://gist.github.com/b1fb2f8aa6ad51d755c27bb446eb051a

Conclusion

The use cases of refinement types are numerous, and they are surprisingly easy to use in TypeScript, and this without any runtime costs. While Flow has opaque type to simulate an equivalent feature, this is something that will not land soon (if at all) in TypeScript, so feel free to use refinement types as they are right now!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment