Universal & Existential Types in ReasonML

You may have seen these terms thrown around in explanations, documentation, conversation, used in comments to describe types in your code base, or a library and been like:

WAT IS GOIN ON?!?!

Fear not, you probably know what these are or understand them conceptually but haven’t seen these names attached to them. Throughout this post we are going to explain what these terms are and how they are useful to you.

Setting the scene

To explain these, we are going to use the analogy of the User & Implementor. Where the User is the person utilizing a piece of code, and the Implementor is the person who authored the code. Universal and existential types, describe the information hiding war between the User and the Implementor.

Throughout this post constantly ask yourself, who has more flexibility, the User or the Implementor, in both existential and universal types?

Universal Types

In the information hiding war, Universal Types represent the following relationship between the User and Implementor:

Implementor doesn’t have information about the types, User has the information about the types

Take a look at the following signatures and think about how you can implement them from the perspective of the Implementor:

let f: (int, int) => int;
let g: int => int;

There are potentially infinite implementations of these signatures–add, increment, decrement, identity, first, second, etc. The party that gains the most information and by extension flexibility/freedom from this signature is the Implementor, and the User loses freedom/flexibility because they must satisfy the function with greater precision when they use it.

Now go ahead and think about how you can implement the following signature just like you did previously:

let f: 'a => 'a;

The function above by definition must work for all ‘a, no matter what the User in the future decides ‘a will be. So you can’t assume that ‘a is an int, string, or any other data type for that matter. In fact, there is only one way to implement the signature above to make it work for all types, and that is identity! This is because f has to produce a value of type ‘a, that is completely unknown to f.

Who has the control in the power struggle for flexibility above, the Implementor or the User? It’s the User in this case, because the function above must work with any value that the Implementor has no clue about.

How could you as the Implementor potentially implement the following signatures to work for all types?

let f: ('a, 'b) => 'a;
let g: ('a, 'b) => 'b;

As the Implementor you are constrained by not having enough information to implement these signatures in a “specialized” way, so you must come up with a generalized solution. As the User you have all the information because you are in control of what is passed as arguments to these functions. So as you come up with an implementation for these, you will come to the conclusion that f will return the first argument passed to it, and g will return the second argument passed to it. Both of these functions as it happens are in the ocaml standard library.

Getting deeper in the universal types pudding

Lets look at a signature of a function familiar to most folks:

// List.map
let map: ('a => 'b, list('a)) => list('b);

List.map will return a list of ‘b elements, it has to produce a list, according to the signature. It could always produce the empty list. If it ever produces a non-empty list, the only manner in which values of ‘b could be obtained is by applying the ‘a => ‘b function. In other words, you can only produce a non empty list if the input list is also non-empty, otherwise there are no elements to apply the ‘a => ‘b function on.

You can reason from the types only, that empty lists get mapped to empty lists. Non-empty lists can still get mapped to empty lists, or it might always produce a list of thousands of copies of the first element mapped by ‘a => ‘b.

The types in the List.map signature are “less polymorphic”, their shape is better known than ‘a => ‘a, and we now have constraints like lists and callbacks. As a result of this:

1. The function got more “interesting”
2. We also know less about what the function actually does

Lets look at a specialization of List.map for int to both for ‘a and ‘b:

// Int_list.map
let map: (int => int, list(int)) => list(int);

This map potentially doesn’t even have to map the empty list to the empty list, and it doesn’t ever have to call int => int, if it wants to produce a non-empty output list.

You might think we have more information, because we know that no matter what when the function is applied, assuming there are arguments, we will get back elements that are ints in our list. We actually have less information here, because the ‘a => ‘a also works with ints. The difference is that the Implementor knows it’s ints, this means Implementor has more freedom to implement the function, and that User has less information about what the Implementor actually did.

This was me when my brooski Anton explained this to me

Sometimes the generalization can specify more concretely what is going on, vs the specificity that may have you wondering what is going on in the function under the hood. It makes the function more useful in different situations that the implementor didn’t predict because the user can use it with different types, and this is known as polymorphism. In fact polymorphism is directly dependent on hiding information from someone.

In ReasonML/OCaml there exists parametric polymorphism that occurs automatically when the type inference determines that an expression is valid for any type. This usually becomes apparent when type variables are present in an expressions type, ie. let fst: (‘a, ‘b) => ‘a;

To boil this down, we have a world with a function xyz, xyz splits the world into two pieces:

1. The implementation of xyz
2. The rest of the world, that might call xyz

The universal quantifiers hide information from (1), and thus make it more polymorphic (flexible) for users in (2).

Existential Types

Conversely Existential Types In the information hiding war, represent the opposite:

Implementor has information about the types, User doesn’t have the information about the types

Heres a simple example of existential types in modules:

In the sample above we made the t type abstract in the module type Animal. In doing so we create a relationship where:

1. The Implementor can implement the abstract type pretty much however YOU, the Implementor want, in any specific way
2. The User, has to write code in a polymorphic manner when using the module.

Because the module type is abstract, only the Implementor knows exactly what t is, and the outside world does not know what it is. No one can just walk up to it and start calling sprint with a string. The module constrains the User to use the Animal.make function to create a type t.

To show the contrast, lets see what happens when we fail to make t abstract in our module type:

If we fail to make t abstract anyone can run up on Animal and call sprint as long as they happen to have a string. They don’t event have to call make to create our module type t.

What does this mean? When the Implementor creates an existential type the User is constrained by not knowing what that type is, and they can no longer assume what value is being passed around in their program. User has to write their code in a polymorphic manner, because it has to work no matter how t was implemented by the Implementor. The implementation could be provided or changed later, but as the User you must take that into account and code “defensively”.

As the User of module Animal, I am writing code against its signature. The implementation of that signature might not even exist yet or there might be lots of different implementations that my code would work with all of them. It is polymorphic. This is because because we don’t know what t actually is.

Summary

To wrap it all up, Existential and Universal types are about imposing polymorphism (aka information hiding) on different parts of the programming world. This promotes reusable and composable code that helps everyone understand relationships within your codebase.

Until Next time!

If you want to receive updates about when ReasonTraining is going to be fully launched and notifications when we release new blog posts, please go ahead and drop your email here and follow us on twitter.

👋