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.[1] 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.

2.1. Basic types

2.1.1. Numeric types and values

2.1.2. Type conversions using cast

2.1.3. Characters and strings

2.1.4. Booleans

2.2. Functions: the building blocks of Idris programs

2.2.1. Function types and definitions

2.2.2. Partially applying functions

2.2.3. Writing generic functions: variables in types

2.2.4. Writing generic functions with constrained types

2.2.5. Higher-order function types

2.2.6. Anonymous functions

2.2.7. Local definitions: let and where

2.3. Composite types

2.3.1. Tuples

2.3.2. Lists

2.3.3. Functions with lists

2.4. A complete Idris program

2.4.1. Whitespace significance: the layout rule

2.4.2. Documentation comments

2.4.3. Interactive programs

2.5. Summary

sitemap