One thing that no one touched on:<p>In reading Haskell (and apparently Idris) types, a name that starts with a lower case letter is an unbound type variable - sort of like a template parameter in C++.  The `a` in each of the Vect&#x27;s must be the same type but it can be any type (picked at the call site, for any given call).