Chapter 2. Getting started with Idris
This chapter covers
- Using built-in types and functions
- Defining functions
- Structuring Idris programs
When learning any new language, it’s important to have a solid grasp of the fundamentals before moving on to the more distinctive features of the language. With this in mind, before we begin exploring dependent types and type-driven development itself, we’ll look at some types and values that will be familiar to you from other languages, and you’ll see how they work in Idris. You’ll also see how to define functions and put these together to build a complete, if simple, Idris program.
If you’re already familiar with a pure functional language, particularly Haskell, much of this chapter will seem very familiar. Listing 2.1 shows a simple, but self--contained, Idris program that repeatedly prompts for input from the console and then displays the average length of the words in the input. If you’re already comfortable reading this program with the help of the annotations, you can safely skip this chapter, as it deliberately avoids introducing any language features specific to Idris. Even so, I still suggest you browse through this chapter’s tips and notes and read the summary at the end to make sure there aren’t any small details you’ve missed.
Otherwise, don’t worry. By the end of this chapter we’ll have covered all of the necessary features for you to be able to implement similar programs yourself.