Generalized algebraic data types (or GADTs) are a powerful tool that can augment algebraic type systems enabling them to be far more expressive. In addition to enabling polymorphic recursion, they also serve as a fundamental unit for existential types. In this post we will look at what all of those phrases mean, and how GADTs can be used in practice.

Background

While it’s easy to think there is only one correct way to write code, in the practice the conflict between typed and untyped languages is yet undecided.

Typed languages provide a number of guarantees about the program that can be checked during compilation whereas untyped languages offer a flexibility and convenience disallowed by strict type systems. One way to mediate this divide is to make use of a more expressive type system. This means that the programmer can define more complex structures because the type system has a way of expressing them. However, in order to make use of this expressiveness, one must understand the type system in which they are working and the techniques that it employs. For the purposes of this article, we will be looking at OCaml’s type system, and how it exposes a powerful typing tool called GADTs

Algebraic Data Types

It would be rather difficult to discuss generalized algebraic data types without first explaining what an algebraic data type is in the first place. Regardless of what languages you are most familiar with, you have likely seen many of these concepts before; polymorphism, abstraction, and structure all emerge out of ADTs.

Before we begin, let us consider a rather basic language. Right now, we have only two types

type t = int;;
type u = unit;;

Primitives

The first type is an integer. Since we are focusing on theoretical concepts and not concrete implementations, we may assume that there are infinitely many such integers that inhabit type t. The second type is one that people may not recognize but are probably familiar with. Often called void in C-like languages, the unit type is a type which has only a single value. We will often denote this as () which may be thought of as an empty tuple. These two types are clearly not the only primitives one might expect in a language — char, boolean and float all come to mind — however they should be sufficient for our discussions.

Tuples

The first algebraic extension to our type system we will consider is a tuple. Also known as product types, a tuple represents a pair of two items.

Let’s consider why this would be helpful. Say for instance that we want to represent a rational number in our language. We could, anywhere we wanted to use it, pass around two variables — the numerator and the denominator. But then we don’t have a rational type, instead we emulate the functionality of a rational by using two types. If, however, we desire to have a rational type, we make make it a tuple of two integers, one for the numerator and one for the denominator. It would look as follows

type rat = int * int;;

Then an example of a rational would be

let (inf : rat) = (1, 0);;

This might seem straightforward, but there is an interesting subtlety related to the notion of products. Consider the type given as unit * unit. While this is technically a tuple, there is still only one value that inhabits this type, namely the tuple ((), ()). Let us for a moment count the number of possible values of a tuple type. To this end, consider the number of valid integers to be Z.

Then we see that the total number of values that can inhabit a rational is Z*Z (there are Z options for the first element, and for each of those Z options for the second element. Hence Z2 total values). Likewise a tuple of int * unit only has Z total options since unit has exactly one inhabitant. The result is that we have Z options for the first element and 1 for the second. As such we see a close relationship between a tuple of types and the product of their inhabitants. This relationship in fact goes much deeper, but we will not cover that much here.

Variants

Now that we have introduced product types, it may seem reasonable that we would wish to introduce sum types. This becomes a little bit more difficult as many people are not used to proper sum types. However, their significance should already be clear. If the purpose of products is to have type a and type b, then preferentially we would like to express that a sum can have type a or type b. We solve this using variants or labeled sums.

Consider again our rational type. In many languages, a decimal type will be able to have an additional value to handle cases where arithmetic does not make sense. This value is often called “Not a Number” which is then abbreviated to NaN. Let us add a new variant type that expresses this rational.

type nanable_rat =
  | Value of rat
  | NaN of unit
;;

Hopefully the syntax of this is relatively straightforward, but if it’s not immediately clear, this declaration says that a nanable_rat can either be a rational tagged with Value or it can be a unit tagged with NaN. Consider again the number of inhabitants of this type. There are Z many inhabitants of the Value case, and 1 inhabitant of the NaN case. Furthermore, since we may only have one or the other, basic counting reveals that we have Z²+1 inhabitants of this type. Thus, we have introduced a type that is the sum of a rational and a unit. Once again we see a relationship between the semantic meaning of the type and the number of inhabitants of it.

Before we go any further, let’s look at some interesting properties of these sum and products. If you remember back to basic algebra, then you will recall that in all rings the relationship between multiplication and addition is given by the distributive property (a+b)*c=a*c+b*c. Knowing this, we would expect that to hold for our types, but it seems odd that it should. Yet, consider the two type ts below

