I&#x27;m not an expert in Idris, but I will try to answer this as best as I can.<p>That&#x27;s the Haskell type notation (Idris and Haskell are similar). Here&#x27;s an example:<p><pre><code>  plus5 :: Int -&gt; Int
  plus5 n = n + 5
</code></pre>
The first line is the type declaration of the `plus5` function. You can read it as &quot;plus5 takes an Int as argument and returns another Int&quot;. The second line is the function declaration. The equivalent in Python would be:<p><pre><code>  def plus5(n):
      return n + 5
</code></pre>
The syntax is the same when functions have more arguments:<p><pre><code>  add :: Int -&gt; Int -&gt; Int
  add a b = a + b
</code></pre>
This means that add takes two integers as arguments and returns another integer. This syntax might look strange (you could be asking yourself &quot;How do I distinguish between the argument and return types?&quot;) but that&#x27;s because in Haskell functions are curried[1].<p>Haskell (and Idris as well) also has parametric polymorphism, so you can define functions which operate on generic types. For example, the identity function:<p><pre><code>  id :: a -&gt; a
  id x = x
</code></pre>
You can read this as &quot;`id` is a function that takes an argument of type a and returns another argument of type a (so the return type and argument type must be the same)&quot;. This means the id function will work for any type of argument (String, Float, Int, etc.). Note that of course this <i>is not</i> dynamic typing, Haskell and Idris are statically typed and therefore all the types are checked at compile-time.<p>Now, let&#x27;s move on to Idris. One of the reasons there&#x27;s a lot of excitement over Idris is because it has dependent types, i.e., you can declare types that depend on values and these are checked at compile-time.<p>The example GP gave was this:<p><pre><code>  app : Vect n a -&gt; Vect m a -&gt; Vect (n + m) a
</code></pre>
`app` here stands for append. This is the function that appends two vectors (lists of static length) together. In Idris, `Vect x y` is a vector of size x and type y, so<p><pre><code>   Vect 5 Int
</code></pre>
is a vector of 5 integers. So, essentially, `app` is a function that takes two vectors as arguments, `Vect n a` and `Vect m a` (this means they can be of different sizes but their content must be of the same type). It returns a `Vect (n + m) a`.<p>Think about it for a minute. That is amazing! We can be sure that, at compile-time, just by looking at the function signature, our append function, given two vectors of size n and m, will _always_ return a vector of size (n + m).<p>If we accidentally implement a function that does adhere to the type specification (for example, it appends the first argument to itself, returning a Vect of size (n + n) instead of (n + m)), the code will <i>not</i> compile and the compiler will tell us where is the bug.<p>[1]: <a href="http:&#x2F;&#x2F;learnyouahaskell.com&#x2F;higher-order-functions#curried-functions" rel="nofollow">http:&#x2F;&#x2F;learnyouahaskell.com&#x2F;higher-order-functions#curried-f...</a>