Notes on Dependent Types

How I’m beginning to (slowly) understand dependently typed programming languages.

In a dependently typed language, a type is allowed to depend on another variable. This makes it possible to describe a more precise situation in programming, such as a “vector of type A with length n”, which is different from a conventional typed language such as Rust or Java, where you can define a “vector of type A” (Vec<A>), which is a collection type of another subtype but without further a value constraint.

Let’s just imagine testing a definition of a vector in Rust:

let mut vec1 = vec![1, 2, 3, 4];
let mut vec2 = vec![5, 6];
vec1.append(&mut vec2);
assert_eq!(vec1, [1, 2, 3, 4, 5, 6]);
assert_eq!(vec1.len(), 6);

While this test works, there is an obvious point that can break this test. That is if vec1 or vec2 changed its value, the assertion becomes false. Simply put, the length of the output was hardcoded and not in any way connected to the definition of the vector. There is just no way to write a test that can constrain the resulting vector’s length outside of a human programmer's own hardcoded asserted value based on the input vectors.

Meanwhile, in a dependently typed programming language such as Agda, one can write code that defines the definition of a parametrized append function that can constrain the output based on the input of the function.

Here is a definition of a vector in Agda:

data Vec (M : Set) : Nat -> Set where
  []   : Vec M 0
  _::_ : {n : Nat} -> M -> Vec M n -> Vec M (suc n)

and then we define the vectors according to the types

vec1 : Vec Nat 0
vec1 = []
vec2 : Vec Nat 2
vec2 = 1 :: 0 :: []
vec3 : Vec Nat 3
vec3 = 4 :: 3 :: 2 :: []
vec4 : Vec (Bool -> Bool) 2
vec4 = not :: (\x -> x) :: []

Note that the types are all parametrized with the length of the vectors, and we call them indexed types. Hence, we are going beyond simple types in programming languages such as Rust and Java and conjuring types to help us prove the utmost correctness of the program.

Check out the definition of a function that appends two vectors:

_++_ : {A : Set} {m n : Nat} -> Vec A m -> Vec A n -> Vec A (m + n)
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

Now we can apply this function to the previously defined vectors to append them, and get the result typed checked at compile time!

appendedVec : Vec Nat 5
appendedVec : vec2 ++ vec3