<p><pre><code>    app : Vect n a -&gt; Vect m a -&gt; Vect (n + m) a
</code></pre>
is a type signature for a function, `app`, which should append a vector (`Vect`) of length `n` to a vector of length `m`.<p>What&#x27;s cool about Idris and other dependently-typed languages is that the length of the resulting vector, `n + m`, can be tracked in the type. This can prevent a whole slew of errors.