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. ...

Get Type-Driven Development with Idris now with the O’Reilly learning platform.

O’Reilly members experience live online training, plus books, videos, and digital content from nearly 200 publishers.