nickburrell.netlify.com

Return

Estimated Reading Time: 2 minutes

Dependent Functions

A depenedent function is a function who's return type can depend on the inputs it recieves. For instance, in Idris, it is possible to write the following.

dupElem : Vect n a -> Vect (2*n) a
dupElem : [] -> []
dupElem : (x::xs) = x :: x :: dupElem xs

Notice that here, the type Vect has a parameter n, which is not a type, in fact, it is a value of type Nat. This has many useful applications, especially to ensuring type safety. For instance, in many applications in C++, we use std::vector to store dynamic length arrays. Thankfully, there are many facilities in C++ to prevent reading garbage heap data, but its very easy, especially for new developers, to forget. Using something like std::array is inconvinient, because you need to break the value/type barrier for parameters, and end up with mixed functions like

template<typename T, std::size_t n> auto doThing(std::array<T, n> p) {
	// . . .
}

While this is completely fine, and very correct in many cases, it feels less natural, like blending two different aspects of the language. To recreate the Idris example in C++, we would need a function along the lines of

template<typename T, std::size_t n> auto doThing(std::array<T, n> p) {
	std::array<T, 2*n> arr();
	for(std::size_t i = 0u; i < n; ++i) {
		arr[2*i] = p[i];
		arr[2*i+1] = p[i];
	}
}

While both versions are very natural, there is an elegance to the first definition. There is no mixing of metaprogramming and normal functions, just a single unified definition.