Making the ReScript type system work for you (Part II)

In the last part of this series we learned how the compiler finds the types of variables. If you didn't read it, go do it now! This part builds directly on that.

If you did read it, here's a reminder of the 2 rules we learned so far:

📏Rule of Principality — In ReScript, every expression has a single type. We call it the Principal Type. This is always the most generic type for the expression, but it can be made more specific using type signatures.

📏Rule of Environment Order — Every time something is typed correctly it will be added to the environment. The Environment is built from the top of the module, so that things defined below have access to things defined above.

Typing Functions

Today we're going to try to find the type of a function that returns a constant.

let current_year = () => 2022

To do this, we need to introduce one new thing: the function type. Function types look like two types with an arrow stuck in the middle: 'a => 'b. Ok, back on the example now.

First, we'll annotate the code with new type variables, just like we did before. This looks like a lot at first sight but we can break it down:

let current_year: 'a = ( ( (): 'b ) => (2022: 'c) : 'd)

The type of the full variable is 'a,  the type of the function argument is 'b, the type of the function body is 'c, and the type of the whole function is 'd.  Okay, let's now put this all together into a our set of constraints:

'c = 2022
'b = ()
'd = 'b => 'c
'a = 'd

Now let's simplify a little. We know 2022 is an int, so we know that 'c = int; and we know that when creating a variable, the type of the binding will be equal to the type of the expression being bound, so if 'a = 'd, we can get rid of 'd and just use 'a instead.

'c = int
'b = ()
'a = 'b => 'c

The last type variable that needs replacement is 'b, so now we need to find out what is the type of the value ().

The compiler then checks if the value () corresponds to any known types that are currently in the environment.

The environment by default has all the types that are part of ReScript. It also includes all the types that have been defined before the value that we are type checking now, and any other types defined in modules that we have open-ed before the value we are type checking now. If at any point we try to look something up and it is not there, this will be considered a Type Error.

In this case, our environment would look something like this:

So when we look () up, we find that the type is unit, and we can move on to replacing this in our system of constraints:

'c = int
'b = unit
'a = 'b => 'c'

Excellent! We can finally solve this by replacing 'b and 'c:

'a = unit => int

With this type, we can go back to our original code, and add the inferred type:

let current_year: unit => int = () => 2022

After the compiler type checks this function, it adds it to the current environment.

Now that we've learned more about the environment, and typed a function, we are ready to tackle our next example.

Typing Compound Expressions

Let's type now a variable that uses other variables in its definition.

let year = 2022
let next_year = year + 1

Our intuition here tells us that both year and next_year should be of type int. Now we will try to follow the same steps the compiler would take to try and arrive at the same conclusion.

But before we continue, here we have another value that comes predefined in ReScript: the function +, with type: (int, int) => int. This will be available in our environment:

This time around we will use the results of type-checking year, and we will only annotate with fresh type variables the new variable:

let year : int = 2022
let next_year: 'a = ((year : 'b) (+ : 'c) (1 : 'd) : 'e)

We know that + is a function that is applied to year and one, so we know that 'c must be a function type, like: ('b, 'd) => 'something. We also know that this return value will be the final value of next_year, so we know that whatever it is, it must be the same as 'a.

Finally, we know that year : int, so our environment is now complete.

And our constraints are almost ready. Since we are applying a function (+), we will need to introduce a similar idea for our constraints.

We will call this apply, and it will look like this: apply 'a 'b. The intuition we are trying to build is the following:

• when'a is a function that takes one or more types as inputs
• and when 'b is exactly the same types that 'a expects
• then apply 'a 'b is the same as return types of 'a

For example:

'a = int => bool
'b = int
apply 'a 'b = bool

This is useful because we know we need to apply a function, and we know we need the return type, but we don't yet know the exact type this function has!

Our constraints then will look like this.

'b = year
'd = 1
'c = ('b, 'd) => 'e
'a = apply 'c ('b, 'd)

We know that 1 is an int, because it is constructed as a valid integer in the syntax, so we can work out that 'd = int. After we look up year in the environment we know that 'b = int. In the same way, after we look up + in our environment, we know that 'c = (int, int) => int.

Our constraints now look like this.

'b = int
'd = int
'c = (int, int) => int
'a = apply 'c ('b, 'd)

Because we were applying the function +, and both arguments have the right type (both are int), we know that the resulting type of the evalution, 'e will be int too. Replacing these all around we get that:

'a = int

Which means our variable next_year can be annotated now:

let year : int = 2022
let next_year : int = year + 1

And our environment is updated.

Success! We have arrived at the same conclusion as our intuition did, following the steps the compiler would take.

Next Steps

You've made it this far! Now it'd be a great moment to have some water and stretch your legs before trying some of these out on your own.

In the next part of this series we'll continue to explore by example how the type system works, building up on what we did today to learn how to type:

• Complex Expressions
• Complex Data (like records and variants)
• Generics!
• and what are the limits of Type Inference in ReScript!

By the end, you will have a correct and intuitive understanding of how the entire ReScript type system can work for you, so you can focus on shipping faster, better products!

If you liked this and would like to get notified as soon as the next piece is out, don't forget to subscribe below :)