This post is a continuation of my journey into Agda following this post. I am following along the lectures of CS410 by Fredrik Forsberg. You can clone the repository for the lecture series here.
data List (A : Set) : Set where
[] : List A
_::_ : A -> List A -> List A
Coming from Haskell, this is a straightforward definition of a list using GADTs.
{-# LANGUAGE GADTs #-}
data List a where
[] :: List a
(:) :: a -> List a -> List a
In haskell, the head function throws an error on an empty list.
head :: [a] -> a
head [] = error "empty list"
head (a:as) = a
Let's try defining a head function in agda.
head : List A -> A
head (a :: as) = a
We can not define an error case because functions have to be total in agda which means computations must terminate by returning a value and not an error as Haskell would. So, agda rightfully complains about a missing case for [].
Incomplete pattern matching for head. Missing cases:
head []
when checking the definition of head
Now, what if we had a way of embedding the length of a list in its type? This idea walks like a C++ duck and quacks like a C++ duck, so let's try shaping this in C++.
template <typename T, size_t n, typename = std::enable_if_t<(n > 0)>>
constexpr T head(std::array<T, n> as) {
return as[0];
}
constexpr auto a = head(std::array<int, 1>{1}); // works
constexpr auto b = head(std::array<int, 0>{}); // error
We have a rough idea of what we want so let's try the same in agda.
data Vec (A : Set) : Nat -> Set where
[] : Vec A 0
_::_ : ∀ {n} -> A -> Vec A n -> Vec A (suc n)
I found Dependent types at work to be an excellent source explaining the syntactic constructs in use, which my explanation below adapts.
Dependent types are types that depend on elements of other types
Vec has type Vec : Set -> Nat -> Set where Vec accepts a small type and an inductively defined natural number. Set, a large type, is a collection of small types like Nat. The reason why we don't usually call the parameterized C++ type std::array<T, n> dependently typed is because the typename T can be any type, while agda's A : Set, A is an element of another type Set and n is an element of another type Nat. Equivalently, Vec is indexed by elements of type Set and Nat. We don't yet have a formal definition of what a dependent type is, so let's agree that our explanation matches the definition above.
A in Vec (A : Set) : Nat -> Set is an implicit argument to its constructors [] and _::_. Written as free functions, the implicit argument expansion is equivalent to
[] : {A : Set} -> List A
_::_ : {A : Set} -> A -> List A -> List A
head for a VecLet's try defining head again, knowing that we have access to the length of a Vec.
head : ∀ {n : Nat} -> {A : Set} -> Vec A n -> A
head {n} {A} (x :: xs) = x
To understand why this is still incomplete, consider the two cases
Vec A n can be pattern matched to Vec A (suc x) and therefore, the second constructor can be matched against A -> Vec A x -> Vec A (suc x). head is simply the first element of type A.
Vec A 0 can only be matched to []. We are not able to construct any value of type A and so, our function is not total. Intuitively, head is only defined for non-empty Vectors, so let's encode that in the type.
head : ∀ {n : Nat} -> {A : Set} -> Vec A (suc n) -> A
head {n} {A} (x :: xs) = x
Finally, the burden of proof is now on the caller who must provide a non-empty vector because [] would simply not be accepted by head. When we try calling head on an arbitrary vector Vec A n, we get the error
n != (suc _n_40) of type Nat
Defining tail is similar (the implicit arguments are elided)
tail : ∀ {A n} -> Vec A (suc n) -> Vec A n
tail (x :: xs) = xs
In the next post, we will look at the Fin type and how we use Fin to define head and tail.