Conclusion

In this introduction we learned about the most basic features of the Idris programming language. We used the REPL to tinker with our ideas and inspect the types of things in our code, and we used the Idris compiler to compile an Idris source file to an executable.

We also learned about the basic shape of a top level definition in Idris, which always consists of an identifier (its name), a type, and an implementation.

What's next?

In the next chapter, we start programming in Idris for real. We learn how to write our own pure functions, how functions compose, and how we can treat functions just like other values and pass them around as arguments to other functions.