|
I'm not an expert in Idris, but I will try to answer this as best as I can. That's the Haskell type notation (Idris and Haskell are similar). Here's an example: plus5 :: Int -> Int
plus5 n = n + 5
The first line is the type declaration of the `plus5` function. You can read it as "plus5 takes an Int as argument and returns another Int". The second line is the function declaration. The equivalent in Python would be: def plus5(n):
return n + 5
The syntax is the same when functions have more arguments: add :: Int -> Int -> Int
add a b = a + b
This means that add takes two integers as arguments and returns another integer. This syntax might look strange (you could be asking yourself "How do I distinguish between the argument and return types?") but that's because in Haskell functions are curried[1].Haskell (and Idris as well) also has parametric polymorphism, so you can define functions which operate on generic types. For example, the identity function: id :: a -> a
id x = x
You can read this as "`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)". This means the id function will work for any type of argument (String, Float, Int, etc.). Note that of course this is not dynamic typing, Haskell and Idris are statically typed and therefore all the types are checked at compile-time.Now, let's move on to Idris. One of the reasons there'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. The example GP gave was this: app : Vect n a -> Vect m a -> Vect (n + m) a
`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 Vect 5 Int
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`.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). 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 not compile and the compiler will tell us where is the bug. [1]: http://learnyouahaskell.com/higher-order-functions#curried-f... |