Dependent Types in A Nutshell

August 12, 2017

Data types have not always been ubiquitous in high-level programming languages. The B programming language, a predecessor of C, is an an untyped language in which all data is simply machine words1. The B compiler does nothing to make sure that function arguments are sensible. For example, the B function putchar(c) assumes that c represents up to four ASCII characters packed into a machine word and prints the characters2. The rather contrived program

main() {
	auto n;
	n = 0;
	putchar('123*n');
}

simply prints the text 123, followed by a line break. ('*n' is the escape character for a line feed in B.) If I were to forget the single-quotes and write

putchar(123*n);

the expression 123*n would evaluate to 0, and putchar would happily accept its input and write a series of null bytes.

Type systems were introduced into programming languages to avoid such errors by making it impossible to represent certain invalid program states in source code. In C, I could define a function void putchar(char c) with the same behavior as the B version, but the C compiler would check the types of the function and its argument and complain if I were to pass it anything but a char.

There are much more expressive type systems around than the one in C; that is, there are type systems that are able to prevent much more complex program states. Arguably the most expressive type systems in modern programming languages are dependent type systems. A dependent type system is one in which types are first-class values, meaning that they can be inputs and outputs of functions just like any other value.3

Type-level functions are nothing new, although many programmers don’t know them as such. For example, the C# “type” List<T> is not really a type—I can’t instantiate it, after all—but a type constructor with a single parameter T. When I “call” the List<T> constructor with the argument int, it returns the new type List<int>.

The limitation of C# and most other languages with generics is that types cannot be intermixed with other values: I cannot define List<T, int n> or makeAList(type T, int n). This is where dependent types differ. In a dependently typed language, there is no separation between the type level and the value level. If I want to define a list that holds n items of type T, I would define List(type T, uint n). (I use parentheses instead of angle brackets because type constructors are now just a plain old functions.) Then, if I add an item to a list of type List(string, 4), the resulting list would be of type List(string, 5). I could even have functions like

print5Strings(List(string,5) strings)

or

addLists(uint length, List(int, length) list1, List(int, length) list2).

In the case of addLists, the type checker would look at the length parameter and make sure—at compile time—that the types of list1 and list2 matched it.

This sized-list type is one of the simplest possible applications of dependent types. A fully dependent type system allows the creation of types from any value, not just numbers, via arbitrarily complex computation. Unfortunately, checking types built through arbitrary, possibly non-terminating computations is not generally decidable. Full dependent type systems require some kind of theorem prover in order to check some of their types. However,

  1. enough is decidable to be useful without having to manually prove anything, and
  2. if the programmer is willing to put in enough work with the theorem prover, she can use the type system to enforce arbitrarily complex program behaviors at compile time.

For more information on programming with dependent types, see Edwin Brady’s Type-Driven Development with Idris.4


  1. “B (programming language)”, Wikipedia. https://en.wikipedia.org/wiki/B_(programming_language)

  2. Kernighan, B. W., “A tutorial introduction to the language B”. https://www.bell-labs.com/usr/dmr/www/btut.html

  3. Henk Barendregt’s lambda cube describes three orthogonal properties of type systems, one of which is dependent types. For simplicity, I’m muddling those properties together. Anyway, what I describe here is what people usually mean by dependent types. If you have a stomach for lambda calculus, see Barendregt, “Introduction to generalized type systems”, Journal of Functional Programming 1 (2): 125–154, April 1991. http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf

  4. https://www.manning.com/books/type-driven-development-with-idris