type i =
  | First of int
  | Second of unit
;;

type t = i * int;;

and

type i' = int * int;;
type j' = unit * int;;

type t' =
  | First of i'
  | Second of j'
;;

Distributivity tells us that these should be the same type, yet they do not look it. And yet, take for example (Second (), 5) which has type t. Trivially, we can rewrite this as Second ((), 5) with type t'. Likewise, we can say that First (7,8) as t' is semantically equivalent to (First 7, 8) as type t. Before continuing, you should convince yourself that distributivity does in fact hold.

Universals

I promised earlier that ADTs were the foundation for polymorphism, but have not mentioned it yet. This is because polymorphism is explicitly declared in the type of an OCaml value. This can be rather confusing so let me put it like this. If we want to implement a list, we would like that to be a list of anything. It can be a list of integers, characters, or even units. If we have a list of items then this is evident, a list of integers is simply an int list. However, consider the empty list. It could, for instance, be a list of integers or even perhaps a list of integer lists. Since there can be an infinite number of types, we cannot reasonably have a different list type for each of its elements. Instead we say that it is parameterized by a universal type. We often denote this universal type 'a (pronounced alpha). Thus, we say that the type of the empty list is 'a list because it is a list of anything. This is akin to saying ∀’a: ([] : 'a list). Hence alpha is universal.

As one might expect, we can then use this alpha term in order to create new types. In fact, we can create a proper list type using only sums and universals now.

type 'a list =
  | Nil of unit
  | Cons of 'a * 'a list
;;

What this expression says is that an 'a list is either a Nil () or a Cons(a, b) where a has type 'a and b has type 'a list. Now, here is a crucial piece to understanding this. Nil can have type 'a list because it does not require an alpha to create. If I say (Nil ()) : impossible list (where impossible is the type with no inhabitants defined as type impossible;;), this is completely valid because we do not need something of type impossible in order to create Nil. However, we cannot say that Cons (a,b) has type 'a list because we have already stipulated that the type of this expression is dependent on the type of a, and an instantiated variable cannot have type 'a.

In this way, we add to our basic algebraic structure a ∀ statement that can be used to quantify over every type.

Existentials

Almost there. Before we begin the last section of background, use this moment to stretch out and grab a cup of water. We’re almost there.

In order to have a basic understanding of what algebraic type systems do, we need the counterpart to the universal, the existential. This is a little bit harder to explain, in part because the syntax for it is verbose and unintuitive at first. As such I’ll begin with an English description.

Sometimes when writing programs we don’t care about the actual types, but rather what they can do. This allows us to abstract away how code is actually written and instead make use of an API to perform operations. A good example of this might be a stringable. We want some type, we don’t know what it is, but we can create it from a string, and we can create a string out of it. Internally it could be an integer, a byte array, or even a string! From our perspective we do not know, nor do we wish to know. This forms the foundations of the existential type, more commonly known as a module signature.

Module signatures serve as a way to describe the operations that a module can do, while optionally ignoring the implementation of how they do that. Consider again stringable, but now as a signature.

module type Stringable = sig
	type t
	val of_string : string -> t
	val to_string : t -> string
end

The signature tells us that there exists some t, but not what it is. One possible example of a stringable module might be

module Stringable_int : Stringable = struct
	type t = int
	
	let of_string x = Int.of_string_exn x
	let to_string x = Int.to_string x
end

From an application writing perspective, it’s clear why we would want this functionality, and this syntax for doing it. However, from a type theory perspective this poses an issue. Seeing the examples as given does not tell us whether we have a true existential type. If the modules are all defined at compile time, then we can always statically determine the type of t, and so this is no longer a true existential type. Yet, in the case of OCaml at least, this is not the case because modules are first-class, meaning they can be created on the fly and passed around like normal variables. Thus this is in fact a viable (if cumbersome) existential type.

GADTs (Finally)

Motivation

With all of that background out of the way, it’s time to see what GADTs are and how we can make use of them in OCaml. In order to show where GADTs shine, lets first consider a few cases where normal ADTs fail.

type 'a t = 'a * 'b;;

Looking at this type, we would not expect it to be valid. In it we’ve specified that you need a 'b in order to create a t, yet we do not encode 'b into the type of the expression in any way. Thus, we have no way of knowing once we’ve extracted it, what the type of that value is. As such, OCaml does not allow you to create this type.

let to_list ...args =
  args
;;

let (_ : int list) = to_list 1 2 3 4 5;;

I confess to making up syntax here, but the point stands that there is no way of using ADTs to define a function that takes an arbitrary number of arguments. Instead, you must explicitly identify the number of arguments in the type of the function.

type ('a, 'b) t =
  | Value of 'a
  | Sub_exp of ('b, 'a) t

let rec get_val = function
  | Value _ -> ()
  | Sub_exp x -> get_val x

This is an interesting case because unlike the other two examples, this one typechecks and compiles without issue. However, we would expect the type of get_val to be ('a, 'b) t -> unit, but instead it ends up being ('a, 'a) t -> unit because OCaml does not allow by default polymorphic recursion (recursion where the input type changes). Thus, it constrains 'b to 'a.

What is a GADT

Informally, a GADT is a normal variant where we choose the return type (within reason). Consider a standard variant example

type 'a t =
  | Foo of 'a

In this example if x has type int, then Foo x will have type int t. This is straightforward and works the way most people intuit it to. However, with GADTs we can get more creative, consider the new version of t.

type _ t' =
  | Foo : 'a -> 'a t

This type is exactly identical, but it uses a new syntax that we have not seen before. Namely, we define the constructor Foo as a function that takes an 'a and returns an 'a t. While this is not particularly exciting on its own, it becomes more so when we realize that we can freely change that return type, as long as it is a _ t.

Existential GADTs

For our first trick, we can use this power to make an inline existential type without needing to use module signatures. Using the stringable interface from before, we simply do

type stringable =
  | Str : ('a -> string * string -> 'a) -> stringable

This might look a bit complicated, but we can unpack it a bit. All this is saying is that Str is a constructor which takes two things. For some specific type 'a it needs a way to turn that type into a string, and a way to create a new element of that type from a string. Once it has both of these, the constructor returns a stringable which knows nothing about 'a and only knows that there exists some alpha such that these statements hold. For readability, we can add an extra type

type 'a v =
  { to_string : 'a -> string
  ; of_string : string -> 'a
  }

type stringable' =
  | Str : 'a v -> stringable'

What we have done is create a type closure. These can be handy for a number of things, but one can easily run into difficulties when you try to unpack them. Consider a stringable generated for an integer.

let int_stringable =
  { to_string : Int.to_string
  ; of_string : Int.of_string_exn
  }
;;

let stringable = Str int_stringable;;

We can now use it, but we have no concept of what 'a is, so the only way we can create an 'a is from of_string, and the only thing we can do with it is turn it into a string with to_string. All of the following are invalid operations on this structure.

let Str { to_string; of_string } = stringable;; (* Unexpected existential *)

let _ = 
  match stringable with
  | Str { to_string; of_string } -> 
    to_string 3                                 (* type int is not equal to type $_'a *)
;;

let int_identity =
  match stringable with
  | Str { to_string; of_string } ->
    Fn.compose of_string to_string              (* type constructor $_'a would escape its scope *)
;;

If this seems limiting, that is largely because it is. The idea behind existential types in the first place is to hide the actual type while only exposing a way to use it. It also allows us to generate a single type that can hold values from arbitrary many types. We will see this in use a bit later, but for now let us consider a different usage for GADTs.

Tagged GADTs

If the previous example used GADTs to hide component types, then the counterpart of that is using GADTs to create types out of thin air. Let’s say that we want to write an interpreter for a simple language, we can create OCaml types using GADTs that represent the interpreted language’s types. Yet, at the same time the underlying structure will be the same. If this sounds confusing consider this example.

type number_v;;
type boolean_v;;
type string_v;;

type interpreted_value = bytes

type _ typed_value =
  | Number  : interpreted_value -> number_v  typed_value
  | Boolean : interpreted_value -> boolean_v typed_value
  | String  : interpreted_value -> string_v  typed_value

The types number_v, boolean_v, and string_v are all void — they have no corresponding values.

However, we can label an interpreted_value (which is just binary data) as a string by using the String constructor. Then, the resulting value has type string_v typed_value. This might seem trivial and not worth the hassle, but it allows us to get stronger guarantees on the correctness of our interpreter by making use of OCaml’s type checker. Consider the following function signatures

let add
  :  number_v typed_value
  -> number_v typed_value
  -> number_v typed_value
  
let string_mult
  :  string_v typed_value
  -> number_v typed_value
  -> string_v typed_value
  
let parse_int
  :  string_v typed_value
  -> number_v typed_value

Assuming that we have correctly constructed our typed_values, then we know our interpreted language cannot itself have type errors, as the OCaml typechecker will prohibit us from, say, multiplying a number with a boolean. These additional static guarantees are one of the primary benefits of GADTs.

Polymorphic Recursion

One of the oft-cited benefits of using Generalized ADTs is that they provide a means for implementing polymorphic recursion. At first blush, this sounds unimpressive — afterall, we’ve already demonstrated some polymorphic recursive functions. However, polymorphic recursion is a special category of recursion in which the recursive function calls itself with a different type parameter. Normally, the OCaml type checker prevents this. This is largely for efficiency; in order to typecheck quickly the OCaml typechecker will constrain the free type variables for the function at the callsite. We will avoid going much deeper into why this is required, but rather look at what it allows us. For instance, say we want to write a function that can take an arbitrary number of arguments. This is impossible to do without using GADTs. However, by being clever about our types we can write a function that creates a list out of all its arguments. Consider its signature here.

type (_,_) list_param =
  | E : 'a -> ('a, ('a, 'b) list_param -> 'b) list_param
  | X : ('a, 'a list) list_param
;;

val create : ('a, 'b) list_param -> 'b

This is pretty confusing, so before we try to write the code, it is imperative

that we understand what it represents. We understand list_param to be a GADT that encodes the arguments to our function. Specifically, we’ve defined our type such that an elt : ('a, 'b) list_param contains data of type 'a and create elt returns a 'b. This makes the constructor X easy to understand; create X should return an 'a list, which as we mentioned earlier requires that create X = []. The E constructor is a bit more complicated however. Specifically, E encodes the recursive condition for create. When create consumes a list parameter created by E, it is required to return something of type ('a, 'b) list_param -> 'b, the type of create itself! This is certainly confusing, and if you don’t understand it yet, its worth looking over again until the general structure makes sense. Once we have that down, we can try writing the code.

A straightforward translation of the above structure would look something like this

let create =
  let rec create' acc elt =
    match elt with
    | E d -> create' (d::acc)
    | X   -> List.rev acc
  in
  create' []

However this doesn’t typecheck! Specifically, because the type checker does not understand how to perform polymorphic recursion, it thinks that create' has type 'a, and so the recursive call fails to return a list (as required by the base case). In order to instruct the type checker that this is valid, we need to introduce new syntax for ∀.

We can declare the create' function to be fully polymorphic as such

let create =
  let rec create' : 'a 'b. 'a list -> ('a, 'b) list_param -> 'b =
    fun (type a) (type b) (acc : a list) (elt : (a, b) list_param) : b ->
      match elt with
      | E d -> create' (d::acc)
      | X   -> List.rev acc 
    in  
    create' []
;;

First, notice that we split this function up into two pieces. The first piece is create' which names the function. We explicitly type create' with 'a 'b. 'a list -> ('a, 'b) list_param -> 'b which in English reads “for all alpha and beta create has type alpha list arrow alpha-beta list_param arrow beta.” This is a mouthful certainly, but it also illustrates how we quantify a type as being defined over all possible types 'a and 'b.

The second component to this function is a lambda which uses two local type variables. We define these variables a and b and use them to explicitly type our arguments. The reason we cannot use generic type variables 'a and 'b is that at the initial callsite for this lambda, the OCaml type checker will constrain 'a and 'b to be specific types. By using our own type variables, the type checker will keep them generic.

This is certainly confusing, and it worth playing with this function in utop in order to get a feel for how it works and why. Hopefully, at least, it demonstrates some of the expressiveness that GADTs provide and why we would consider using them.

A Triple Edged Blade

For the sake of not letting this article run on forever, I will end our discussion of GADTs here. They are incredibly powerful, but because of the limitations of OCaml’s type checker, often difficult to use. Furthermore, even with the best of type checkers it can be confusing to know how and when GADTs are appropriate, and why one would want them in one’s codebase. Speaking from experience, they can add a lot of complexity to, for instance, an otherwise simple type checker for a C-like language. However, their expressiveness provides a great means for creating interfaces and modules that are user friendly and powerful, especially for programmers used to weakly typed languages.

Hopefully this helps, and any questions can be left in the comments or emailed to me.