The Idris 2 Programming Language

by Stefan Höck, Nathan McCarty, and others

Welcome to the community Idris 2 tutorial! This book aims to be a comprehensive resource for learning the Idris 2 programming language.

This book is rendered from a collection of Idris source files structured as a normal Idris project, which you can download and play around with.

Introduction

Many of the Markdown files making up this book (those with a .md file extension) are literate Idris files, consisting of a mixture of Markdown and Idris code, and can be type checked and built just like regular code by the Idris compiler. You can identify a document as a literate Idris document if it contains a module declaration, like so:

module Tutorial.Intro

Even though this file (src/Tutorial/Intro.md) has no actual code in it, by including that module declaration, it qualifies as a literate Idris file. A module name consists of a list of identifiers separated by dots and must reflect the folder structure plus the module file's name, starting from the source directory. For instance, as this file's path, from the root of the src directory is Tutorial/Intro.md, it's module name must be Tutorial.Intro.

Before starting this book, make sure you have the Idris compiler installed on your computer. While it is technically possible to work through this book without it, we recommend that you have the pack package manager installed and have a skeleton package setup as described in the Getting Started with pack and Idris2 appendix, as such a setup is assumed.

Later in the book, you will encounter various exercises. The solutions to these exercises can be found as regular Idris files in the src/Solutions directory of the git repository, or in syntax highlight form in the "Exercise Solutions" section at the bottom of the navigation sidebar.

About the Idris Programming Language

Idris is a pure, dependently typed, total functional programming language.

Lets break that down and explore what each of those terms means on their own.

Functional Programming

In functional programming languages, functions are first-class constructs, meaning that they can be assigned to variables, passed as arguments to other functions, and returned as results from functions, just like any other value in the language. Unlike in, for instance, object-oriented languages, functions are the main form of abstraction in functional programming.

Whenever we find a common pattern or (almost) identical code in several parts of a project, we try to implement an abstraction over it to avoid write the same code multiple times. In functional programming, we do this by introducing one or more new functions implementing the required behavior, often trying to be as general as possible to maximize the versatility and re-usability of our functions.

Functional programming languages are concerned with the evaluation of functions, unlike imperative languages, which are concerned with the execution of statements.

Pure Functional Programming

Pure functional programming languages come with an additional important guarantee:

Functions don't have side effects, like writing to a file or mutating global state. They can only compute a result from their arguments possibly by invoking other pure functions, and nothing else. Given the same input, a pure function will always generate the same output, this property is known as referential transparency.

Pure functions have several advantages:

• They are easy to test by specifying (possibly randomly generated) sets of input arguments alongside the expected results.

• They are thread-safe. Since they don't mutate global state, they be used in several computations running in parallel without interfering with each other.

There are, of course, also some disadvantages:

• Some algorithms are hard to implement efficiently with only pure functions.

• Writing programs that actually do something (have some observable effect) is a bit tricky, but certainly possible.

Dependent Types

Idris is a strongly, statically typed programming language. Every expression is given a type (for instance: integer, list of strings, boolean, function from integer to boolean, etc.), and types are verified at compile time to rule out certain common programming errors.

For instance, if a function expects an argument of type String (a sequence of unicode characters, such as "Hello123"), it is a type error to invoke this function with an argument of type Integer, and Idris will refuse to compile such an ill-typed program.

Being statically typed means that Idris will catch type errors at compile time, before it generates an executable program that can be run. This stands in contrast with dynamically typed languages such as Python, which check for type errors at runtime, while a program is already being executed. It is the goal of statically typed languages to catch as many type errors as possible before there even is a program that can be run.

Furthermore, Idris is dependently typed, which is one of its most characteristic properties in comparison to other programming languages. In Idris, types are first class: Types can be passed as arguments to functions, and functions can return types as their results. Types can also depend on other values, as one example, the return type of a function can depend on the value of one of its arguments. This is a quite abstract statement that may be difficult to grasp at first, but we will be exploring its meaning and the profound impact it has on programming through example as we move through this book.

Total Functions

A total function is a pure function which is guaranteed to return a value of its return type for every possible set of inputs in a finite number of computational steps. A total function will never fail with an exception or loop infinitely, although it can still take arbitrarily long to compute its result.

Idris comes with a totality checker built-in, which allows us to verify that the functions we write are provably total. Totality in Idris is opt-in, as checking the totality of an arbitrary computer program is undecidable in the general case (a dilemma you may recognize as the halting problem). However, if we annotate a function with the total keyword, and the totality checker is unable to verify that the function is, indeed, total, Idris will fail with a type error. Notably, failing to determine a function is total is not the same as judging the function to be non-total.

Using the REPL

Idris comes with a REPL (Read Evaluate Print Loop), which is useful for tinkering with small ideas, and for quickly experimenting with the code we just wrote. To start a REPL session, run the following command in a terminal:

pack repl

Idris should now be ready to accept your commands:

     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.5.1-3c532ea35
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main>

We can go ahead and enter some simple arithmetic expressions, Idris will evaluate them and print the result:

Main> 2 * 4
8
Main> 3 * (7 + 100)
321

Since every expression in Idris has a type, we might want to inspect those as well:

Main> :t 2
2 : Integer

:t is a command specific to the Idris REPL (it is not part of the Idris programming language), and it is used to inspect the type of an expression:

Main> :t 2 * 4
2 * 4 : Integer

Whenever we perform calculations involving integer literals without explicitly specifying the types involved, Idris will assume the Integer type by default. Integer is an arbitrary precision (there is no hard-coded maximum value) signed integer type. It is one of the primitive types built into the language. Other primitives include fixed precision signed and unsigned integral types (Bits8, Bits16, Bits32 Bits64, Int8, Int16, Int32, and Int64), double precision (64 bit) floating point numbers (Double), unicode characters (Char) and strings of unicode characters (String).

A First Idris Program

module Tutorial.Intro.FirstIdrisProgram

While we will often start with the REPL for tinkering with small parts of the Idris language, for reading some documentation, or for inspecting the content of an Idris module, lets go ahead and will write a minimal Idris program to get started with the language.

Here comes the mandatory Hello World:

main : IO ()
main = putStrLn "Hello World!"

We will inspect the code above in some detail in a moment, but first we'd like to compile and run it. If you have checked out this books source code, you can run the following from the root directory:

pack -o hello exec src/Tutorial/Intro/FirstIdrisProgram.md

This will create an executable called hello in the build/exec directory, which can be invoked from the command-line like so (without the dollar prefix; this is used here to distinguish the terminal command from its output):

$ build/exec/hello
Hello World!

The pack program requires an .ipkg to be in scope (in the current directory or one of its parent directories), which provides other settings like the source directory to use (src in our case). The optional -o option provides a name to use for the executable to be generated. Pack comes up with a name of its own it this is not provided. Type pack help for a list of available command-line options and commands, and pack help <cmd> for help with a specific command.

You can also load this source file in a REPL session and invoke function main from there:

pack repl src/Tutorial/Intro/FirstIdrisProgram.md

Tutorial.Intro> :exec main
Hello World!

Go ahead and try both ways of building and running main on your system!

The Shape of an Idris Definition

module Tutorial.Intro.ShapeOfADef

Now that we have executed our first Idris program, lets talk a bit more about the code we had to write to define it.

A typical top level function in Idris consists of three things:

1. The function's name (main in our case)
2. Its type (IO ())
3. Its implementation (putStrLn "Hello World")

Lets explore these parts through a couple of examples, starting out by defining a constant for the largest unsigned 8 bit integer:

maxBits8 : Bits8
maxBits8 = 255

The first line can be read as:

We'd like to declare a (nullary, or zero argument) function maxBits8. It is of type Bits8.

This is called the function declaration, we declare that there shall be a function of the given name and type.

The second line reads:

The result of invoking maxBits8 should be 255. (As you can see, we can use integer literals for other integral types and not just Integer.)

This is called the function definition, the function maxBits8 should behave as described here when being evaluated.

We can inspect this at the REPL, load this source file into an Idris REPL (as described in the previous section, this time using src/Tutorial/Intro/ShapeOfADef.md as the source file), and try running the following tests:

Tutorial.Intro> maxBits8
255
Tutorial.Intro> :t maxBits8
Tutorial.Intro.maxBits8 : Bits8

We can also use maxBits8 as part of another expression:

Tutorial.Intro> maxBits8 - 100
155

We previously described maxBits8 as a nullary function, which is just a fancy word for a constant. Let's write and test our first real function:

distanceToMax : Bits8 -> Bits8
distanceToMax n = maxBits8 - n

This introduces some new syntax and a new kind of type: Function types.

distanceToMax : Bits8 -> Bits8 can be read as:

distanceToMax is a function of one argument, with type Bits8, which returns a result of type Bits8.

In the implementation, the argument is given a local identifier (a fancy term for "name") n, which is then used in the calculation on the right hand side. Go ahead and try this function at the REPL:

Tutorial.Intro> distanceToMax 12
243
Tutorial.Intro> :t distanceToMax
Tutorial.Intro.distanceToMax : Bits8 -> Bits8
Tutorial.Intro> :t distanceToMax 12
distanceToMax 12 : Bits8

As a final example, let's implement a function that calculates the square of an integer:

square : Integer -> Integer
square n = n * n

We now learn a very important aspect of programming in Idris: Idris is a statically typed programming language. We are not allowed to freely mix types as we please, doing so will result in an error message from the type checker (which is part of Idris's compilation process). For instance, if we try the following at the REPL, we will get a type error:

Tutorial.Intro> square maxBits8
Error: ...

This is because square expects an argument of type Integer, but maxBits8 is of type Bits8. Many primitive types can be converted back and forth between each other (sometimes with the risk of loss of precision) using function cast (we will cover cast in further detail in the section on Interfaces in the Prelude):

Tutorial.Intro> square (cast maxBits8)
65025

Notice that the above result is much larger than maxBits8. This is because maxBits8 is first converted to an Integer of the same value, which is then squared. If we instead squared maxBits8 directly, the result would be truncated to still fit in the range of valid Bits8s:

Tutorial.Intro> maxBits8 * maxBits8
1

Where to get Help

There are several resources available online and in print, where you can find help and documentation about the Idris programming language. Here is a non-comprehensive list:

• Type-Driven Development with Idris

  The Idris book! This describes in great detail the core concepts for using Idris and dependent types to write robust and concise code. It uses Idris 1 in its examples, so parts of it have to be slightly adjusted when using Idris 2. There is also a list of required updates.

• A Crash Course in Idris 2

  The official Idris 2 tutorial. A comprehensive but dense explanation of all features of Idris 2. I find this to be useful as a reference, and as such it is highly accessible. However, it is not an introduction to functional programming or type-driven development in general.

• The Idris 2 GitHub Repository

  Look here for detailed installation instructions and some introductory material. There is also a wiki, where you can find a list of editor plugins, a list of external backends, and other useful information.

• The pack Database

  This is the listing of all the libraries included in pack's collection, which is currently the most comprehensive source of community contributed libraries for Idris 2.

• The Idris 2 Discord Channel

  If you get stuck with a piece of code, want to ask about some obscure language feature, want to promote your new library, or want to just hang out with other Idris programmers, this is the place to go. The discord channel is pretty active and very friendly towards newcomers.

• The Idris REPL

  Finally, a lot of useful information can be provided by Idris itself. Many users tend to kep at least one REPL open while working on an Idris project. Text editors can be set up to use the language server for Idris 2, which is incredibly useful. In the REPL,

  • use :t to inspect the type of an expression or meta variable (hole): :t foldl,
  • use :ti to inspect the type of a function including implicit arguments: :ti foldl,
  • use :m to list all meta variables (holes) in scope,
  • use :doc to access the documentation of a top level function (:doc the), a data type plus all its constructors and available hints (:doc Bool), a language feature (:doc case, :doc let, :doc interface, :doc record, or even :doc ?), or an interface (:doc Uninhabited),
  • use :module to import a module from one of the available packages: :module Data.Vect,
  • use :browse to list the names and types of all functions exported by a loaded module: :browse Data.Vect,
  • use :help to get a list of other commands plus a short description for each.

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.

Introduction To Functions

Idris is a functional programming language, functions are its main form of abstraction (unlike for instance in an object oriented language like Java, where objects and classes are the main form of abstraction). Thus, we expect Idris to make it very easy for us to compose and combine functions to create new functions. In fact, in Idris functions are first class, functions can take other functions as arguments and can return functions as their results.

This chapter will explore some of the basic tools Idris provides for combining and producing functions .

Functions with more than one Argument

module Tutorial.Functions1.FunctionsWithMultipleArguments

Let's implement a function, which checks if its three Integer arguments form a Pythagorean triple, we'll need to use a new operator for this: ==, the equality operator.

export
isTriple : Integer -> Integer -> Integer -> Bool
isTriple x y z = x * x + y * y == z * z

Let's give this a spin at the REPL before we talk a about the types:

Tutorial.Functions1> isTriple 1 2 3
False
Tutorial.Functions1> isTriple 3 4 5
True

As this example demonstrates, the type of a function of several arguments consists of a sequence of argument types (also called input types) chained by function arrows (->), terminated by an output type (Bool in this case).

The implementation looks like a mathematical equation: The arguments are listed on the left hand side of the =, and the computation(s) to perform with them are described on the right hand side.

Function implementations in functional programming languages often have a more mathematical look compared to implementations in imperative languages, which often describe not what to compute, but instead how to compute it by describing an algorithm as a sequence of imperative statements. This imperative style is also available in Idris, and we will explore it in later chapters, but we prefer the declarative style whenever possible.

As shown in the above example, functions can be invoked by passing the arguments separated by whitespace. No parentheses are necessary, unless one of the expressions we pass as the function's arguments contains its own additional whitespace. This syntax provides for particularly ergonomic partial function application, a concept we will cover in a later section.

Note that, unlike Integer or Bits8, Bool is not a primitive data type built into the Idris language but just a normal data type that you could have written yourself. We will cover data type definitions in the next chapter

Function Composition

module Tutorial.Functions1.FunctionComposition

Functions can be combined in several ways, the most direct probably being the dot (.) operator:

export
square : Integer -> Integer
square n = n * n

times2 : Integer -> Integer
times2 n = 2 * n

squareTimes2 : Integer -> Integer
squareTimes2 = times2 . square

Give this a try at the REPL! Does it do what you'd expect?

We could have implemented squareTimes2 without using the dot operator as follows:

squareTimes2' : Integer -> Integer
squareTimes2' n = times2 (square n)

To get a better insight into how the dot operator works, let's implement our own version of it, instead called <.> to avoid name collision with the built-in dot operator:

private infixr 9 <.>
(<.>) : (b -> c) -> (a -> b) -> a -> c
f <.> g = \x => (f (g x))

We'll cover more about functions that take other functions as arguments in the next section, but for now, it suffices to know that our <.> is identical to the built-in ., and can be used the same way:

squareTimes2'' : Integer -> Integer
squareTimes2'' = times2 <.> square

It is important to note that functions chained by the dot operator are invoked from right to left: times2 . square is the same as \n => times2 (square n) and not \n => square (times2 n). This can be seen in our definition of <.>.

We can conveniently chain several functions using the dot operator to write more complex functions:

dotChain : Integer -> String
dotChain = reverse . show . square . square . times2 . times2

This will first multiply the argument by four, then square it twice before converting it to a string (show) and reversing the resulting String (functions show and reverse are part of the Idris Prelude and as such are available in every Idris program).

Higher-order Functions

module Tutorial.Functions1.HigherOrder

import Tutorial.Functions1.FunctionComposition

Functions can take other functions as arguments. This is an incredibly powerful concept which can be taken to an extreme very easily, but to keep things simple, we'll start slowly:

isEven : Integer -> Bool
isEven n = mod n 2 == 0

testSquare : (Integer -> Bool) -> Integer -> Bool
testSquare fun n = fun (square n)

In the above definition, isEven uses the mod function to check if an integer is divisible by two, and is defined in the same straightforward manor as the other functions we have defined so far.

testSquare, however, is more interesting. It takes two arguments, the first argument having the type of a function from Integer to Bool, and the second having type Integer. The second argument is squared before being passed to the first argument.

Let's give this a go at the REPL:

Tutorial.Functions1> testSquare isEven 12
True

Take your time to understand what's going on here. We pass the function isEven as the first argument to testSquare. The second argument is an integer, which will first be squared and then passed to isEven. While this particular example is not very interesting, we will cover lots of use cases for passing functions as arguments to other functions as we continue.

As noted earlier, things can go to an extreme pretty easily. Consider the following example:

twice : (Integer -> Integer) -> Integer -> Integer
twice f n = f (f n)

And at the REPL:

Tutorial.Functions1> twice square 2
16
Tutorial.Functions1> (twice . twice) square 2
65536
Tutorial.Functions1> (twice . twice . twice . twice) square 2
*** huge number ***

You might be surprised about this behavior, so let's break it down. The following two expressions are identical in their behavior:

expr1 : Integer -> Integer
expr1 = (twice . twice . twice . twice) square

expr2 : Integer -> Integer
expr2 = twice (twice (twice (twice square)))

Let's walk through this:

• square raises its argument to the 2nd power
• twice square applies square twice, raising its argument to the 4th power
• twice (twice square) raises it to the 16th power, by invoking twice square twice
• And so on until twice (twice (twice (twice square))), which raises it's argument to the 65536th power, giving an impressively huge result

Currying

module Tutorial.Functions1.Currying

import Tutorial.Functions1.FunctionsWithMultipleArguments

Once we start using higher-order functions, the concept of partial function application (also called currying after mathematician and logician Haskell Curry) becomes very important.

Load this file in a REPL session and try the following:

Tutorial.Functions1.Currying> :t testSquare isEven
testSquare isEven : Integer -> Bool
Tutorial.Functions1.Currying> :t isTriple 1
isTriple 1 : Integer -> Integer -> Bool
Tutorial.Functions1.Currying> :t isTriple 1 2
isTriple 1 2 : Integer -> Bool

Notice how in Idris we can partially apply a function with more than one argument and, as a result, get a new function back. For instance, isTriple 1 applies argument 1 to function isTriple and returns a new function of type Integer -> Integer -> Bool. We can even use the result of such a partially applied function in a new top level definition:

partialExample : Integer -> Bool
partialExample = isTriple 3 4

And at the REPL:

Tutorial.Functions1.Currying> partialExample 5
True

We already used partial function application in our twice examples above to get some impressive results with very little code.

Anonymous Functions

module Tutorial.Functions1.Lambdas

import Tutorial.Functions1.FunctionsWithMultipleArguments

Sometimes we'd like to pass a small custom function to a higher-order function, but without the hassle writing a top level definition. For instance, in the following example, function someTest is very specific and probably not very useful in general, but we'd still like to pass it to higher-order function testSquare:

someTest : Integer -> Bool
someTest n = n >= 3 || n <= 10

Here's, how to pass it to testSquare:

Tutorial.Functions1> testSquare someTest 100
True

Instead of defining and using someTest, we can use an anonymous function:

Tutorial.Functions1> testSquare (\n => n >= 3 || n <= 10) 100
True

For clarity, lets use an anonymous function to reproduce the above definition:

someTest' : Integer -> Bool
someTest' = \n => n >= 3 || n <= 10

Anonymous functions are sometimes also called lambdas (from lambda calculus), and the backslash is chosen since it resembles the Greek letter lambda.

The \n => syntax introduces a new anonymous function of one argument called n, the implementation of which is given on the right hand side of the function arrow. Like other top level functions, lambdas can have more than one arguments, separated by commas: \x,y => x * x + y. When we pass lambdas as arguments to higher-order functions, they typically need to be wrapped in parentheses or separated by the dollar operator ($) (see the next section about this).

Note that, in a lambda, arguments are not annotated with types, so Idris has to be able to infer them from the current context.

Operators

module Tutorial.Functions1.Operators

In Idris, infix operators like ., * or + are not built into the language, they are instead just regular Idris function with some special support for using them in infix notation. When we use operators outside of infix notation, we have to wrap them in parentheses.

As an example, let us define a custom operator for sequencing functions of type Bits8 -> Bits8:

infixr 4 >>>

(>>>) : (Bits8 -> Bits8) -> (Bits8 -> Bits8) -> Bits8 -> Bits8
f1 >>> f2 = f2 . f1

foo : Bits8 -> Bits8
foo n = 2 * n + 3

test : Bits8 -> Bits8
test = foo >>> foo >>> foo >>> foo

In addition to declaring and defining the operator itself, we also have to specify its fixity: infixr 4 >>> means, that (>>>) associates to the right (meaning, that f >>> g >>> h is to be interpreted as f >>> (g >>> h)) with a priority of 4. You can also have a look at the fixity of operators exported by the Prelude in the REPL:

Tutorial.Functions1> :doc (.)
Prelude.. : (b -> c) -> (a -> b) -> a -> c
  Function composition.
  Totality: total
  Fixity Declaration: infixr operator, level 9

When you mix infix operators in an expression, those with a higher priority bind more tightly. For instance, (+) is left associated with a priority of 8, while (*) is left associated with a priority of 9. Hence, a * b + c is the same as (a * b) + c instead of a * (b + c).

Operator Sections

Operators can be partially applied just like regular functions. In this case, the whole expression has to be wrapped in parentheses and is called an operator section. Here are two examples:

Tutorial.Functions1> testSquare (< 10) 5
False
Tutorial.Functions1> testSquare (10 <) 5
True

As you can see, there is a difference between (< 10) and (10 <). The first tests whether its argument is less than 10, and the second tests whether 10 is less than its argument.

One exception where operator sections will not work is with the minus operator (-). Here is an example to demonstrate this:

applyToTen : (Integer -> Integer) -> Integer
applyToTen f = f 10

This is just a higher-order function applying the number ten to its function argument. This works very well in the following example:

Tutorial.Functions1> applyToTen (* 2)
20

However, if we want to subtract five from ten, the following will fail:

Tutorial.Functions1> applyToTen (- 5)
Error: Can't find an implementation for Num (Integer -> Integer).

(Interactive):1:12--1:17
 1 | applyToTen (- 5)

The problem here is that Idris treats - 5 as an integer literal instead of an operator section. In this special case, we have to use an anonymous function instead:

Tutorial.Functions1> applyToTen (\x => x - 5)
5

Infix Notation for Non-Operators

In Idris, it is possible to use infix notation for regular binary functions by wrapping them in backticks. It is even possible to define a precedence (fixity) for these and use them in operator sections, just like regular operators:

infixl 8 `plus`

infixl 9 `mult`

plus : Integer -> Integer -> Integer
plus = (+)

mult : Integer -> Integer -> Integer
mult = (*)

arithTest : Integer
arithTest = 5 `plus` 10 `mult` 12

arithTest' : Integer
arithTest' = 5 + 10 * 12

Operators exported by the Prelude

Here is a list of important operators exported by the Prelude:

• (.): Function composition
• (+): Addition
• (*): Multiplication
• (-): Subtraction
• (/): Division
• (==) : True, if two values are equal
• (/=) : True, if two values are not equal
• (<=), (>=), (<), and (>) : Comparison operators
• ($): Function application

Most of these are constrained, that is they work only for types implementing a certain interface. Don't worry about this right now. We will learn about interfaces their own chapter later, and the operators behave as they intuitively should. For instance, addition and multiplication work for all numeric types, and comparison operators work for almost all types in the Prelude with the exception of functions.

The most special of the above is the last one, ($). It has a priority of 0, so all other operators bind more tightly. In addition, function application binds more tightly, so this can be used to reduce the number of parentheses required in an expression. For instance, instead of writing isTriple 3 4 (2 + 3 * 1) we can write isTriple 3 4 $ 2 + 3 * 1, with exactly the same meaning. Sometimes this helps readability, other times it doesn't, you will naturally build an intuition for which form of a given expression is more readable with experience, especially from rereading your own code after some time has passed. The important thing to remember is that fun $ x y is just the same as fun (x y).

Introductory Function Exercises

module Tutorial.Functions1.Exercises

The solutions to these exercises can be found in src/Solutions/Functions1.idr.

Exercise 1

Reimplement functions testSquare and twice by using the dot operator and dropping the second arguments (have a look at the implementation of squareTimes2 to get an idea where this should lead you). This highly concise way of writing function implementations is sometimes called point-free style and is often the preferred way of writing small utility functions.

Exercise 2

Declare and implement function isOdd by combining functions isEven from above and not (from the Idris Prelude). Use point-free style.

Exercise 3

Declare and implement function isSquareOf, which checks whether its first Integer argument is the square of the second argument.

Exercise 4

Declare and implement function isSmall, which checks whether its Integer argument is less than or equal to 100. Use one of the comparison operators <= or >= in your implementation.

Exercise 5

Declare and implement function absIsSmall, which checks whether the absolute value of its Integer argument is less than or equal to 100. Use functions isSmall and abs (from the Idris Prelude) in your implementation, which should be in point-free style.

Exercise 6

In this slightly extended exercise we are going to implement some utilities for working with Integer predicates (functions from Integer to Bool). Implement the following higher-order functions (use boolean operators &&, ||, and function not in your implementations):

-- return true, if and only if both predicates hold
and : (Integer -> Bool) -> (Integer -> Bool) -> Integer -> Bool

-- return true, if and only if at least one predicate holds
or : (Integer -> Bool) -> (Integer -> Bool) -> Integer -> Bool

-- return true, if the predicate does not hold
negate : (Integer -> Bool) -> Integer -> Bool

After solving this exercise, give it a go in the REPL. In the example below, we use binary function and in infix notation by wrapping it in backticks. This is just a syntactic convenience to make certain function applications more readable:

Tutorial.Functions1> negate (isSmall `and` isOdd) 73
False

Exercise 7

As explained above, Idris allows us to define our own infix operators. Even better, Idris supports overloading of function names, that is, two functions or operators can have the same name, but different types and implementations. Idris will make use of the types to distinguish between equally named operators and functions.

This allows us, to reimplement functions and, or, and negate from Exercise 6 by using the existing operator and function names from boolean algebra:

-- return true, if and only if both predicates hold
(&&) : (Integer -> Bool) -> (Integer -> Bool) -> Integer -> Bool
x && y = and x y

-- return true, if and only if at least one predicate holds
(||) : (Integer -> Bool) -> (Integer -> Bool) -> Integer -> Bool

-- return true, if the predicate does not hold
not : (Integer -> Bool) -> Integer -> Bool

Implement the other two functions and test them at the REPL:

Tutorial.Functions1> not (isSmall && isOdd) 73
False

Conclusion

In this chapter, we learned:

• A function in Idris can take an arbitrary number of arguments, separated by -> in the function's type.

• Functions can be combined sequentially using the dot operator (.), which leads to concise code.

• Functions can be partially applied by passing them fewer arguments than they expect, resulting in a new function expecting the remaining arguments. This technique is called currying.

• Functions can be passed as arguments to other functions, which allows us to easily combine small units of code to create more complex behavior.

• If writing a corresponding top level function would be too cumbersome, we can pass anonymous functions (lambdas) to higher-order functions.

• Idris allows us to define our own infix operators. These have to be written in parentheses unless they are being used in infix notation.

• Infix operators can also be partially applied. These operator sections have to be wrapped in parentheses, and the position of the argument determines whether it is used as the operator's first or second argument.

• Idris supports name overloading, functions can have the same names but different implementations. Idris will decide which function to use based to the types involved.

Please note, that function and operator names within an individual a module must be unique. In order to define two functions with the same name, they have to be declared in distinct modules. If Idris is not able to decide which of the two functions to use, we can help name resolution by prefixing a function with (a part of) its namespace:

Tutorial.Functions1> :t Prelude.not
Prelude.not : Bool -> Bool
Tutorial.Functions1> :t Functions1.not
Tutorial.Functions1.not : (Integer -> Bool) -> (Integer -> Bool) -> Integer -> Bool

What's next

In the next section, we will learn how to define our own data types and how to construct and deconstruct values of these new types. We will also learn about generic types and functions.

Algebraic Data Types

In the previous chapter, we learned how to write our own functions and combine them to create more complex functionality. Of equal importance is the ability to define our own data types and use them as arguments and results in functions.

This is a lengthy chapter, densely packed with information. If you are new to Idris and functional programming, make sure to follow along slowly, experimenting with the examples, and possibly coming up with your own. Make sure to try and solve all exercises.

module Tutorial.DataTypes

Enumerations

module Tutorial.DataTypes.Enumerations

Let's start with a data type for the days of the week as an example.

public export
data Weekday = Monday
             | Tuesday
             | Wednesday
             | Thursday
             | Friday
             | Saturday
             | Sunday

The declaration above defines a new type (Weekday) and several new values (Monday to Sunday) of the given type. Go ahead, and verify this at the REPL:

Tutorial.DataTypes> :t Monday
Tutorial.DataTypes.Monday : Weekday
Tutorial.DataTypes> :t Weekday
Tutorial.DataTypes.Weekday : Type

So, Monday is of type Weekday, while Weekday itself is of type Type.

It is important to note that a value of type Weekday can only ever be one of the values listed above. It is a type error to use anything else where a Weekday is expected.

Pattern Matching

In order to use our new data type as a function argument, we need to learn about an important concept in functional programming languages: Pattern matching. Let's implement a function which calculates the successor of a weekday:

total
next : Weekday -> Weekday
next Monday    = Tuesday
next Tuesday   = Wednesday
next Wednesday = Thursday
next Thursday  = Friday
next Friday    = Saturday
next Saturday  = Sunday
next Sunday    = Monday

In order to inspect a Weekday argument, we match on the different possible values and return a result for each of them. This is a very powerful concept, as it allows us to match on and extract values from deeply nested data structures. The different cases in a pattern match are inspected from top to bottom, each being compared against the current function argument. Once a matching pattern is found, the computation on the right hand side of this pattern is evaluated. Later patterns are then ignored.

For instance, if we invoke next with argument Thursday, the first three patterns (Monday, Tuesday, and Wednesday) will be checked against the argument, but they do not match. The fourth pattern is a match, and result Friday is being returned. Later patterns are then ignored, even if they would also match the input (this becomes relevant with catch-all patterns, which we will talk about in a moment).

The function above is provably total. Idris knows about the possible values of type Weekday, and can therefore figure out that our pattern match covers all possible cases. We can therefore annotate the function with the total keyword, and Idris will answer with a type error if it can't verify the function's totality. (Go ahead, and try removing one of the clauses in next to get an idea about how an error message from the coverage checker looks like.)

Please remember that these are very strong guarantees from the type checker: Given enough resources, a provably total function will always return a result of the given type in a finite amount of time (resources here meaning computational resources like memory or, in case of recursive functions, stack space).

Catch-all Patterns

Sometimes, it is convenient to only match on a subset of the possible values and collect the remaining possibilities in a catch-all clause:

export
total
isWeekend : Weekday -> Bool
isWeekend Saturday = True
isWeekend Sunday   = True
isWeekend _        = False

The final line with the catch-all pattern is only invoked if the argument is not equal to Saturday or Sunday. Remember: Patterns in a pattern match are matched against the input from top to bottom, and the first match decides which path on the right hand side will be taken.

We can use catch-all patterns to implement an equality test for Weekday (we will not yet use the == operator for this; this will have to wait until we learn about interfaces):

total
eqWeekday : Weekday -> Weekday -> Bool
eqWeekday Monday Monday        = True
eqWeekday Tuesday Tuesday      = True
eqWeekday Wednesday Wednesday  = True
eqWeekday Thursday Thursday    = True
eqWeekday Friday Friday        = True
eqWeekday Saturday Saturday    = True
eqWeekday Sunday Sunday        = True
eqWeekday _ _                  = False

Enumeration Types in the Prelude

Data types like Weekday consisting of a finite set of values are sometimes called enumerations. The Idris Prelude defines some common enumerations for us: for instance, Bool and Ordering. As with Weekday, we can use pattern matching when implementing functions on these types:

-- this is how `not` is implemented in the *Prelude*
total
negate : Bool -> Bool
negate False = True
negate True  = False

The Ordering data type describes an ordering relation between two values. For instance:

total
compareBool : Bool -> Bool -> Ordering
compareBool False False = EQ
compareBool False True  = LT
compareBool True True   = EQ
compareBool True False  = GT

Here, LT means that the first argument is less than the second, EQ means that the two arguments are equal and GT means, that the first argument is greater than the second.

Case Expressions

Sometimes we need to perform a computation with one of the arguments and want to pattern match on the result of this computation. We can use case expressions in this situation:

-- returns the larger of the two arguments
total
maxBits8 : Bits8 -> Bits8 -> Bits8
maxBits8 x y =
  case compare x y of
    LT => y
    _  => x

The first line of the case expression (case compare x y of) will invoke function compare with arguments x and y. On the following (indented) lines, we pattern match on the result of this computation. This is of type Ordering, so we expect one of the three constructors LT, EQ, or GT as the result. On the first line, we handle the LT case explicitly, while the other two cases are handled with an underscore as a catch-all pattern.

Note that indentation matters here: The case block as a whole must be indented (if it starts on a new line), and the different cases must also be indented by the same amount of whitespace.

Function compare is overloaded for many data types. We will learn how this works when we talk about interfaces.

If Then Else

When working with Bool, there is an alternative to pattern matching common to most programming languages:

total
maxBits8' : Bits8 -> Bits8 -> Bits8
maxBits8' x y = if compare x y == LT then y else x

Note that the if then else expression always returns a value and, therefore, the else branch cannot be dropped. This is different from the behavior in typical imperative languages, where if is a statement with possible side effects.

Naming Conventions: Identifiers

While we are free to use lower-case and upper-case identifiers for function names, type- and data constructors must be given upper-case identifiers in order not to confuse Idris (operators are also fine). For instance, the following data definition is not valid, and Idris will complain that it expected upper-case identifiers:

data foo = bar | baz

The same goes for similar data definitions like records and sum types (both will be explained below):

-- not valid Idris
record Foo where
  constructor mkfoo

On the other hand, we typically use lower-case identifiers for function names, unless we plan to use them mostly during type checking (more on this later). This is not enforced by Idris, however, so if you are working in a domain where upper-case identifiers are preferable, feel free to use those:

foo : Bits32 -> Bits32
foo = (* 2)

Bar : Bits32 -> Bits32
Bar = foo

Exercises part 1

module Tutorial.DataTypes.Exercises1

1. Use pattern matching to implement your own versions of boolean operators (&&) and (||) calling them and and or respectively.

   Note: One way to go about this is to enumerate all four possible combinations of two boolean values and give the result for each. However, there is a shorter, more clever way, requiring only two pattern matches for each of the two functions.

2. Define your own data type representing different units of time (seconds, minutes, hours, days, weeks), and implement the following functions for converting between time spans using different units. Hint: Use integer division (div) when going from seconds to some larger unit like hours).

   data UnitOfTime = Second -- add additional values
   
   -- calculate the number of seconds from a
   -- number of steps in the given unit of time
   total
   toSeconds : UnitOfTime -> Integer -> Integer
   
   -- Given a number of seconds, calculate the
   -- number of steps in the given unit of time
   total
   fromSeconds : UnitOfTime -> Integer -> Integer
   
   -- convert the number of steps in a given unit of time
   -- to the number of steps in another unit of time.
   -- use `fromSeconds` and `toSeconds` in your implementation
   total
   convert : UnitOfTime -> Integer -> UnitOfTime -> Integer
   

3. Define a data type for representing a subset of the chemical elements: Hydrogen (H), Carbon (C), Nitrogen (N), Oxygen (O), and Fluorine (F).

   Declare and implement function atomicMass, which for each element returns its atomic mass in dalton:

   Hydrogen : 1.008
   Carbon : 12.011
   Nitrogen : 14.007
   Oxygen : 15.999
   Fluorine : 18.9984
   

Sum Types

module Tutorial.DataTypes.SumTypes

Assume we'd like to write some web form, where users of our web application can decide how they like to be addressed. We give them a choice between two common predefined forms of address (Mr and Mrs), but also allow them to decide on a customized form. The possible choices can be encapsulated in an Idris data type:

public export
data Title = Mr | Mrs | Other String

This looks almost like an enumeration type, with the exception that there is a new thing, called a data constructor, which accepts a String argument (actually, the values in an enumeration are also called (nullary) data constructors). If we inspect the types at the REPL, we learn the following:

Tutorial.DataTypes> :t Mr
Tutorial.DataTypes.Mr : Title
Tutorial.DataTypes> :t Other
Tutorial.DataTypes.Other : String -> Title

So, Other is a function from String to Title. This means, that we can pass Other a String argument and get a Title as the result:

public export
total
dr : Title
dr = Other "Dr."

Again, a value of type Title can only consist of one of the three choices listed above, and again, we can use pattern matching to implement functions on the Title data type in a provably total way:

export
total
showTitle : Title -> String
showTitle Mr        = "Mr."
showTitle Mrs       = "Mrs."
showTitle (Other x) = x

Note, how in the last pattern match, the string value stored in the Other data constructor is bound to local variable x. Also, the Other x pattern has to be wrapped in parentheses, as otherwise Idris would think Other and x were to distinct function arguments.

This is a very common way to extract the values from data constructors. We can use showTitle to implement a function for creating a courteous greeting:

export
total
greet : Title -> String -> String
greet t name = "Hello, " ++ showTitle t ++ " " ++ name ++ "!"

In the implementation of greet, we use string literals and the string concatenation operator (++) to assemble the greeting from its parts.

At the REPL:

Tutorial.DataTypes> greet dr "Höck"
"Hello, Dr. Höck!"
Tutorial.DataTypes> greet Mrs "Smith"
"Hello, Mrs. Smith!"

Data types like Title are called sum types as they consist of the sum of their different parts: A value of type Title is either a Mr, a Mrs, or a String wrapped up in Other.

Here's another (drastically simplified) example of a sum type. Assume we allow two forms of authentication in our web application: Either by entering a username plus a password (for which we'll use an unsigned 64 bit integer here), or by providing username plus a (very complex) secret key. Here's a data type to encapsulate this use case:

data Credentials = Password String Bits64 | Key String String

As an example of a very primitive login function, we can hard-code some known credentials:

total
login : Credentials -> String
login (Password "Anderson" 6665443) = greet Mr "Anderson"
login (Key "Y" "xyz")               = greet (Other "Agent") "Y"
login _                             = "Access denied!"

As can be seen in the example above, we can also pattern match against primitive values by using integer and string literals. Give login a go at the REPL:

Tutorial.DataTypes> login (Password "Anderson" 6665443)
"Hello, Mr. Anderson!"
Tutorial.DataTypes> login (Key "Y" "xyz")
"Hello, Agent Y!"
Tutorial.DataTypes> login (Key "Y" "foo")
"Access denied!"

Exercises part 2

module Tutorial.DataTypes.Exercises2

1. Implement an equality test for Title (you can use the equality operator (==) for comparing two Strings):

   total
   eqTitle : Title -> Title -> Bool
   

2. For Title, implement a simple test to check, whether a custom title is being used:

   total
   isOther : Title -> Bool
   

3. Given our simple Credentials type, there are three ways for authentication to fail:

   • An unknown username was used.
   • The password given does not match the one associated with the username.
   • An invalid key was used.

   Encapsulate these three possibilities in a sum type called LoginError, but make sure not to disclose any confidential information: An invalid username should be stored in the corresponding error value, but an invalid password or key should not.

4. Implement function showError : LoginError -> String, which can be used to display an error message to the user who unsuccessfully tried to login into our web application.

Records

module Tutorial.DataTypes.Records

import Tutorial.DataTypes.Enumerations
import Tutorial.DataTypes.SumTypes

It is often useful to group together several values as a logical unit. For instance, in our web application we might want to group information about a user in a single data type. Such data types are often called product types (see below for an explanation). The most common and convenient way to define them is the record construct:

record User where
  constructor MkUser
  name  : String
  title : Title
  age   : Bits8

The declaration above creates a new type called User, and a new data constructor called MkUser. As usual, have a look at their types in the REPL:

Tutorial.DataTypes> :t User
Tutorial.DataTypes.User : Type
Tutorial.DataTypes> :t MkUser
Tutorial.DataTypes.MkUser : String -> Title -> Bits8 -> User

We can use MkUser (which is a function from String to Title to Bits8 to User) to create values of type User:

total
agentY : User
agentY = MkUser "Y" (Other "Agent") 51

total
drNo : User
drNo = MkUser "No" dr 73

We can also use pattern matching to extract the fields from a User value (they can again be bound to local variables):

total
greetUser : User -> String
greetUser (MkUser n t _) = greet t n

In the example above, the name and title field are bound to two new local variables (n and t respectively), which can then be used on the right hand side of greetUser's implementation. For the age field, which is not used on the right hand side, we can use an underscore as a catch-all pattern.

Note, how Idris will prevent us from making a common mistake: If we confuse the order of arguments, the implementation will no longer type check. We can verify this by putting the erroneous code in a failing block: This is an indented code block, which will lead to an error during elaboration (type checking). We can give part of the expected error message as an optional string argument to a failing block. If this does not match part of the error message (or the whole code block does not fail to type check) the failing block itself fails to type check. This is a useful tool to demonstrate that type safety works in two directions: We can show that valid code type checks but also that invalid code is rejected by the Idris elaborator:

failing "Mismatch between: String and Title"
  greetUser' : User -> String
  greetUser' (MkUser n t _) = greet n t

In addition, for every record field, Idris creates an extractor function of the same name. This can either be used as a regular function, or it can be used in postfix notation by appending it to a variable of the record type separated by a dot. Here are two examples for extracting the age from a user:

getAgeFunction : User -> Bits8
getAgeFunction u = age u

getAgePostfix : User -> Bits8
getAgePostfix u = u.age

Syntactic Sugar for Records

As was already mentioned in the introduction, Idris is a pure functional programming language. In pure functions, we are not allowed to modify global mutable state. As such, if we want to modify a record value, we will always create a new value with the original value remaining unchanged: Records and other Idris values are immutable. While this can have a slight impact on performance, it has the benefit that we can freely pass a record value to different functions, without fear of the functions modifying the value by in-place mutation. These are, again, very strong guarantees, which makes it drastically easier to reason about our code.

There are several ways to modify a record, the most general being to pattern match on the record and adjust each field as desired. If, for instance, we'd like to increase the age of a User by one, we could do the following:

total
incAge : User -> User
incAge (MkUser name title age) = MkUser name title (age + 1)

That's a lot of code for such a simple thing, so Idris offers several syntactic conveniences for this. For instance, using record syntax, we can just access and update the age field of a value:

total
incAge2 : User -> User
incAge2 u = { age := u.age + 1 } u

Assignment operator := assigns a new value to the age field in u. Remember, that this will create a new User value. The original value u remains unaffected by this.

We can access a record field, either by using the field name as a projection function (age u; also have a look at :t age in the REPL), or by using dot syntax: u.age. This is special syntax and not related to the dot operator for function composition ((.)).

The use case of modifying a record field is so common that Idris provides special syntax for this as well:

total
incAge3 : User -> User
incAge3 u = { age $= (+ 1) } u

Here, I used an operator section ((+ 1)) to make the code more concise. As an alternative to an operator section, we could have used an anonymous function like so:

total
incAge4 : User -> User
incAge4 u = { age $= \x => x + 1 } u

Finally, since our function's argument u is only used once at the very end, we can drop it altogether, to get the following, highly concise version:

total
incAge5 : User -> User
incAge5 = { age $= (+ 1) }

As usual, we should have a look at the result at the REPL:

Tutorial.DataTypes> incAge5 drNo
MkUser "No" (Other "Dr.") 74

It is possible to use this syntax to set and/or update several record fields at once:

total
drNoJunior : User
drNoJunior = { name $= (++ " Jr."), title := Mr, age := 17 } drNo

Tuples

I wrote above that a record is also called a product type. This is quite obvious when we consider the number of possible values inhabiting a given type. For instance, consider the following custom record:

record Foo where
  constructor MkFoo
  wd   : Weekday
  bool : Bool

How many possible values of type Foo are there? The answer is 7 * 2 = 14, as we can pair every possible Weekday (seven in total) with every possible Bool (two in total). So, the number of possible values of a record type is the product of the number of possible values for each field.

The canonical product type is the Pair, which is available from the Prelude:

total
weekdayAndBool : Weekday -> Bool -> Pair Weekday Bool
weekdayAndBool wd b = MkPair wd b

Since it is quite common to return several values from a function wrapped in a Pair or larger tuple, Idris provides some syntactic sugar for working with these. Instead of Pair Weekday Bool, we can just write (Weekday, Bool). Likewise, instead of MkPair wd b, we can just write (wd, b) (the space is optional):

total
weekdayAndBool2 : Weekday -> Bool -> (Weekday, Bool)
weekdayAndBool2 wd b = (wd, b)

This works also for nested tuples:

total
triple : Pair Bool (Pair Weekday String)
triple = MkPair False (Friday, "foo")

total
triple2 : (Bool, Weekday, String)
triple2 = (False, Friday, "foo")

In the example above, triple2 is converted to the form used in triple by the Idris compiler.

We can even use tuple syntax in pattern matches:

total
bar : Bool
bar = case triple of
  (b,wd,_) => b && isWeekend wd

As Patterns

Sometimes, we'd like to take apart a value by pattern matching on it but still retain the value as a whole for using it in further computations:

total
baz : (Bool,Weekday,String) -> (Nat,Bool,Weekday,String)
baz t@(_,_,s) = (length s, t)

In baz, variable t is bound to the triple as a whole, which is then reused to construct the resulting quadruple. Remember, that (Nat,Bool,Weekday,String) is just sugar for Pair Nat (Bool,Weekday,String), and (length s, t) is just sugar for MkPair (length s) t. Hence, the implementation above is correct as is confirmed by the type checker.

Exercises part 3

1. Define a record type for time spans by pairing a UnitOfTime with an integer representing the duration of the time span in the given unit of time. Define also a function for converting a time span to an Integer representing the duration in seconds.

2. Implement an equality check for time spans: Two time spans should be considered equal, if and only if they correspond to the same number of seconds.

3. Implement a function for pretty printing time spans: The resulting string should display the time span in its given unit, plus show the number of seconds in parentheses, if the unit is not already seconds.

4. Implement a function for adding two time spans. If the two time spans use different units of time, use the smaller unit of time to ensure a lossless conversion.

Generic Data Types

module Tutorial.DataTypes.GenericDataTypes

import Tutorial.DataTypes.Enumerations

Sometimes, a concept is general enough that we'd like to apply it not only to a single type, but to all kinds of types. For instance, we might not want to define data types for lists of integers, lists of strings, and lists of booleans, as this would lead to a lot of code duplication. Instead, we'd like to have a single generic list type parameterized by the type of values it stores. This section explains how to define and use generic types.

Maybe

Consider the case of parsing a Weekday from user input. Surely, such a function should return Saturday, if the string input was "Saturday", but what if the input was "sdfkl332"? We have several options here. For instance, we could just return a default result (Sunday perhaps?). But is this the behavior programmers expect when using our library? Maybe not. To silently continue with a default value in the face of invalid user input is hardly ever the best choice and may lead to a lot of confusion.

In an imperative language, our function would probably throw an exception. We could do this in Idris as well (there is function idris_crash in the Prelude for this), but doing so, we would abandon totality! A high price to pay for such a common thing as a parsing error.

In languages like Java, our function might also return some kind of null value (leading to the dreaded NullPointerExceptions if not handled properly in client code). Our solution will be similar, but instead of silently returning null, we will make the possibility of failure visible in the types! We define a custom data type, which encapsulates the possibility of failure. Defining new data types in Idris is very cheap (in terms of the amount of code needed), therefore this is often the way to go in order to increase type safety. Here's an example how to do this:

data MaybeWeekday = WD Weekday | NoWeekday

total
readWeekday : String -> MaybeWeekday
readWeekday "Monday"    = WD Monday
readWeekday "Tuesday"   = WD Tuesday
readWeekday "Wednesday" = WD Wednesday
readWeekday "Thursday"  = WD Thursday
readWeekday "Friday"    = WD Friday
readWeekday "Saturday"  = WD Saturday
readWeekday "Sunday"    = WD Sunday
readWeekday _           = NoWeekday

But assume now, we'd also like to read Bool values from user input. We'd now have to write a custom data type MaybeBool and so on for all types we'd like to read from String, and the conversion of which might fail.

Idris, like many other programming languages, allows us to generalize this behavior by using generic data types. Here's an example:

data Option a = Some a | None

total
readBool : String -> Option Bool
readBool "True"    = Some True
readBool "False"   = Some False
readBool _         = None

It is important to go to the REPL and look at the types:

Tutorial.DataTypes> :t Some
Tutorial.DataTypes.Some : a -> Option a
Tutorial.DataTypes> :t None
Tutorial.DataTypes.None : Option a
Tutorial.DataTypes> :t Option
Tutorial.DataTypes.Option : Type -> Type

We need to introduce some jargon here. Option is what we call a type constructor. It is not yet a saturated type: It is a function from Type to Type. However, Option Bool is a type, as is Option Weekday. Even Option (Option Bool) is a valid type. Option is a type constructor parameterized over a parameter of type Type. Some and None are Options data constructors: The functions used to create values of type Option a for a type a.

Let's see some other use cases for Option. Below is a safe division operation:

total
safeDiv : Integer -> Integer -> Option Integer
safeDiv n 0 = None
safeDiv n k = Some (n `div` k)

The possibility of returning some kind of null value in the face of invalid input is so common, that there is a data type like Option already in the Prelude: Maybe, with data constructors Just and Nothing.

It is important to understand the difference between returning Maybe Integer in a function, which might fail, and returning null in languages like Java: In the former case, the possibility of failure is visible in the types. The type checker will force us to treat Maybe Integer differently than Integer: Idris will not allow us to forget to eventually handle the failure case. Not so, if null is silently returned without adjusting the types. Programmers may (and often will) forget to handle the null case, leading to unexpected and sometimes hard to debug runtime exceptions.

Either

While Maybe is very useful to quickly provide a default value to signal some kind of failure, this value (Nothing) is not very informative. It will not tell us what exactly went wrong. For instance, in case of our Weekday reading function, it might be interesting later on to know the value of the invalid input string. And just like with Maybe and Option above, this concept is general enough that we might encounter other types of invalid values. Here's a data type to encapsulate this:

data Validated e a = Invalid e | Valid a

Validated is a type constructor parameterized over two type parameters e and a. It's data constructors are Invalid and Valid, the former holding a value describing some error condition, the latter the result in case of a successful computation. Let's see this in action:

total
readWeekdayV : String -> Validated String Weekday
readWeekdayV "Monday"    = Valid Monday
readWeekdayV "Tuesday"   = Valid Tuesday
readWeekdayV "Wednesday" = Valid Wednesday
readWeekdayV "Thursday"  = Valid Thursday
readWeekdayV "Friday"    = Valid Friday
readWeekdayV "Saturday"  = Valid Saturday
readWeekdayV "Sunday"    = Valid Sunday
readWeekdayV s           = Invalid ("Not a weekday: " ++ s)

Again, this is such a general concept that a data type similar to Validated is already available from the Prelude: Either with data constructors Left and Right. It is very common for functions to encapsulate the possibility of failure by returning an Either err val, where err is the error type and val is the desired return type. This is the type safe (and total!) alternative to throwing a catchable exception in an imperative language.

Note, however, that the semantics of Either are not always "Left is an error and Right a success". A function returning an Either just means that it can have to different types of results, each of which are tagged with the corresponding data constructor.

List

One of the most important data structures in pure functional programming is the singly linked list. Here is its definition (called Seq in order for it not to collide with List, which is of course already available from the Prelude):

data Seq a = Nil | (::) a (Seq a)

This calls for some explanations. Seq consists of two data constructors: Nil (representing an empty sequence of values) and (::) (also called the cons operator), which prepends a new value of type a to an already existing list of values of the same type. As you can see, we can also use operators as data constructors, but please do not overuse this. Use clear names for your functions and data constructors and only introduce new operators when it truly helps readability!

Here is an example of how to use the List constructors (I use List here, as this is what you should use in your own code):

total
ints : List Int64
ints = 1 :: 2 :: -3 :: Nil

However, there is a more concise way of writing the above. Idris accepts special syntax for constructing data types consisting exactly of the two constructors Nil and (::):

total
ints2 : List Int64
ints2 = [1, 2, -3]

total
ints3 : List Int64
ints3 = []

The two definitions ints and ints2 are treated identically by the compiler. Note, that list syntax can also be used in pattern matches.

There is another thing that's special about Seq and List: Each of them is defined in terms of itself (the cons operator accepts a value and another Seq as arguments). We call such data types recursive data types, and their recursive nature means, that in order to decompose or consume them, we typically require recursive functions. In an imperative language, we might use a for loop or similar construct to iterate over the values of a List or a Seq, but these things do not exist in a language without in-place mutation. Here's how to sum a list of integers:

total
intSum : List Integer -> Integer
intSum Nil       = 0
intSum (n :: ns) = n + intSum ns

Recursive functions can be hard to grasp at first, so I'll break this down a bit. If we invoke intSum with the empty list, the first pattern matches and the function returns zero immediately. If, however, we invoke intSum with a non-empty list - [7,5,9] for instance - the following happens:

1. The second pattern matches and splits the list into two parts: Its head (7) is bound to variable n and its tail ([5,9]) is bound to ns:

   7 + intSum [5,9]
   

2. In a second invocation, intSum is called with a new list: [5,9]. The second pattern matches and n is bound to 5 and ns is bound to [9]:

   7 + (5 + intSum [9])
   

3. In a third invocation intSum is called with list [9]. The second pattern matches and n is bound to 9 and ns is bound to []:

   7 + (5 + (9 + intSum [])
   

4. In a fourth invocation, intSum is called with list [] and returns 0 immediately:

   7 + (5 + (9 + 0)
   

5. In the third invocation, 9 and 0 are added and 9 is returned:

   7 + (5 + 9)
   

6. In the second invocation, 5 and 9 are added and 14 is returned:

   7 + 14
   

7. Finally, our initial invocation of intSum adds 7 and 14 and returns 21.

Thus, the recursive implementation of intSum leads to a sequence of nested calls to intSum, which terminates once the argument is the empty list.

Generic Functions

In order to fully appreciate the versatility that comes with generic data types, we also need to talk about generic functions. Like generic types, these are parameterized over one or more type parameters.

Consider for instance the case of breaking out of the Option data type. In case of a Some, we'd like to return the stored value, while for the None case we provide a default value. Here's how to do this, specialized to Integers:

total
integerFromOption : Integer -> Option Integer -> Integer
integerFromOption _ (Some y) = y
integerFromOption x None     = x

It's pretty obvious that this, again, is not general enough. Surely, we'd also like to break out of Option Bool or Option String in a similar fashion. That's exactly what the generic function fromOption does:

total
fromOption : a -> Option a -> a
fromOption _ (Some y) = y
fromOption x None     = x

The lower-case a is again a type parameter. You can read the type signature as follows: "For any type a, given a value of type a, and an Option a, we can return a value of type a." Note, that fromOption knows nothing else about a, other than it being a type. It is therefore not possible, to conjure a value of type a out of thin air. We must have a value available to deal with the None case.

The pendant to fromOption for Maybe is called fromMaybe and is available from module Data.Maybe from the base library.

Sometimes, fromOption is not general enough. Assume we'd like to print the value of a freshly parsed Bool, giving some generic error message in case of a None. We can't use fromOption for this, as we have an Option Bool and we'd like to return a String. Here's how to do this:

total
option : b -> (a -> b) -> Option a -> b
option _ f (Some y) = f y
option x _ None     = x

total
handleBool : Option Bool -> String
handleBool = option "Not a boolean value." show

Function option is parameterized over two type parameters: a represents the type of values stored in the Option, while b is the return type. In case of a Just, we need a way to convert the stored a to a b, an that's done using the function argument of type a -> b.

In Idris, lower-case identifiers in function types are treated as type parameters, while upper-case identifiers are treated as types or type constructors that must be in scope.

Exercises part 4

If this is your first time programming in a purely functional language, the exercises below are very important. Do not skip any of them! Take your time and work through them all. In most cases, the types should be enough to explain what's going on, even though they might appear cryptic in the beginning. Otherwise, have a look at the comments (if any) of each exercise.

Remember, that lower-case identifiers in a function signature are treated as type parameters.

1. Implement the following generic functions for Maybe:

   -- make sure to map a `Just` to a `Just`.
   total
   mapMaybe : (a -> b) -> Maybe a -> Maybe b
   
   -- Example: `appMaybe (Just (+2)) (Just 20) = Just 22`
   total
   appMaybe : Maybe (a -> b) -> Maybe a -> Maybe b
   
   -- Example: `bindMaybe (Just 12) Just = Just 12`
   total
   bindMaybe : Maybe a -> (a -> Maybe b) -> Maybe b
   
   -- keep the value in a `Just` only if the given predicate holds
   total
   filterMaybe : (a -> Bool) -> Maybe a -> Maybe a
   
   -- keep the first value that is not a `Nothing` (if any)
   total
   first : Maybe a -> Maybe a -> Maybe a
   
   -- keep the last value that is not a `Nothing` (if any)
   total
   last : Maybe a -> Maybe a -> Maybe a
   
   -- this is another general way to extract a value from a `Maybe`.
   -- Make sure the following holds:
   -- `foldMaybe (+) 5 Nothing = 5`
   -- `foldMaybe (+) 5 (Just 12) = 17`
   total
   foldMaybe : (acc -> el -> acc) -> acc -> Maybe el -> acc
   

2. Implement the following generic functions for Either:

   total
   mapEither : (a -> b) -> Either e a -> Either e b
   
   -- In case of both `Either`s being `Left`s, keep the
   -- value stored in the first `Left`.
   total
   appEither : Either e (a -> b) -> Either e a -> Either e b
   
   total
   bindEither : Either e a -> (a -> Either e b) -> Either e b
   
   -- Keep the first value that is not a `Left`
   -- If both `Either`s are `Left`s, use the given accumulator
   -- for the error values
   total
   firstEither : (e -> e -> e) -> Either e a -> Either e a -> Either e a
   
   -- Keep the last value that is not a `Left`
   -- If both `Either`s are `Left`s, use the given accumulator
   -- for the error values
   total
   lastEither : (e -> e -> e) -> Either e a -> Either e a -> Either e a
   
   total
   fromEither : (e -> c) -> (a -> c) -> Either e a -> c
   

3. Implement the following generic functions for List:

   total
   mapList : (a -> b) -> List a -> List b
   
   total
   filterList : (a -> Bool) -> List a -> List a
   
   -- re-implement list concatenation (++) such that e.g. (++) [1, 2] [3, 4] = [1, 2, 3, 4]
   -- note that because this function conflicts with the standard
   -- Prelude.List.(++), if you use it then you will need to prefix it with
   -- the name of your module, like DataTypes.(++) or Ch3.(++). alternatively
   -- you could simply call the function something unique like myListConcat or concat'
   total
   (++) : List a -> List a -> List a
   
   -- return the first value of a list, if it is non-empty
   total
   headMaybe : List a -> Maybe a
   
   -- return everything but the first value of a list, if it is non-empty
   total
   tailMaybe : List a -> Maybe (List a)
   
   -- return the last value of a list, if it is non-empty
   total
   lastMaybe : List a -> Maybe a
   
   -- return everything but the last value of a list,
   -- if it is non-empty
   total
   initMaybe : List a -> Maybe (List a)
   
   -- accumulate the values in a list using the given
   -- accumulator function and initial value
   --
   -- Examples:
   -- `foldList (+) 10 [1,2,7] = 20`
   -- `foldList String.(++) "" ["Hello","World"] = "HelloWorld"`
   -- `foldList last Nothing (mapList Just [1,2,3]) = Just 3`
   total
   foldList : (acc -> el -> acc) -> acc -> List el -> acc
   

4. Assume we store user data for our web application in the following record:

   record Client where
     constructor MkClient
     name          : String
     title         : Title
     age           : Bits8
     passwordOrKey : Either Bits64 String
   

   Using LoginError from an earlier exercise, implement function login, which, given a list of Clients plus a value of type Credentials will return either a LoginError in case no valid credentials where provided, or the first Client for whom the credentials match.

5. Using your data type for chemical elements from an earlier exercise, implement a function for calculating the molar mass of a molecular formula.

   Use a list of elements each paired with its count (a natural number) for representing formulae. For instance:

   ethanol : List (Element,Nat)
   ethanol = [(C,2),(H,6),(O,1)]
   

   Hint: You can use function cast to convert a natural number to a Double.

Alternative Syntax for Data Definitions

module Tutorial.DataTypes.AltSyntax

While the examples in the section about parameterized data types are short and concise, there is a slightly more verbose but much more general form for writing such definitions, which makes it much clearer what's going on. In my opinion, this more general form should be preferred in all but the most simple data definitions.

Here are the definitions of Option, Validated, and Seq again, using this more general form (I put them in their own namespace, so Idris will not complain about identical names in the same source file):

-- GADT is an acronym for "generalized algebraic data type"
namespace GADT
  data Option : Type -> Type where
    Some : a -> Option a
    None : Option a

  data Validated : Type -> Type -> Type where
    Invalid : e -> Validated e a
    Valid   : a -> Validated e a

  data Seq : Type -> Type where
    Nil  : Seq a
    (::) : a -> GADT.Seq a -> Seq a

Here, Option is clearly declared as a type constructor (a function of type Type -> Type), while Some is a generic function of type a -> Option a (where a is a type parameter) and None is a nullary generic function of type Option a (a again being a type parameter). Likewise for Validated and Seq. Note, that in case of Seq we had to disambiguate between the different Seq definitions in the recursive case. Since we will usually not define several data types with the same name in a source file, this is not necessary most of the time.

Conclusion

We covered a lot of ground in this chapter, so I'll summarize the most important points below:

• Enumerations are data types consisting of a finite number of possible values.

• Sum types are data types with more than one data constructor, where each constructor describes a choice that can be made.

• Product types are data types with a single constructor used to group several values of possibly different types.

• We use pattern matching to deconstruct immutable values in Idris. The possible patterns correspond to a data type's data constructors.

• We can bind variables to values in a pattern or use an underscore as a placeholder for a value that's not needed on the right hand side of an implementation.

• We can pattern match on an intermediary result by introducing a case block.

• The preferred way to define new product types is to define them as records, since these come with additional syntactic conveniences for setting and modifying individual record fields.

• Generic types and functions allow us generalize certain concepts and make them available for many types by using type parameters instead of concrete types in function and type signatures.

• Common concepts like nullary values (Maybe), computations that might fail with some error condition (Either), and handling collections of values of the same type at once (List) are example use cases of generic types and functions already provided by the Prelude.

What's next

In the next section, we will introduce interfaces, another approach to function overloading.

Interfaces

Function overloading - the definition of functions with the same name but different implementations - is a concept found in many programming languages. Idris natively supports overloading of functions: Two functions with the same name can be defined in different modules or namespaces, and Idris will try to disambiguate between these based on the types involved. Here is an example:

module Tutorial.Interfaces

%default total

namespace Bool
  export
  size : Bool -> Integer
  size True  = 1
  size False = 0

namespace Integer
  export
  size : Integer -> Integer
  size = id

namespace List
  export
  size : List a -> Integer
  size = cast . length

Here, we defined three different functions called size, each in its own namespace. We can disambiguate between these by prefixing them with their namespace:

Tutorial.Interfaces> :t Bool.size
Tutorial.Interfaces.Bool.size : Bool -> Integer

However, this is usually not necessary:

mean : List Integer -> Integer
mean xs = sum xs `div` size xs

As you can see, Idris can disambiguate between the different size functions, since xs is of type List Integer, which unifies only with List a, the argument type of List.size.

Interface Basics

module Tutorial.Interfaces.Basics

While function overloading as described above works well, there are use cases, where this form of overloaded functions leads to a lot of code duplication.

As an example, consider a function cmp (short for compare, which is already exported by the Prelude), for describing an ordering for the values of type String:

cmp : String -> String -> Ordering

We'd also like to have similar functions for many other data types. Function overloading allows us to do just that, but cmp is not an isolated piece of functionality. From it, we can derive functions like greaterThan', lessThan', minimum', maximum', and many others:

lessThan' : String -> String -> Bool
lessThan' s1 s2 = LT == cmp s1 s2

greaterThan' : String -> String -> Bool
greaterThan' s1 s2 = GT == cmp s1 s2

minimum' : String -> String -> String
minimum' s1 s2 =
  case cmp s1 s2 of
    LT => s1
    _  => s2

maximum' : String -> String -> String
maximum' s1 s2 =
  case cmp s1 s2 of
    GT => s1
    _  => s2

We'd need to implement all of these again for the other types with a cmp function, and most if not all of these implementations would be identical to the ones written above. That's a lot of code repetition.

One way to solve this is to use higher-order functions. For instance, we could define function minimumBy, which takes a comparison function as its first argument and returns the smaller of the two remaining arguments:

minimumBy : (a -> a -> Ordering) -> a -> a -> a
minimumBy f a1 a2 =
  case f a1 a2 of
    LT => a1
    _  => a2

This solution is another proof of how higher-order functions allow us to reduce code duplication. However, the need to explicitly pass around the comparison function all the time can get tedious as well. It would be nice, if we could teach Idris to come up with such a function on its own.

Interfaces solve exactly this issue. Here's an example:

public export
interface Comp a where
  comp : a -> a -> Ordering

export
implementation Comp Bits8 where
  comp = compare

export
implementation Comp Bits16 where
  comp = compare

The code above defines interface Comp providing function comp for calculating the ordering for two values of a type a, followed by two implementations of this interface for types Bits8 and Bits16. Note, that the implementation keyword is optional.

The comp implementations for Bits8 and Bits16 both use function compare, which is part of a similar interface from the Prelude called Ord.

The next step is to look at the type of comp at the REPL:

Tutorial.Interfaces> :t comp
Tutorial.Interfaces.comp : Comp a => a -> a -> Ordering

The interesting part in the type signature of comp is the initial Comp a => argument. Here, Comp is a constraint on type parameter a. This signature can be read as: "For any type a, given an implementation of interface Comp for a, we can compare two values of type a and return an Ordering for these." Whenever we invoke comp, we expect Idris to come up with a value of type Comp a on its own, hence the new => arrow. If Idris fails to do so, it will answer with a type error.

We can now use comp in the implementations of related functions. All we have to do is to also prefix these derived functions with a Comp constraint:

lessThan : Comp a => a -> a -> Bool
lessThan s1 s2 = LT == comp s1 s2

greaterThan : Comp a => a -> a -> Bool
greaterThan s1 s2 = GT == comp s1 s2

minimum : Comp a => a -> a -> a
minimum s1 s2 =
  case comp s1 s2 of
    LT => s1
    _  => s2

maximum : Comp a => a -> a -> a
maximum s1 s2 =
  case comp s1 s2 of
    GT => s1
    _  => s2

Note, how the definition of minimum is almost identical to minimumBy. The only difference being that in case of minimumBy we had to pass the comparison function as an explicit argument, while for minimum it is provided as part of the Comp implementation, which is passed around by Idris for us.

Thus, we have defined all these utility functions once and for all for every type with an implementation of interface Comp.

Exercises Part 1

1. Implement function anyLarger, which should return True, if and only if a list of values contains at least one element larger than a given reference value. Use interface Comp in your implementation.

2. Implement function allLarger, which should return True, if and only if a list of values contains only elements larger than a given reference value. Note, that this is trivially true for the empty list. Use interface Comp in your implementation.

3. Implement function maxElem, which tries to extract the largest element from a list of values with a Comp implementation. Likewise for minElem, which tries to extract the smallest element. Note, that the possibility of the list being empty must be considered when deciding on the output type.

4. Define an interface Concat for values like lists or strings, which can be concatenated. Provide implementations for lists and strings.

5. Implement function concatList for concatenating the values in a list holding values with a Concat implementation. Make sure to reflect the possibility of the list being empty in your output type.

More About Interfaces

module Tutorial.Interfaces.More

import Tutorial.Interfaces.Basics

In the last section, we learned about the very basics of interfaces: Why they are useful and how to define and implement them. In this section, we will learn about some slightly advanced concepts: Extending interfaces, interfaces with constraints, and default implementations.

Extending Interfaces

Some interfaces form a kind of hierarchy. For instance, for the Concat interface used in exercise 4, there might be a child interface called Empty, for those types, which have a neutral element with relation to concatenation. In such a case, we make an implementation of Concat a prerequisite for implementing Empty:

interface Concat a where
  concat : a -> a -> a

implementation Concat String where
  concat = (++)

interface Concat a => Empty a where
  empty : a

implementation Empty String where
  empty = ""

Concat a => Empty a should be read as: "An implementation of Concat for type a is a prerequisite for there being an implementation of Empty for a." But this also means that, whenever we have an implementation of interface Empty, we must also have an implementation of Concat and can invoke the corresponding functions:

concatListE : Empty a => List a -> a
concatListE []        = empty
concatListE (x :: xs) = concat x (concatListE xs)

Note, how in the type of concatListE we only used an Empty constraint, and how in the implementation we were still able to invoke both empty and concat.

Constrained Implementations

Sometimes, it is only possible to implement an interface for a generic type, if its type parameters implement this interface as well. For instance, implementing interface Comp for Maybe a makes sense only if type a itself implements Comp. We can constrain interface implementations with the same syntax we use for constrained functions:

implementation Comp a => Comp (Maybe a) where
  comp Nothing  Nothing  = EQ
  comp (Just _) Nothing  = GT
  comp Nothing  (Just _) = LT
  comp (Just x) (Just y) = comp x y

This is not the same as extending an interface, although the syntax looks very similar. Here, the constraint lies on a type parameter instead of the full type. The last line in the implementation of Comp (Maybe a) compares the values stored in the two Justs. This is only possible, if there is a Comp implementation for these values as well. Go ahead, and remove the Comp a constraint from the above implementation. Learning to read and understand Idris' type errors is important for fixing them.

The good thing is, that Idris will solve all these constraints for us:

maxTest : Maybe Bits8 -> Ordering
maxTest = comp (Just 12)

Here, Idris tries to find an implementation for Comp (Maybe Bits8). In order to do so, it needs an implementation for Comp Bits8. Go ahead, and replace Bits8 in the type of maxTest with Bits64, and have a look at the error message Idris produces.

Default Implementations

Sometimes, we'd like to pack several related functions in an interface to allow programmers to implement each in the most efficient way, although they could be implemented in terms of each other. For instance, consider an interface Equals for comparing two values for equality, with functions eq returning True if two values are equal and neq returning True if they are not. Surely, we can implement neq in terms of eq, so most of the time when implementing Equals, we will only implement the latter. In this case, we can give an implementation for neq already in the definition of Equals:

interface Equals a where
  eq : a -> a -> Bool

  neq : a -> a -> Bool
  neq a1 a2 = not (eq a1 a2)

If in an implementation of Equals we only implement eq, Idris will use the default implementation for neq as shown above:

Equals String where
  eq = (==)

If on the other hand we'd like to provide explicit implementations for both functions, we can do so as well:

Equals Bool where
  eq True True   = True
  eq False False = True
  eq _ _         = False

  neq True  False = True
  neq False True  = True
  neq _ _         = False

Exercises part 2

1. Implement interfaces Equals, Comp, Concat, and Empty for pairs, constraining your implementations as necessary. (Note, that multiple constraints can be given sequentially like other function arguments: Comp a => Comp b => Comp (a,b).)

2. Below is an implementation of a binary tree. Implement interfaces Equals and Concat for this type.

   data Tree : Type -> Type where
     Leaf : a -> Tree a
     Node : Tree a -> Tree a -> Tree a
   

Interfaces in the Prelude

module Tutorial.Interfaces.Prelude

The Idris Prelude provides several interfaces plus implementations that are useful in almost every non-trivial program. I'll introduce the basic ones here. The more advanced ones will be discussed in later chapters.

Most of these interfaces come with associated mathematical laws, and implementations are assumed to adhere to these laws. These laws will be given here as well.

Eq

Probably the most often used interface, Eq corresponds to interface Equals we used above as an example. Instead of eq and neq, Eq provides two operators (==) and (/=) for comparing two values of the same type for being equal or not. Most of the data types defined in the Prelude come with an implementation of Eq, and whenever programmers define their own data types, Eq is typically one of the first interfaces they implement.

Eq Laws

We expect the following laws to hold for all implementations of Eq:

• (==) is reflexive: x == x = True for all x. This means, that every value is equal to itself.

• (==) is symmetric: x == y = y == x for all x and y. This means, that the order of arguments passed to (==) does not matter.

• (==) is transitive: From x == y = True and y == z = True follows x == z = True.

• (/=) is the negation of (==): x == y = not (x /= y) for all x and y.

In theory, Idris has the power to verify these laws at compile time for many non-primitive types. However, out of pragmatism this is not required when implementing Eq, since writing such proofs can be quite involved.

Ord

The pendant to Comp in the Prelude is interface Ord. In addition to compare, which is identical to our own comp it provides comparison operators (>=), (>), (<=), and (<), as well as utility functions max and min. Unlike Comp, Ord extends Eq, so whenever there is an Ord constraint, we also have access to operators (==) and (/=) and related functions.

Ord Laws

We expect the following laws to hold for all implementations of Ord:

• (<=) is reflexive and transitive.
• (<=) is antisymmetric: From x <= y = True and y <= x = True follows x == y = True.
• x <= y = y >= x.
• x < y = not (y <= x)
• x > y = not (y >= x)
• compare x y = EQ => x == y = True
• compare x y == GT = x > y
• compare x y == LT = x < y

Semigroup and Monoid

Semigroup is the pendant to our example interface Concat, with operator (<+>) (also called append) corresponding to function concat.

Likewise, Monoid corresponds to Empty, with neutral corresponding to empty.

These are incredibly important interfaces, which can be used to combine two or more values of a data type into a single value of the same type. Examples include but are not limited to addition or multiplication of numeric types, concatenation of sequences of data, or sequencing of computations.

As an example, consider a data type for representing distances in a geometric application. We could just use Double for this, but that's not very type safe. It would be better to use a single field record wrapping values type Double, to give such values clear semantics:

record Distance where
  constructor MkDistance
  meters : Double

There is a natural way for combining two distances: We sum up the values they hold. This immediately leads to an implementation of Semigroup:

Semigroup Distance where
  x <+> y = MkDistance $ x.meters + y.meters

It is also immediately clear, that zero is the neutral element of this operation: Adding zero to any value does not affect the value at all. This allows us to implement Monoid as well:

Monoid Distance where
  neutral = MkDistance 0

Semigroup and Monoid Laws

We expect the following laws to hold for all implementations of Semigroup and Monoid:

• (<+>) is associative: x <+> (y <+> z) = (x <+> y) <+> z, for all values x, y, and z.
• neutral is the neutral element with relation to (<+>): neutral <+> x = x <+> neutral = x, for all x.

Show

The Show interface is mainly used for debugging purposes, and is supposed to display values of a given type as a string, typically closely resembling the Idris code used to create the value. This includes the proper wrapping of arguments in parentheses where necessary. For instance, experiment with the output of the following function at the REPL:

showExample : Maybe (Either String (List (Maybe Integer))) -> String
showExample = show

And at the REPL:

Tutorial.Interfaces> showExample (Just (Right [Just 12, Nothing]))
"Just (Right [Just 12, Nothing])"

We will learn how to implement instances of Show in an exercise.

Overloaded Literals

Literal values in Idris, such as integer literals (12001), string literals ("foo bar"), floating point literals (12.112), and character literals ('$') can be overloaded. This means, that we can create values of types other than String from just a string literal. The exact workings of this has to wait for another section, but for many common cases, it is sufficient for a value to implement interfaces FromString (for using string literals), FromChar (for using character literals), or FromDouble (for using floating point literals). The case of integer literals is special, and will be discussed in the next section.

Here is an example of using FromString. Assume, we write an application where users can identify themselves with a username and password. Both consist of strings of characters, so it is pretty easy to confuse and mix up the two things, although they clearly have very different semantics. In these cases, it is advisable to come up with new types for the two, especially since getting these things wrong is a security concern.

Here are three example record types to do this:

record UserName where
  constructor MkUserName
  name : String

record Password where
  constructor MkPassword
  value : String

record User where
  constructor MkUser
  name     : UserName
  password : Password

In order to create a value of type User, even for testing, we'd have to wrap all strings using the given constructors:

hock : User
hock = MkUser (MkUserName "hock") (MkPassword "not telling")

This is rather cumbersome, and some people might think this to be too high a price to pay just for an increase in type safety (I'd tend to disagree). Luckily, we can get the convenience of string literals back very easily:

FromString UserName where
  fromString = MkUserName

FromString Password where
  fromString = MkPassword

hock2 : User
hock2 = MkUser "hock" "not telling"

Numeric Interfaces

The Prelude also exports several interfaces providing the usual arithmetic operations. Below is a comprehensive list of the interfaces and the functions each provides:

• Num

  • (+) : Addition
  • (*) : Multiplication
  • fromInteger : Overloaded integer literals

• Neg

  • negate : Negation
  • (-) : Subtraction

• Integral

  • div : Integer division
  • mod : Modulo operation

• Fractional

  • (/) : Division
  • recip : Calculates the reciprocal of a value

As you can see: We need to implement interface Num to use integer literals for a given type. In order to use negative integer literals like -12, we also have to implement interface Neg.

Cast

The last interface we will quickly discuss in this section is Cast. It is used to convert values of one type to values of another via function cast. Cast is special, since it is parameterized over two type parameters unlike the other interfaces we looked at so far, with only one type parameter.

So far, Cast is mainly used for interconversion between primitive types in the standard libraries, especially numeric types. When you look at the implementations exported from the Prelude (for instance, by invoking :doc Cast at the REPL), you'll see that there are dozens of implementations for most pairings of primitive types.

Although Cast would also be useful for other conversions (for going from Maybe to List or for going from Either e to Maybe, for instance), the Prelude and base seem not to introduce these consistently. For instance, there are Cast implementations from going from SnocList to List and vice versa, but not for going from Vect n to List, or for going from List1 to List, although these would be just as feasible.

Exercises part 3

These exercises are meant to make you comfortable with implementing interfaces for your own data types, as you will have to do so regularly when writing Idris code.

While it is immediately clear why interfaces like Eq, Ord, or Num are useful, the usability of Semigroup and Monoid may be harder to appreciate at first. Therefore, there are several exercises where you'll implement different instances for these.

1. Define a record type Complex for complex numbers, by pairing two values of type Double. Implement interfaces Eq, Num, Neg, and Fractional for Complex.

2. Implement interface Show for Complex. Have a look at data type Prec and function showPrec and how these are used in the Prelude to implement instances for Either and Maybe.

   Verify the correct behavior of your implementation by wrapping a value of type Complex in a Just and show the result at the REPL.

3. Consider the following wrapper for optional values:

   record First a where
     constructor MkFirst
     value : Maybe a
   

   Implement interfaces Eq, Ord, Show, FromString, FromChar, FromDouble, Num, Neg, Integral, and Fractional for First a. All of these will require corresponding constraints on type parameter a. Consider implementing and using the following utility functions where they make sense:

   pureFirst : a -> First a
   
   mapFirst : (a -> b) -> First a -> First b
   
   mapFirst2 : (a -> b -> c) -> First a -> First b -> First c
   

4. Implement interfaces Semigroup and Monoid for First a in such a way, that (<+>) will return the first non-nothing argument and neutral is the corresponding neutral element. There must be no constraints on type parameter a in these implementations.

5. Repeat exercises 3 and 4 for record Last. The Semigroup implementation should return the last non-nothing value.

   record Last a where
     constructor MkLast
     value : Maybe a
   

6. Function foldMap allows us to map a function returning a Monoid over a list of values and accumulate the result using (<+>) at the same time. This is a very powerful way to accumulate the values stored in a list. Use foldMap and Last to extract the last element (if any) from a list.

   Note, that the type of foldMap is more general and not specialized to lists only. It works also for Maybe, Either and other container types we haven't looked at so far. We will learn about interface Foldable in a later section.

7. Consider record wrappers Any and All for boolean values:

   record Any where
     constructor MkAny
     any : Bool
   
   record All where
     constructor MkAll
     all : Bool
   

   Implement Semigroup and Monoid for Any, so that the result of (<+>) is True, if and only if at least one of the arguments is True. Make sure that neutral is indeed the neutral element for this operation.

   Likewise, implement Semigroup and Monoid for All, so that the result of (<+>) is True, if and only if both of the arguments are True. Make sure that neutral is indeed the neutral element for this operation.

8. Implement functions anyElem and allElems using foldMap and Any or All, respectively:

   -- True, if the predicate holds for at least one element
   anyElem : (a -> Bool) -> List a -> Bool
   
   -- True, if the predicate holds for all elements
   allElems : (a -> Bool) -> List a -> Bool
   

9. Record wrappers Sum and Product are mainly used to hold numeric types.

   record Sum a where
     constructor MkSum
     value : a
   
   record Product a where
     constructor MkProduct
     value : a
   

   Given an implementation of Num a, implement Semigroup (Sum a) and Monoid (Sum a), so that (<+>) corresponds to addition.

   Likewise, implement Semigroup (Product a) and Monoid (Product a), so that (<+>) corresponds to multiplication.

   When implementing neutral, remember that you can use integer literals when working with numeric types.

10. Implement sumList and productList by using foldMap together with the wrappers from Exercise 9:

    sumList : Num a => List a -> a
    
    productList : Num a => List a -> a
    

11. To appreciate the power and versatility of foldMap, after solving exercises 6 to 10 (or by loading Solutions.Inderfaces in a REPL session), run the following at the REPL, which will - in a single list traversal! - calculate the first and last element of the list as well as the sum and product of all values.

    > foldMap (\x => (pureFirst x, pureLast x, MkSum x, MkProduct x)) [3,7,4,12]
    (MkFirst (Just 3), (MkLast (Just 12), (MkSum 26, MkProduct 1008)))
    

    Note, that there are also Semigroup implementations for types with an Ord implementation, which will return the smaller or larger of two values. In case of types with an absolute minimum or maximum (for instance, 0 for natural numbers, or 0 and 255 for Bits8), these can even be extended to Monoid.

12. In an earlier exercise, you implemented a data type representing chemical elements and wrote a function for calculating their atomic masses. Define a new single field record type for representing atomic masses, and implement interfaces Eq, Ord, Show, FromDouble, Semigroup, and Monoid for this.

13. Use the new data type from exercise 12 to calculate the atomic mass of an element and compute the molecular mass of a molecule given by its formula.

    Hint: With a suitable utility function, you can use foldMap once again for this.

Final notes: If you are new to functional programming, make sure to give your implementations of exercises 6 to 10 a try at the REPL. Note, how we can implement all of these functions with a minimal amount of code and how, as shown in exercise 11, these behaviors can be combined in a single list traversal.

Conclusion

• Interfaces allow us to implement the same function with different behavior for different types.
• Functions taking one or more interface implementations as arguments are called constrained functions.
• Interfaces can be organized hierarchically by extending other interfaces.
• Interfaces implementations can themselves be constrained requiring other implementations to be available.
• Interface functions can be given a default implementation, which can be overridden by implementers, for instance for reasons of efficiency.
• Certain interfaces allow us to use literal values such as string or integer literals for our own data types.

Note, that I did not yet tell the whole story about literal values in this section. More details for using literals with types that accept only a restricted set of values can be found in the chapter about primitives.

What's next

In the next chapter, we have a closer look at functions and their types. We will learn about named arguments, implicit arguments, and erased arguments as well as some constructors for implementing more complex functions.

Functions Part 2

So far, we learned about the core features of the Idris language, which it has in common with several other pure, strongly typed programming languages like Haskell: (Higher-order) Functions, algebraic data types, pattern matching, parametric polymorphism (generic types and functions), and ad hoc polymorphism (interfaces and constrained functions).

In this chapter, we start to dissect Idris functions and their types for real. We learn about implicit arguments, named arguments, as well as erasure and quantities. But first, we'll look at let bindings and where blocks, which help us implement functions too complex to fit on a single line of code. Let's get started!

module Tutorial.Functions2

%default total

Let Bindings and Local Definitions

module Tutorial.Functions2.LetBindings

%default total

The functions we looked at so far were simple enough to be implemented directly via pattern matching without the need of additional auxiliary functions or variables. This is not always the case, and there are two important language constructs for introducing and reusing new local variables and functions. We'll look at these in two case studies.

Use Case 1: Arithmetic Mean and Standard Deviation

In this example, we'd like to calculate the arithmetic mean and the standard deviation of a list of floating point values. There are several things we need to consider.

First, we need a function for calculating the sum of a list of numeric values. The Prelude exports function sum for this:

Main> :t sum
Prelude.sum : Num a => Foldable t => t a -> a

This is - of course - similar to sumList from Exercise 10 of the last section, but generalized to all container types with a Foldable implementation. We will learn about interface Foldable in a later section.

In order to also calculate the variance, we need to convert every value in the list to a new value, as we have to subtract the mean from every value in the list and square the result. In the previous section's exercises, we defined function mapList for this. The Prelude - of course - already exports a similar function called map, which is again more general and works also like our mapMaybe for Maybe and mapEither for Either e. Here's its type:

Main> :t map
Prelude.map : Functor f => (a -> b) -> f a -> f b

Interface Functor is another one we'll talk about in a later section.

Finally, we need a way to calculate the length of a list of values. We use function length for this:

Main> :t List.length
Prelude.List.length : List a -> Nat

Here, Nat is the type of natural numbers (unbounded, unsigned integers). Nat is actually not a primitive data type but a sum type defined in the Prelude with data constructors Z : Nat (for zero) and S : Nat -> Nat (for successor). It might seem highly inefficient to define natural numbers this way, but the Idris compiler treats these and several other number-like types specially, and replaces them with primitive integers during code generation.

We are now ready to give the implementation of mean a go. Since this is Idris, and we care about clear semantics, we will quickly define a custom record type instead of just returning a tuple of Doubles. This makes it clearer, which floating point number corresponds to which statistic entity:

square : Double -> Double
square n = n * n

record Stats where
  constructor MkStats
  mean      : Double
  variance  : Double
  deviation : Double

stats : List Double -> Stats
stats xs =
  let len      := cast (length xs)
      mean     := sum xs / len
      variance := sum (map (\x => square (x - mean)) xs) / len
   in MkStats mean variance (sqrt variance)

As usual, we first try this at the REPL:

Tutorial.Functions2> stats [2,4,4,4,5,5,7,9]
MkStats 5.0 4.0 2.0

Seems to work, so let's digest this step by step. We introduce several new local variables (len, mean, and variance), which all will be used more than once in the remainder of the implementation. To do so, we use a let binding. This consists of the let keyword, followed by one or more variable assignments, followed by the final expression, which has to be prefixed by in. Note, that whitespace is significant again: We need to properly align the three variable names. Go ahead, and try out what happens if you remove a space in front of mean or variance. Note also, that the alignment of assignment operators := is optional. I do this, since I thinks it helps readability.

Let's also quickly look at the different variables and their types. len is the length of the list cast to a Double, since this is what's needed later on, where we divide other values of type Double by the length. Idris is very strict about this: We are not allowed to mix up numeric types without explicit casts. Please note, that in this case Idris is able to infer the type of len from the surrounding context. mean is straight forward: We sum up the values stored in the list and divide by the list's length. variance is the most involved of the three: We map each item in the list to a new value using an anonymous function to subtract the mean and square the result. We then sum up the new terms and divide again by the number of values.

Use Case 2: Simulating a Simple Web Server

In the second use case, we are going to write a slightly larger application. This should give you an idea about how to design data types and functions around some business logic you'd like to implement.

Assume we run a music streaming web server, where users can buy whole albums and listen to them online. We'd like to simulate a user connecting to the server and getting access to one of the albums they bought.

We first define a bunch of record types:

record Artist where
  constructor MkArtist
  name : String

record Album where
  constructor MkAlbum
  name   : String
  artist : Artist

record Email where
  constructor MkEmail
  value : String

record Password where
  constructor MkPassword
  value : String

record User where
  constructor MkUser
  name     : String
  email    : Email
  password : Password
  albums   : List Album

Most of these should be self-explanatory. Note, however, that in several cases (Email, Artist, Password) we wrap a single value in a new record type. Of course, we could have used the unwrapped String type instead, but we'd have ended up with many String fields, which can be hard to disambiguate. In order not to confuse an email string with a password string, it can therefore be helpful to wrap both of them in a new record type to drastically increase type safety at the cost of having to reimplement some interfaces. Utility function on from the Prelude is very useful for this. Don't forget to inspect its type at the REPL, and try to understand what's going on here.

Eq Artist where (==) = (==) `on` name

Eq Email where (==) = (==) `on` value

Eq Password where (==) = (==) `on` value

Eq Album where (==) = (==) `on` \a => (a.name, a.artist)

In case of Album, we wrap the two fields of the record in a Pair, which already comes with an implementation of Eq. This allows us to again use function on, which is very convenient.

Next, we have to define the data types representing server requests and responses:

record Credentials where
  constructor MkCredentials
  email    : Email
  password : Password

record Request where
  constructor MkRequest
  credentials : Credentials
  album       : Album

data Response : Type where
  UnknownUser     : Email -> Response
  InvalidPassword : Response
  AccessDenied    : Email -> Album -> Response
  Success         : Album -> Response

For server responses, we use a custom sum type encoding the possible outcomes of a client request. In practice, the Success case would return some kind of connection to start the actual album stream, but we just wrap up the album we found to simulate this behavior.

We can now go ahead and simulate the handling of a request at the server. To emulate our user data base, a simple list of users will do. Here's the type of the function we'd like to implement:

DB : Type
DB = List User

handleRequest : DB -> Request -> Response

Note, how we defined a short alias for List User called DB. This is often useful to make lengthy type signatures more readable and communicate the meaning of a type in the given context. However, this will not introduce a new type, nor will it increase type safety: DB is identical to List User, and as such, a value of type DB can be used wherever a List User is expected and vice versa. In more complex programs it is therefore usually preferable to define new types by wrapping values in single-field records.

The implementation will proceed as follows: It will first try and lookup a User by is email address in the data base. If this is successful, it will compare the provided password with the user's actual password. If the two match, it will lookup the requested album in the user's list of albums. If all of these steps succeed, the result will be an Album wrapped in a Success. If any of the steps fails, the result will describe exactly what went wrong.

Here's a possible implementation:

handleRequest db (MkRequest (MkCredentials email pw) album) =
  case lookupUser db of
    Just (MkUser _ _ password albums)  =>
      if password == pw then lookupAlbum albums else InvalidPassword

    Nothing => UnknownUser email

  where lookupUser : List User -> Maybe User
        lookupUser []        = Nothing
        lookupUser (x :: xs) =
          if x.email == email then Just x else lookupUser xs

        lookupAlbum : List Album -> Response
        lookupAlbum []        = AccessDenied email album
        lookupAlbum (x :: xs) =
          if x == album then Success album else lookupAlbum xs

I'd like to point out several things in this example. First, note how we can extract values from nested records in a single pattern match. Second, we defined two local functions in a where block: lookupUser, and lookupAlbum. Both of these have access to all variables in the surrounding scope. For instance, lookupUser uses the email variable from the pattern match in the implementation's first line. Likewise, lookupAlbum makes use of the album variable.

A where block introduces new local definitions, accessible only from the surrounding scope and from other functions defined later in the same where block. These need to be explicitly typed and indented by the same amount of whitespace.

Local definitions can also be introduced before a function's implementation by using the let keyword. This usage of let is not to be confused with let bindings described above, which are used to bind and reuse the results of intermediate computations. Below is how we could have implemented handleRequest with local definitions introduced by the let keyword. Again, all definitions have to be properly typed and indented:

handleRequest' : DB -> Request -> Response
handleRequest' db (MkRequest (MkCredentials email pw) album) =
  let lookupUser : List User -> Maybe User
      lookupUser []        = Nothing
      lookupUser (x :: xs) =
        if x.email == email then Just x else lookupUser xs

      lookupAlbum : List Album -> Response
      lookupAlbum []        = AccessDenied email album
      lookupAlbum (x :: xs) =
        if x == album then Success album else lookupAlbum xs

   in case lookupUser db of
        Just (MkUser _ _ password albums)  =>
          if password == pw then lookupAlbum albums else InvalidPassword

        Nothing => UnknownUser email

Exercises

The exercises in this section are supposed to increase you experience in writing purely functional code. In some cases it might be useful to use let expressions or where blocks, but this will not always be required.

Exercise 3 is again of utmost importance. traverseList is a specialized version of the more general traverse, one of the most powerful and versatile functions available in the Prelude (check out its type!).

1. Module Data.List in base exports functions find and elem. Inspect their types and use these in the implementation of handleRequest. This should allow you to completely get rid of the where block.

2. Refactor handleRequest to use Either, such that handleRequest : DB -> Request -> Either Failure Album, where

   data Failure : Type where
     UnknownUser : Email -> Failure
     InvalidPassword : Failure
     AccessDenied : Email -> Album -> Failure
   

   Hint: You may find nested case statements helpful.

3. Define an enumeration type listing the four nucleobases occurring in DNA strands. Define also a type alias DNA for lists of nucleobases. Declare and implement function readBase for converting a single character (type Char) to a nucleobase. You can use character literals in your implementation like so: 'A', 'a'. Note, that this function might fail, so adjust the result type accordingly.

4. Implement the following function, which tries to convert all values in a list with a function, which might fail. The result should be a Just holding the list of converted values in unmodified order, if and only if every single conversion was successful.

   traverseList : (a -> Maybe b) -> List a -> Maybe (List b)
   

   You can verify, that the function behaves correctly with the following test: traverseList Just [1,2,3] = Just [1,2,3].

5. Implement function readDNA : String -> Maybe DNA using the functions and types defined in exercises 2 and 3. You will also need function unpack from the Prelude.

6. Implement function complement : DNA -> DNA to calculate the complement of a strand of DNA.

The Truth about Function Arguments

module Tutorial.Functions2.TheTruth

%default total

So far, when we defined a top level function, it looked something like the following:

zipEitherWith : (a -> b -> c) -> Either e a -> Either e b -> Either e c
zipEitherWith f (Right va) (Right vb) = Right (f va vb)
zipEitherWith f (Left e)   _          = Left e
zipEitherWith f _          (Left e)   = Left e

Function zipEitherWith is a generic higher-order function combining the values stored in two Eithers via a binary function. If either of the Either arguments is a Left, the result is also a Left.

This is a generic function with type parameters a, b, c, and e. However, there is a more verbose type for zipEitherWith, which is visible in the REPL when entering :ti zipEitherWith (the i here tells Idris to include implicit arguments). You will get a type similar to this:

zipEitherWith' :  {0 a : Type}
               -> {0 b : Type}
               -> {0 c : Type}
               -> {0 e : Type}
               -> (a -> b -> c)
               -> Either e a
               -> Either e b
               -> Either e c

In order to understand what's going on here, we will have to talk about named arguments, implicit arguments, and quantities.

Named Arguments

In a function type, we can give each argument a name. Like so:

fromMaybe : (deflt : a) -> (ma : Maybe a) -> a
fromMaybe deflt Nothing = deflt
fromMaybe _    (Just x) = x

Here, the first argument is given name deflt, the second ma. These names can be reused in a function's implementation, as was done for deflt, but this is not mandatory: We are free to use different names in the implementation. There are several reasons, why we'd choose to name our arguments: It can serve as documentation, but it also allows us to pass the arguments to a function in arbitrary order when using the following syntax:

extractBool : Maybe Bool -> Bool
extractBool v = fromMaybe { ma = v, deflt = False }

Or even :

extractBool2 : Maybe Bool -> Bool
extractBool2 = fromMaybe { deflt = False }

The arguments in a record's constructor are automatically named in accordance with the field names:

record Dragon where
  constructor MkDragon
  name      : String
  strength  : Nat
  hitPoints : Int16

gorgar : Dragon
gorgar = MkDragon { strength = 150, name = "Gorgar", hitPoints = 10000 }

For the use cases described above, named arguments are merely a convenience and completely optional. However, Idris is a dependently typed programming language: Types can be calculated from and depend on values. For instance, the result type of a function can depend on the value of one of its arguments. Here's a contrived example:

IntOrString : Bool -> Type
IntOrString True  = Integer
IntOrString False = String

intOrString : (v : Bool) -> IntOrString v
intOrString False = "I'm a String"
intOrString True  = 1000

If you see such a thing for the first time, it can be hard to understand what's going on here. First, function IntOrString computes a Type from a Bool value: If the argument is True, it returns type Integer, if the argument is False it returns String. We use this to calculate the return type of function intOrString based on its boolean argument v: If v is True, the return type is (in accordance with IntOrString True = Integer) Integer, otherwise it is String.

Note, how in the type signature of intOrString, we must give the argument of type Bool a name (v) in order to reference it in the result type IntOrString v.

You might wonder at this moment, why this is useful and why we would ever want to define a function with such a strange type. We will see lots of very useful examples in due time! For now, suffice to say that in order to express dependent function types, we need to name at least some of the function's arguments and refer to them by name in the types of other arguments.

Implicit Arguments

Implicit arguments are arguments, the values of which the compiler should infer and fill in for us automatically. For instance, in the following function signature, we expect the compiler to infer the value of type parameter a automatically from the types of the other arguments (ignore the 0 quantity for the moment; I'll explain it in the next subsection):

maybeToEither : {0 a : Type} -> Maybe a -> Either String a
maybeToEither Nothing  = Left "Nope"
maybeToEither (Just x) = Right x

-- Please remember, that the above is
-- equivalent to the following:
maybeToEither' : Maybe a -> Either String a
maybeToEither' Nothing  = Left "Nope"
maybeToEither' (Just x) = Right x

As you can see, implicit arguments are wrapped in curly braces, unlike explicit named arguments, which are wrapped in parentheses. Inferring the value of an implicit argument is not always possible. For instance, if we enter the following at the REPL, Idris will fail with an error:

Tutorial.Functions2> show (maybeToEither Nothing)
Error: Can't find an implementation for Show (Either String ?a).

Idris is unable to find an implementation of Show (Either String a) without knowing what a actually is. Note the question mark in front of the type parameter: ?a. If this happens, there are several ways to help the type checker. We could, for instance, pass a value for the implicit argument explicitly. Here's the syntax to do this:

Tutorial.Functions2> show (maybeToEither {a = Int8} Nothing)
"Left "Nope""

As you can see, we use the same syntax as shown above for explicit named arguments and the two forms of argument passing can be mixed.

We could also specify the type of the whole expression using utility function the from the Prelude:

Tutorial.Functions2> show (the (Either String Int8) (maybeToEither Nothing))
"Left "Nope""

It is instructive to have a look at the type of the:

Tutorial.Functions2> :ti the
Prelude.the : (0 a : Type) -> a -> a

Compare this with the identity function id:

Tutorial.Functions2> :ti id
Prelude.id : {0 a : Type} -> a -> a

The only difference between the two: In case of the, the type parameter a is an explicit argument, while in case of id, it is an implicit argument. Although the two functions have almost identical types (and implementations!), they serve quite different purposes: the is used to help type inference, while id is used whenever we'd like to return an argument without modifying it at all (which, in the presence of higher-order functions, happens surprisingly often).

Both ways to improve type inference shown above are used quite often, and must be understood by Idris programmers.

Multiplicities

Finally, we need to talk about the zero multiplicity, which appeared in several of the type signatures in this section. Idris 2, unlike its predecessor Idris 1, is based on a core language called quantitative type theory (QTT): Every variable in Idris 2 is associated with one of three possible multiplicities:

• 0, meaning that the variable is erased at runtime.
• 1, meaning that the variable is used exactly once at runtime.
• Unrestricted (the default), meaning that the variable is used an arbitrary number of times at runtime.

We will not talk about the most complex of the three, multiplicity 1, here. We are, however, often interested in multiplicity 0: A variable with multiplicity 0 is only relevant at compile time. It will not make any appearance at runtime, and the computation of such a variable will never affect a program's runtime performance.

In the type signature of maybeToEither we see that type parameter a has multiplicity 0, and will therefore be erased and is only relevant at compile time, while the Maybe a argument has unrestricted multiplicity.

It is also possible to annotate explicit arguments with multiplicities, in which case the argument must again be put in parentheses. For an example, look again at the type signature of the.

Underscores

It is often desirable, to only write as little code as necessary and let Idris figure out the rest. We have already learned about one such occasion: Catch-all patterns. If a variable in a pattern match is not used on the right hand side, we can't just drop it, as this would make it impossible for Idris to know, which of several arguments we were planning to drop, but we can use an underscore as a placeholder instead:

isRight : Either a b -> Bool
isRight (Right _) = True
isRight _         = False

But when we look at the type signature of isRight, we will note that type parameters a and b are also only used once, and are therefore of no importance. Let's get rid of them:

isRight' : Either _ _ -> Bool
isRight' (Right _) = True
isRight' _         = False

In the detailed type signature of zipEitherWith, it should be obvious for Idris that the implicit arguments are of type Type. After all, all of them are later on applied to the Either type constructor, which is of type Type -> Type -> Type. Let's get rid of them:

zipEitherWith'' :  {0 a : _}
                -> {0 b : _}
                -> {0 c : _}
                -> {0 e : _}
                -> (a -> b -> c)
                -> Either e a
                -> Either e b
                -> Either e c

Consider the following contrived example:

foo : Integer -> String
foo n = show (the (Either String Integer) (Right n))

Since we wrap an Integer in a Right, it is obvious that the second argument in Either String Integer is Integer. Only the String argument can't be inferred by Idris. Even better, the Either itself is obvious! Let's get rid of the unnecessary noise:

foo' : Integer -> String
foo' n = show (the (_ String _) (Right n))

Please note, that using underscores as in foo' is not always desirable, as it can quite drastically obfuscate the written code. Always use a syntactic convenience to make code more readable, and not to show people how clever you are.

Programming with Holes

module Tutorial.Functions2.Holes

%default total

Solved all the exercises so far? Got angry at the type checker for always complaining and never being really helpful? It's time to change that. Idris comes with several highly useful interactive editing features. Sometimes, the compiler is able to implement complete functions for us (if the types are specific enough). Even if that's not possible, there's an incredibly useful and important feature, which can help us when the types are getting too complicated: Holes. Holes are variables, the names of which are prefixed with a question mark. We can use them as placeholders whenever we plan to implement a piece of functionality at a later time. In addition, their types and the types and quantities of all other variables in scope can be inspected at the REPL (or in your editor, if you setup the necessary plugin). Let's see them holes in action.

Remember the traverseList example from an Exercise earlier in this section? If this was your first encounter with applicative list traversals, this might have been a nasty bit of work. Well, let's just make it a wee bit harder still. We'd like to implement the same piece of functionality for functions returning Either e, where e is a type with a Semigroup implementation, and we'd like to accumulate the values in all Lefts we meet along the way.

Here's the type of the function:

traverseEither :  Semigroup e
               => (a -> Either e b)
               -> List a
               -> Either e (List b)

As an optional exercise, you may wish to attempt this yourself first. You've seen everything you need. Consider:

• semigroups have an append operation <+> : e -> e -> e that combines two values into one
• the empty list will succeed vacuously
• if any of the function applications fail, you'll return a consolidation of all of the errors e
• if all of the function applications succeed, you'll return a list with all of the results b
• if you get it to compile, there are some test functions and variables at the bottom of this section for you to confirm that it's working as intended

Now, in order to follow along, you might want to start your own Idris source file, load it into a REPL session and adjust the code as described here. The first thing we'll do, is write a skeleton implementation with a hole on the right hand side:

traverseEither fun as = ?impl

When you now go to the REPL and reload the file using command :r, you can enter :m to list all the metavariables:

Tutorial.Functions2> :m
1 hole:
  Tutorial.Functions2.impl : Either e (List b)

Next, we'd like to display the hole's type (including all variables in the surrounding context plus their types):

Tutorial.Functions2> :t impl
 0 b : Type
 0 a : Type
 0 e : Type
   as : List a
   fun : a -> Either e b
------------------------------
impl : Either e (List b)

So, we have some erased type parameters (a, b, and e), a value of type List a called as, and a function from a to Either e b called fun. Our goal is to come up with a value of type Either a (List b).

We could just return a Right [], but that only make sense if our input list is indeed the empty list. We therefore should start with a pattern match on the list:

traverseEither fun []        = ?impl_0
traverseEither fun (x :: xs) = ?impl_1

The result is two holes, which must be given distinct names. When inspecting impl_0, we get the following result:

Tutorial.Functions2> :t impl_0
 0 b : Type
 0 a : Type
 0 e : Type
   fun : a -> Either e b
------------------------------
impl_0 : Either e (List b)

Now, this is an interesting situation. We are supposed to come up with a value of type Either e (List b) with nothing to work with. We know nothing about a, so we can't provide an argument with which to invoke fun. Likewise, we know nothing about e or b either, so we can't produce any values of these either. The only option we have is to replace impl_0 with an empty list wrapped in a Right:

traverseEither fun []        = Right []

The non-empty case is of course slightly more involved. Here's the context of ?impl_1:

Tutorial.Functions2> :t impl_1
 0 b : Type
 0 a : Type
 0 e : Type
   x : a
   xs : List a
   fun : a -> Either e b
------------------------------
impl_1 : Either e (List b)

Since x is of type a, we can either use it as an argument to fun or drop and ignore it. xs, on the other hand, is the remainder of the list of type List a. We could again drop it or process it further by invoking traverseEither recursively. Since the goal is to try and convert all values, we should drop neither. Since in case of two Lefts we are supposed to accumulate the values, we eventually need to run both computations anyway (invoking fun, and recursively calling traverseEither). We therefore can do both at the same time and analyze the results in a single pattern match by wrapping both in a Pair:

traverseEither fun (x :: xs) =
  case (fun x, traverseEither fun xs) of
   p => ?impl_2

Once again, we inspect the context:

Tutorial.Functions2> :t impl_2
 0 b : Type
 0 a : Type
 0 e : Type
   xs : List a
   fun : a -> Either e b
   x : a
   p : (Either e b, Either e (List b))
------------------------------
impl_2 : Either e (List b)

We'll definitely need to pattern match on pair p next to figure out, which of the two computations succeeded:

traverseEither fun (x :: xs) =
  case (fun x, traverseEither fun xs) of
    (Left y, Left z)   => ?impl_6
    (Left y, Right _)  => ?impl_7
    (Right _, Left z)  => ?impl_8
    (Right y, Right z) => ?impl_9

At this point we might have forgotten what we actually wanted to do (at least to me, this happens annoyingly often), so we'll just quickly check what our goal is:

Tutorial.Functions2> :t impl_6
 0 b : Type
 0 a : Type
 0 e : Type
   xs : List a
   fun : a -> Either e b
   x : a
   y : e
   z : e
------------------------------
impl_6 : Either e (List b)

So, we are still looking for a value of type Either e (List b), and we have two values of type e in scope. According to the spec we want to accumulate these using es Semigroup implementation. We can proceed for the other cases in a similar manner, remembering that we should return a Right, if and only if all conversions where successful:

traverseEither fun (x :: xs) =
  case (fun x, traverseEither fun xs) of
    (Left y, Left z)   => Left (y <+> z)
    (Left y, Right _)  => Left y
    (Right _, Left z)  => Left z
    (Right y, Right z) => Right (y :: z)

To reap the fruits of our labour, let's show off with a small example:

data Nucleobase = Adenine | Cytosine | Guanine | Thymine

readNucleobase : Char -> Either (List String) Nucleobase
readNucleobase 'A' = Right Adenine
readNucleobase 'C' = Right Cytosine
readNucleobase 'G' = Right Guanine
readNucleobase 'T' = Right Thymine
readNucleobase c   = Left ["Unknown nucleobase: " ++ show c]

DNA : Type
DNA = List Nucleobase

readDNA : String -> Either (List String) DNA
readDNA = traverseEither readNucleobase . unpack

Let's try this at the REPL:

Tutorial.Functions2> readDNA "CGTTA"
Right [Cytosine, Guanine, Thymine, Thymine, Adenine]
Tutorial.Functions2> readDNA "CGFTAQ"
Left ["Unknown nucleobase: 'F'", "Unknown nucleobase: 'Q'"]

Interactive Editing

There are plugins available for several editors and programming environments, which facilitate interacting with the Idris compiler when implementing your functions. One editor, which is well supported in the Idris community, is Neovim. Since I am a Neovim user myself, I added some examples of what's possible to the appendix. Now would be a good time to start using the utilities discussed there.

If you use a different editor, probably with less support for the Idris programming language, you should at the very least have a REPL session open all the time, where the source file you are currently working on is loaded. This allows you to introduce new metavariables and inspect their types and context as you develop your code.

Conclusion

We again covered a lot of ground in this section. I can't stress enough that you should get yourselves accustomed to programming with holes and let the type checker help you figure out what to do next.

• When in need of local utility functions, consider defining them as local definitions in a where block.

• Use let expressions to define and reuse local variables.

• Function arguments can be given a name, which can serve as documentation, can be used to pass arguments in any order, and is used to refer to them in dependent types.

• Implicit arguments are wrapped in curly braces. The compiler is supposed to infer them from the context. If that's not possible, they can be passed explicitly as other named arguments.

• Whenever possible, Idris adds implicit erased arguments for all type parameters automatically.

• Quantities allow us to track how often a function argument is used. Quantity 0 means, the argument is erased at runtime.

• Use holes as placeholders for pieces of code you plan to fill in at a later time. Use the REPL (or your editor) to inspect the types of holes together with the names, types, and quantities of all variables in their context.

What's next

In the next chapter we'll start using dependent types to help us write provably correct code. Having a good understanding of how to read Idris' type signatures will be of paramount importance there. Whenever you feel lost, add one or more holes and inspect their context to decide what to do next.

Dependent Types

The ability to calculate types from values, pass them as arguments to functions, and return them as results from functions - in short, being a dependently typed language - is one of the most distinguishing features of Idris. Many of the more advanced type level extensions of languages like Haskell (and quite a bit more) can be treated in one fell swoop with dependent types.

module Tutorial.Dependent

%default total

Consider the following functions:

bogusMapList : (a -> b) -> List a -> List b
bogusMapList _ _ = []

bogusZipList : (a -> b -> c) -> List a -> List b -> List c
bogusZipList _ _ _ = []

The implementations type check, and still, they are obviously not what users of our library would expect. In the first example, we'd expect the implementation to apply the function argument to all values stored in the list, without dropping any of them or changing their order. The second is trickier: The two list arguments might be of different length. What are we supposed to do when that's the case? Return a list of the same length as the smaller of the two? Return an empty list? Or shouldn't we in most use cases expect the two lists to be of the same length? How could we even describe such a precondition?

Length-Indexed Lists

module Tutorial.Dependent.LengthIndexedLists

%default total

The answer to the issues described above is of course: Dependent types. Before we proceed to our example, first consider how Idris recursively defines the natural numbers (here affixed with apostrophes to avoid introducing a conflict with the actual definition of Nat, which you can find here for reference)):

data Nat' : Type where
  Z' : Nat'
  S' : Nat' -> Nat'

In this scheme, 0 is represented by Z, 1 is represented by S Z, 2 is represented by S (S Z), and so on. Idris does this automatically so if you enter Z or S Z into the REPL, it will return 0 or 1. Note that the only function inherently available to act on a value of type Nat is our data constructor S, which represents the successor function, i.e. adding 1.

Also note that in Idris, every Nat can be represented as either a Z or an S n where n is another Nat. Much as every List a can be represented as either a Nil or an x :: xs (where x is an a and xs is a List a), this informs our pattern matching when solving problems.

Now we can consider the textbook introductory example of dependent types, the vector, which is a list indexed by its length:

public export
data Vect : (len : Nat) -> (a : Type) -> Type where
  Nil  : Vect 0 a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

Before we move on, please compare this with the implementation of Seq in the section about algebraic data types. The constructors are exactly the same: Nil and (::). But there is an important difference: Vect, unlike Seq or List, is not a function from Type to Type, it is a function from Nat to Type to Type. Go ahead! Open the REPL and verify this! The Nat argument (also called an index) represents the length of the vector here. Nil has type Vect 0 a: A vector of length zero. Cons has type a -> Vect n a -> Vect (S n) a: It is exactly one element longer (S n) than its second argument, which is of length n.

Let's experiment with this idea to gain a better understanding. There is only one way to come up with a vector of length zero:

ex1 : Vect 0 Integer
ex1 = Nil

The following, on the other hand, leads to a type error (a pretty complicated one, actually):

failing "Mismatch between: S ?n and 0."
  ex2 : Vect 0 Integer
  ex2 = [12]

The problem: [12] gets desugared to 12 :: Nil, but this has the wrong type! Since Nil has type Vect 0 Integer here, 12 :: Nil has type Vect (S 0) Integer, which is identical to Vect 1 Integer. Idris verifies, at compile time, that our vector is of the correct length!

ex3 : Vect 1 Integer
ex3 = [12]

So, we found a way to encode the length of a list-like data structure in its type, and it is a type error if the number of elements in a vector does not agree with then length given in its type. We will shortly see several use cases, where this additional piece of information allows us to be more precise in the types and rule out additional programming mistakes. But first, we need to quickly clarify some terminology.

Type Indices versus Type Parameters

Vect is not only a generic type, parameterized over the type of elements it holds, it is actually a family of types, each of them associated with a natural number representing it's length. We also say, the type family Vect is indexed by its length.

The difference between a type parameter and an index is, that the latter can and does change across data constructors, while the former is the same for all data constructors. Or, put differently, we can learn about the value of an index by pattern matching on a value of the type family, while this is not possible with a type parameter.

Let's demonstrate this with a contrived example:

data Indexed : Nat -> Type where
  I0 : Indexed 0
  I3 : Indexed 3
  I4 : String -> Indexed 4

Here, Indexed is indexed over its Nat argument, as values of the index changes across constructors (I chose some arbitrary value for each constructor), and we can learn about these values by pattern matching on Indexed values. We can use this, for instance, to create a Vect of the same length as the index of Indexed:

fromIndexed : Indexed n -> a -> Vect n a

Go ahead, and try implementing this yourself! Work with holes, pattern match on the Indexed argument, and learn about the expected output type in each case by inspecting the holes and their context.

Here is my implementation:

fromIndexed I0     va = []
fromIndexed I3     va = [va, va, va]
fromIndexed (I4 _) va = [va, va, va, va]

As you can see, by pattern matching on the value of the Indexed n argument, we learned about the value of the n index itself, which was necessary to return a Vect of the correct length.

Length-Preserving map

Function bogusMapList behaved unexpectedly, because it always returned the empty list. With Vect, we need to be true to the types here. If we map over a Vect, the argument and output type contain a length index, and these length indices will tell us exactly, if and how the lengths of our vectors are modified:

map3_1 : (a -> b) -> Vect 3 a -> Vect 1 b
map3_1 f [_,y,_] = [f y]

map5_0 : (a -> b) -> Vect 5 a -> Vect 0 b
map5_0 f _ = []

map5_10 : (a -> b) -> Vect 5 a -> Vect 10 b
map5_10 f [u,v,w,x,y] = [f u, f u, f v, f v, f w, f w, f x, f x, f y, f y]

While these examples are quite interesting, they are not really useful, are they? That's because they are too specialized. We'd like to have a general function for mapping vectors of any length. Instead of using concrete lengths in type signatures, we can also use variables as already seen in the definition of Vect. This allows us to declare the general case:

mapVect' : (a -> b) -> Vect n a -> Vect n b

This type describes a length-preserving map. It is actually more instructive (but not necessary) to include the implicit arguments as well:

mapVect : {0 a,b : _} -> {0 n : Nat} -> (a -> b) -> Vect n a -> Vect n b

We ignore the two type parameters a, and b, as these just describe a generic function (note, however, that we can group arguments of the same type and quantity in a single pair of curly braces; this is optional, but it sometimes helps making type signatures a bit shorter). The implicit argument of type Nat, however, tells us that the input and output Vect are of the same length. It is a type error to not uphold to this contract. When implementing mapVect, it is very instructive to follow along and use some holes. In order to get any information about the length of the Vect argument, we need to pattern match on it:

mapVect _ Nil       = ?impl_0
mapVect f (x :: xs) = ?impl_1

At the REPL, we learn the following:

Tutorial.Dependent> :t impl_0
 0 a : Type
 0 b : Type
 0 n : Nat
------------------------------
impl_0 : Vect 0 b


Tutorial.Dependent> :t impl_1
 0 a : Type
 0 b : Type
   x : a
   xs : Vect n a
   f : a -> b
 0 n : Nat
------------------------------
impl_1 : Vect (S n) b

The first hole, impl_0 is of type Vect 0 b. There is only one such value, as discussed above:

mapVect _ Nil       = Nil

The second case is again more interesting. We note, that xs is of type Vect n a, for an arbitrary length n (given as an erased argument), while the result is of type Vect (S n) b. So, the result has to be one element longer than xs. Luckily, we already have a value of type a (bound to variable x) and a function from a to b (bound to variable f), so we can apply f to x and prepend the result to a yet unknown remainder:

mapVect f (x :: xs) = f x :: ?rest

Let's inspect the new hole at the REPL:

Tutorial.Dependent> :t rest
 0 a : Type
 0 b : Type
   x : a
   xs : Vect n a
   f : a -> b
 0 n : Nat
------------------------------
rest : Vect n b

Now, we have a Vect n a and need a Vect n b, without knowing anything else about n. We could learn more about n by pattern matching further on xs, but this would quickly lead us down a rabbit hole, since after such a pattern match, we'd end up with another Nil case and another cons case, with a new tail of unknown length. Instead, we can invoke mapVect recursively to convert the remainder (xs) to a Vect n b. The type checker guarantees, that the lengths of xs and mapVect f xs are the same, so the whole expression type checks and we are done:

mapVect f (x :: xs) = f x :: mapVect f xs

Zipping Vectors

Let us now have a look at bogusZipList: We'd like to pairwise merge two lists holding elements of (possibly) distinct types through a given binary function. As discussed above, the most reasonable thing to do is to expect the two lists as well as the result to be of equal length. With Vect, this can be expressed and implemented as follows:

export
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith f []        []         = Nil
zipWith f (x :: xs) (y :: ys)  = f x y :: zipWith f xs ys

Now, here is an interesting thing: The totality checker (activated throughout this source file due to the initial %default total pragma) accepts the above implementation as being total, although it is missing two more cases. This works, because Idris can figure out on its own, that the other two cases are impossible. From the pattern match on the first Vect argument, Idris learns whether n is zero or the successor of another natural number. But from this it can derive, whether the second vector, being also of length n, is a Nil or a cons. Still, it can be informative to add the impossible cases explicitly. We can use keyword impossible to do so:

zipWith _ [] (_ :: _) impossible
zipWith _ (_ :: _) [] impossible

It is - of course - a type error to annotate a case in a pattern match with impossible, if Idris cannot verify that this case is indeed impossible. We will learn in a later section what to do, when we think we are right about an impossible case and Idris is not.

Let's give zipWith a spin at the REPL:

Tutorial.Dependent> zipWith (*) [1,2,3] [10,20,30]
[10, 40, 90]
Tutorial.Dependent> zipWith (\x,y => x ++ ": " ++ show y) ["The answer"] [42]
["The answer: 42"]
Tutorial.Dependent> zipWith (*) [1,2,3] [10,20]
... Nasty type error ...

Simplifying Type Errors

It is amazing to experience the amount of work Idris can do for us and the amount of things it can infer on its own when things go well. When things don't go well, however, the error messages we get from Idris can be quite long and hard to understand, especially for programmers new to the language. For instance, the error message in the last REPL example above was pretty long, listing different things Idris tried to do together with the reason why each of them failed.

If this happens, it often means that a combination of a type error and an ambiguity resulting from overloaded function names is at work. In the example above, the two vectors are of distinct length, which leads to a type error if we interpret the list literals as vectors. However, list literals are overloaded to work with all data types with constructors Nil and (::), so Idris will now try other data constructors than those of Vect (the ones of List and Stream from the Prelude in this case), each of which will again fail with a type error since zipWith expects arguments of type Vect, and neither List nor Stream will work.

If this happens, prefixing overloaded function names with their namespaces can often simplify things, as Idris no longer needs to disambiguate these functions:

Tutorial.Dependent> zipWith (*) (Dependent.(::) 1 Dependent.Nil) Dependent.Nil
Error: When unifying:
    Vect 0 ?c
and:
    Vect 1 ?c
Mismatch between: 0 and 1.

Here, the message is much clearer: Idris can't unify the lengths of the two vectors. Unification means: Idris tries to at compile time convert two expressions to the same normal form. If this succeeds, the two expressions are considered to be equivalent, if it doesn't, Idris fails with a unification error.

As an alternative to prefixing overloaded functions with their namespace, we can use the to help with type inference:

Tutorial.Dependent> zipWith (*) (the (Vect 3 _) [1,2,3]) (the (Vect 2 _) [10,20])
Error: When unifying:
    Vect 2 ?c
and:
    Vect 3 ?c
Mismatch between: 0 and 1.

It is interesting to note, that the error above is not "Mismatch between: 2 and 3" but "Mismatch between: 0 and 1" instead. Here's what's going on: Idris tries to unify integer literals 2 and 3, which are first converted to the corresponding Nat values S (S Z) and S (S (S Z)), respectively. The two patterns match until we arrive at Z vs S Z, corresponding to values 0 and 1, which is the discrepancy reported in the error message.

Creating Vectors

So far, we were able to learn something about the lengths of vectors by pattern matching on them. In the Nil case, it was clear that the length is 0, while in the cons case the length was the successor of another natural number. This is not possible when we want to create a new vector:

failing "Mismatch between: S ?n and n."
  fill : a -> Vect n a

You will have a hard time implementing fill. The following, for instance, leads to a type error:

  fill va = [va,va]

The problem is, that the callers of our function decide about the length of the resulting vector. The full type of fill is actually the following:

fill' : {0 a : Type} -> {0 n : Nat} -> a -> Vect n a

You can read this type as follows: For every type a and for every natural number n (about which I know nothing at runtime, since it has quantity zero), given a value of type a, I'll give you a vector holding exactly n elements of type a. This is like saying: "Think about a natural number n, and I'll give you n apples without you telling me the value of n". Idris is powerful, but it is not a clairvoyant.

In order to implement fill, we need to know what n actually is: We need to pass n as an explicit, unerased argument, which will allow us to pattern match on it and decide - based on this pattern match - which constructors of Vect to use:

export
replicate : (n : Nat) -> a -> Vect n a

Now, replicate is a dependent function type: The output type depends on the value of one of the arguments. It is straight forward to implement replicate by pattern matching on n:

replicate 0     _  = []
replicate (S k) va = va :: replicate k va

This is a pattern that comes up often when working with indexed types: We can learn about the values of the indices by pattern matching on the values of the type family. However, in order to return a value of the type family from a function, we need to either know the values of the indices at compile time (see constants ex1 or ex3, for instance), or we need to have access to the values of the indices at runtime, in which case we can pattern match on them and learn from this, which constructor(s) of the type family to use.

Exercises part 1

1. Implement a function len : List a -> Nat for calculating the length of a List. For example, len [1, 1, 1] produces 3.

2. Implement function head for non-empty vectors:

   head : Vect (S n) a -> a
   

   Note, how we can describe non-emptiness by using a pattern in the length of Vect. This rules out the Nil case, and we can return a value of type a, without having to wrap it in a Maybe! Make sure to add an impossible clause for the Nil case (although this is not strictly necessary here).

3. Using head as a reference, declare and implement function tail for non-empty vectors. The types should reflect that the output is exactly one element shorter than the input.

4. Implement zipWith3. If possible, try to doing so without looking at the implementation of zipWith:

   zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d
   

5. Declare and implement a function foldSemi for accumulating the values stored in a List through Semigroups append operator ((<+>)). (Make sure to only use a Semigroup constraint, as opposed to a Monoid constraint.)

6. Do the same as in Exercise 4, but for non-empty vectors. How does a vector's non-emptiness affect the output type?

7. Given an initial value of type a and a function a -> a, we'd like to generate Vects of as, the first value of which is a, the second value being f a, the third being f (f a) and so on.

   For instance, if a is 1 and f is (* 2), we'd like to get results similar to the following: [1,2,4,8,16,...].

   Declare and implement function iterate, which should encapsulate this behavior. Get some inspiration from replicate if you don't know where to start.

8. Given an initial value of a state type s and a function fun : s -> (s,a), we'd like to generate Vects of as. Declare and implement function generate, which should encapsulate this behavior. Make sure to use the updated state in every new invocation of fun.

   Here's an example how this can be used to generate the first n Fibonacci numbers:

   generate 10 (\(x,y) => let z = x + y in ((y,z),z)) (0,1)
   [1, 2, 3, 5, 8, 13, 21, 34, 55, 89]
   

9. Implement function fromList, which converts a list of values to a Vect of the same length. Use holes if you get stuck:

   fromList : (as : List a) -> Vect (length as) a
   

   Note how, in the type of fromList, we can calculate the length of the resulting vector by passing the list argument to function length.

10. Consider the following declarations:

maybeSize : Maybe a -> Nat

fromMaybe : (m : Maybe a) -> Vect (maybeSize m) a

Choose a reasonable implementation for maybeSize and implement fromMaybe afterwards.

Fin: Safe Indexing into Vectors

module Tutorial.Dependent.Fin

import Tutorial.Dependent.LengthIndexedLists

%default total

Consider function index, which tries to extract a value from a List at the given position:

indexList : (pos : Nat) -> List a -> Maybe a
indexList _     []        = Nothing
indexList 0     (x :: _)  = Just x
indexList (S k) (_ :: xs) = indexList k xs

Now, here is a thing to consider when writing functions like indexList: Do we want to express the possibility of failure in the output type, or do we want to restrict the accepted arguments, so the function can no longer fail? These are important design decisions, especially in larger applications. Returning a Maybe or Either from a function forces client code to eventually deal with the Nothing or Left case, and until this happens, all intermediary results will carry the Maybe or Either stain, which will make it more cumbersome to run calculations with these intermediary results. On the other hand, restricting the values accepted as input will complicate the argument types and will put the burden of input validation on our functions' callers, (although, at compile time we can get help from Idris, as we will see when we talk about auto implicits) while keeping the output pure and clean.

Languages without dependent types (like Haskell), can often only take the route described above: To wrap the result in a Maybe or Either. However, in Idris we can often refine the input types to restrict the set of accepted values, thus ruling out the possibility of failure.

Assume, as an example, we'd like to extract a value from a Vect n a at (zero-based) index k. Surely, this can succeed if and only if k is a natural number strictly smaller than the length n of the vector. Luckily, we can express this precondition in an indexed type:

data Fin : (n : Nat) -> Type where
  FZ : {0 n : Nat} -> Fin (S n)
  FS : (k : Fin n) -> Fin (S n)

Fin n is the type of natural numbers strictly smaller than n. It is defined inductively: FZ corresponds to natural number zero, which, as can be seen in its type, is strictly smaller than S n for any natural number n. FS is the inductive case: If k is strictly smaller than n (k being of type Fin n), then FS k is strictly smaller than S n.

Let's come up with some values of type Fin:

fin0_5 : Fin 5
fin0_5 = FZ

fin0_7 : Fin 7
fin0_7 = FZ

fin1_3 : Fin 3
fin1_3 = FS FZ

fin4_5 : Fin 5
fin4_5 = FS (FS (FS (FS FZ)))

Note, that there is no value of type Fin 0. We will learn in a later session, how to express "there is no value of type x" in a type.

Let us now check, whether we can use Fin to safely index into a Vect:

index : Fin n -> Vect n a -> a

Before you continue, try to implement index yourself, making use of holes if you get stuck.

index FZ     (x :: _) = x
index (FS k) (_ :: xs) = index k xs

Note, how there is no Nil case and the totality checker is still happy. That's because Nil is of type Vect 0 a, but there is no value of type Fin 0! We can verify this by adding the missing impossible clauses:

index FZ     Nil impossible
index (FS _) Nil impossible

Exercises part 2

1. Implement function update, which, given a function of type a -> a, updates the value in aVect n a at position k < n.

2. Implement function insert, which inserts a value of type a at position k <= n in a Vect n a. Note, that k is the index of the freshly inserted value, so that the following holds:

   index k (insert k v vs) = v
   

3. Implement function delete, which deletes a value from a vector at the given index.

   This is trickier than Exercises 1 and 2, as we have to properly encode in the types that the vector is getting one element shorter.

4. We can use Fin to implement safe indexing into Lists as well. Try to come up with a type and implementation for safeIndexList.

   Note: If you don't know how to start, look at the type of fromList for some inspiration. You might also need give the arguments in a different order than for index.

5. Implement function finToNat, which converts a Fin n to the corresponding natural number, and use this to declare and implement function take for splitting of the first k elements of a Vect n a with k <= n.

6. Implement function minus for subtracting a value k from a natural number n with k <= n.

7. Use minus from Exercise 6 to declare and implement function drop, for dropping the first k values from a Vect n a, with k <= n.

8. Implement function splitAt for splitting a Vect n a at position k <= n, returning the prefix and suffix of the vector wrapped in a pair.

   Hint: Use take and drop in your implementation.

Hint: Since Fin n consists of the values strictly smaller than n, Fin (S n) consists of the values smaller than or equal to n.

Note: Functions take, drop, and splitAt, while correct and provably total, are rather cumbersome to type. There is an alternative way to declare their types, as we will see in the next section.

Compile-Time Computations

module Tutorial.Dependent.Comptime

import Tutorial.Dependent.LengthIndexedLists

%default total

In the last section - especially in some of the exercises - we started more and more to use compile time computations to describe the types of our functions and values. This is a very powerful concept, as it allows us to compute output types from input types. Here's an example:

It is possible to concatenate two Lists with the (++) operator. Surely, this should also be possible for Vect. But Vect is indexed by its length, so we have to reflect in the types exactly how the lengths of the inputs affect the lengths of the output. Here's how to do this:

(++) : Vect m a -> Vect n a -> Vect (m + n) a
(++) []        ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)

Note, how we keep track of the lengths at the type-level, again ruling out certain common programming errors like inadvertently dropping some values.

We can also use type-level computations as patterns on the input types. Here is an alternative type and implementation for drop, which you implemented in the exercises by using a Fin n argument:

drop' : (m : Nat) -> Vect (m + n) a -> Vect n a
drop' 0     xs        = xs
drop' (S k) (_ :: xs) = drop' k xs

Note that changing the order from (m + n) to (n + m) in the second parameter will cause an error at the second xs:

While processing right hand side of drop'. Can't solve constraint between: plus n 0 and n.

You will learn why in the next section.

Limitations

After all the examples and exercises in this section you might have come to the conclusion that we can use arbitrary expressions in the types and Idris will happily evaluate and unify all of them for us.

I'm afraid that's not even close to the truth. The examples in this section were hand-picked because they are known to just work. The reason being, that there was always a direct link between our own pattern matches and the implementations of functions we used at compile time.

For instance, here is the implementation of addition of natural numbers:

add : Nat -> Nat -> Nat
add Z     n = n
add (S k) n = S $ add k n

As you can see, add is implemented via a pattern match on its first argument, while the second argument is never inspected. Note, how this is exactly how (++) for Vect is implemented: There, we also pattern match on the first argument, returning the second unmodified in the Nil case, and prepending the head to the result of appending the tail in the cons case. Since there is a direct correspondence between the two pattern matches, it is possible for Idris to unify 0 + n with n in the Nil case, and (S k) + n with S (k + n) in the cons case.

Here is a simple example, where Idris will not longer be convinced without some help from us:

failing "Can't solve constraint"
  reverse : Vect n a -> Vect n a
  reverse []        = []
  reverse (x :: xs) = reverse xs ++ [x]

When we type-check the above, Idris will fail with the following error message: "Can't solve constraint between: plus n 1 and S n." Here's what's going on: From the pattern match on the left hand side, Idris knows that the length of the vector is S n, for some natural number n corresponding to the length of xs. The length of the vector on the right hand side is n + 1, according to the type of (++) and the lengths of xs and [x]. Overloaded operator (+) is implemented via function Prelude.plus, that's why Idris replaces (+) with plus in the error message.

As you can see from the above, Idris can't verify on its own that 1 + n is the same thing as n + 1. It can accept some help from us, though. If we come up with a proof that the above equality holds (or - more generally - that our implementation of addition for natural numbers is commutative), we can use this proof to rewrite the types on the right hand side of reverse. Writing proofs and using rewrite will require some in-depth explanations and examples. Therefore, these things will have to wait until another chapter.

Unrestricted Implicits

In functions like replicate, we pass a natural number n as an explicit, unrestricted argument from which we infer the length of the vector to return. In some circumstances, n can be inferred from the context. For instance, in the following example it is tedious to pass n explicitly:

ex4 : Vect 3 Integer
ex4 = zipWith (*) (replicate 3 10) (replicate 3 11)

The value n is clearly derivable from the context, which can be confirmed by replacing it with underscores:

ex5 : Vect 3 Integer
ex5 = zipWith (*) (replicate _ 10) (replicate _ 11)

We therefore can implement an alternative version of replicate, where we pass n as an implicit argument of unrestricted quantity:

replicate' : {n : _} -> a -> Vect n a
replicate' = replicate n

Note how, in the implementation of replicate', we can refer to n and pass it as an explicit argument to replicate.

Deciding whether to pass potentially inferable arguments to a function implicitly or explicitly is a question of how often the arguments actually are inferable by Idris. Sometimes it might even be useful to have both versions of a function. Remember, however, that even in case of an implicit argument we can still pass the value explicitly:

ex6 : Vect ? Bool
ex6 = replicate' {n = 2} True

In the type signature above, the question mark (?) means, that Idris should try and figure out the value on its own by unification. This forces us to specify n explicitly on the right hand side of ex6.

Pattern Matching on Implicits

The implementation of replicate' makes use of function replicate, where we could pattern match on the explicit argument n. However, it is also possible to pattern match on implicit, named arguments of non-zero quantity:

replicate'' : {n : _} -> a -> Vect n a
replicate'' {n = Z}   _ = Nil
replicate'' {n = S _} v = v :: replicate'' v

Exercises part 3

1. Here is a function declaration for flattening a List of Lists:

   flattenList : List (List a) -> List a
   

   Implement flattenList and declare and implement a similar function flattenVect for flattening vectors of vectors.

2. Implement functions take' and splitAt' like in the exercises of the previous section but using the technique shown for drop'.

3. Implement function transpose for converting an m x n-matrix (represented as a Vect m (Vect n a)) to an n x m-matrix.

   Note: This might be a challenging exercise, but make sure to give it a try. As usual, make use of holes if you get stuck!

   Here is an example how this should work in action:

   Solutions.Dependent> transpose [[1,2,3],[4,5,6]]
   [[1, 4], [2, 5], [3, 6]]
   

Conclusion

• Dependent types allow us to calculate types from values. This makes it possible to encode properties of values at the type-level and verify these properties at compile time.

• Length-indexed lists (vectors) let us rule out certain implementation errors, by forcing us to be precise about the lengths of input and output vectors.

• We can use patterns in type signatures, for instance to express that the length of a vector is non-zero and therefore, the vector is non-empty.

• When creating values of a type family, the values of the indices need to be known at compile time, or they need to be passed as arguments to the function creating the values, where we can pattern match on them to figure out, which constructors to use.

• We can use Fin n, the type of natural numbers strictly smaller than n, to safely index into a vector of length n.

• Sometimes, it is convenient to pass inferable arguments as non-erased implicits, in which case we can still inspect them by pattern matching or pass them to other functions, while Idris will try and fill in the values for us.

Note, that data type Vect together with many of the functions we implemented here is available from module Data.Vect from the base library. Likewise, Fin is available from Data.Fin from base.

What's next

In the next section, it is time to learn how to write effectful programs and how to do this while still staying pure.

IO: Programming with Side Effects

So far, all our examples and exercises dealt with pure, total functions. We didn't read or write content from or to files, nor did we write any messages to the standard output. It is time to change that and learn, how we can write effectful programs in Idris.

Pure Side Effects?

module Tutorial.IO.PureSideEffects

import Data.List1
import Data.String
import Data.Vect

%default total

If we once again look at the hello world example from the introduction, it had the following type and implementation:

hello : IO ()
hello = putStrLn "Hello World!"

If you load this module in a REPL session and evaluate hello, you'll get the following:

Tutorial.IO> hello
MkIO (prim__putStr "Hello World!")

This might not be what you expected, given that we'd actually wanted the program to just print "Hello World!". In order to explain what's going on here, we need to quickly look at how evaluation at the REPL works.

When we evaluate some expression at the REPL, Idris tries to reduce it to a value until it gets stuck somewhere. In the above case, Idris gets stuck at function prim__putStr. This is a foreign function defined in the Prelude, which has to be implemented by each backend in order to be available there. At compile time (and at the REPL), Idris knows nothing about the implementations of foreign functions and therefore can't reduce foreign function calls, unless they are built into the compiler itself. But even then, values of type IO a (a being a type parameter) are typically not reduced.

It is important to understand that values of type IO a describe a program, which, when being executed, will return a value of type a, after performing arbitrary side effects along the way. For instance, putStrLn has type String -> IO (). Read this as: "putStrLn is a function, which, when given a String argument, will return a description of an effectful program with an output type of ()". (() is syntactic sugar for type Unit, the empty tuple defined at the Prelude, which has only one value called MkUnit, for which we can also use () in our code.)

Since values of type IO a are mere descriptions of effectful computations, functions returning such values or taking such values as arguments are still pure and thus referentially transparent. It is, however, not possible to extract a value of type a from a value of type IO a, that is, there is no generic function IO a -> a, as such a function would inadvertently execute the side effects when extracting the result from its argument, thus breaking referential transparency. (Actually, there is such a function called unsafePerformIO. Do not ever use it in your code unless you know what you are doing.)

Do Blocks

If you are new to pure functional programming, you might now - rightfully - mumble something about how useless it is to have descriptions of effectful programs without being able to run them. So please, hear me out. While we are not able to run values of type IO a when writing programs, that is, there is no function of type IO a -> a, we are able to chain such computations and describe more complex programs. Idris provides special syntax for this: Do blocks. Here's an example:

export
readHello : IO ()
readHello = do
  name <- getLine
  putStrLn $ "Hello " ++ name ++ "!"

Before we talk about what's going on here, let's give this a go at the REPL:

Tutorial.IO> :exec readHello
Stefan
Hello Stefan!

This is an interactive program, which will read a line from standard input (getLine), assign the result to variable name, and then use name to create a friendly greeting and write it to standard output.

Note the do keyword at the beginning of the implementation of readHello: It starts a do block, where we can chain IO computations and bind intermediary results to variables using arrows pointing to the left (<-), which can then be used in later IO actions. This concept is powerful enough to let us encapsulate arbitrary programs with side effects in a single value of type IO. Such a description can then be returned by function main, the main entry point to an Idris program, which is being executed when we run a compiled Idris binary.

The Difference between Program Description and Execution

In order to better understand the difference between describing an effectful computation and executing or running it, here is a small program:

launchMissiles : IO ()
launchMissiles = putStrLn "Boom! You're dead."

export
friendlyReadHello : IO ()
friendlyReadHello = do
  _ <- putStrLn "Please enter your name."
  readHello

actions : Vect 3 (IO ())
actions = [launchMissiles, friendlyReadHello, friendlyReadHello]

runActions : Vect (S n) (IO ()) -> IO ()
runActions (_ :: xs) = go xs
  where go : Vect k (IO ()) -> IO ()
        go []        = pure ()
        go (y :: ys) = do
          _ <- y
          go ys

readHellos : IO ()
readHellos = runActions actions

Before I explain what the code above does, please note function pure used in the implementation of runActions. It is a constrained function, about which we will learn in the next chapter. Specialized to IO, it has generic type a -> IO a: It allows us to wrap a value in an IO action. The resulting IO program will just return the wrapped value without performing any side effects. We can now look at the big picture of what's going on in readHellos.

First, we define a friendlier version of readHello: When executed, this will ask about our name explicitly. Since we will not use the result of putStrLn any further, we can use an underscore as a catch-all pattern here. Afterwards, readHello is invoked. We also define launchMissiles, which, when being executed, will lead to the destruction of planet earth.

Now, runActions is the function we use to demonstrate that describing an IO action is not the same as running it. It will drop the first action from the non-empty vector it takes as its argument and return a new IO action, which describes the execution of the remaining IO actions in sequence. If this behaves as expected, the first IO action passed to runActions should be silently dropped together with all its potential side effects.

When we execute readHellos at the REPL, we will be asked for our name twice, although actions also contains launchMissiles at the beginning. Luckily, although we described how to destroy the planet, the action was not executed, and we are (probably) still here.

From this example we learn several things:

• Values of type IO a are pure descriptions of programs, which, when being executed, perform arbitrary side effects before returning a value of type a.

• Values of type IO a can be safely returned from functions and passed around as arguments or in data structures, without the risk of them being executed.

• Values of type IO a can be safely combined in do blocks to describe new IO actions.

• An IO action will only ever get executed when it's passed to :exec at the REPL, or when it is the main function of a compiled Idris program that is being executed.

• It is not possible to ever break out of the IO context: There is no function of type IO a -> a, as such a function would need to execute its argument in order to extract the final result, and this would break referential transparency.

Combining Pure Code with IO Actions

The title of this subsection is somewhat misleading. IO actions are pure values, but what is typically meant here, is that we combine non-IO functions with effectful computations.

As a demonstration, in this section we are going to write a small program for evaluating arithmetic expressions. We are going to keep things simple and allow only expressions with a single operator and two arguments, both of which must be integers, for instance 12 + 13.

We are going to use function split from Data.String in base to tokenize arithmetic expressions. We are then trying to parse the two integer values and the operator. These operations might fail, since user input can be invalid, so we also need an error type. We could actually just use String, but I consider it to be good practice to use custom sum types for erroneous conditions.

public export
data Error : Type where
  NotAnInteger    : (value : String) -> Error
  UnknownOperator : (value : String) -> Error
  ParseError      : (input : String) -> Error

dispError : Error -> String
dispError (NotAnInteger v)    = "Not an integer: " ++ v ++ "."
dispError (UnknownOperator v) = "Unknown operator: " ++ v ++ "."
dispError (ParseError v)      = "Invalid expression: " ++ v ++ "."

In order to parse integer literals, we use function parseInteger from Data.String:

export
readInteger : String -> Either Error Integer
readInteger s = maybe (Left $ NotAnInteger s) Right $ parseInteger s

Likewise, we declare and implement a function for parsing arithmetic operators:

export
readOperator : String -> Either Error (Integer -> Integer -> Integer)
readOperator "+" = Right (+)
readOperator "*" = Right (*)
readOperator s   = Left (UnknownOperator s)

We are now ready to parse and evaluate simple arithmetic expressions. This consists of several steps (splitting the input string, parsing each literal), each of which can fail. Later, when we learn about monads, we will see that do blocks can be used in such occasions just as well. However, in this case we can use an alternative syntactic convenience: Pattern matching in let bindings. Here is the code:

eval : String -> Either Error Integer
eval s =
  let [x,y,z]  := forget $ split isSpace s | _ => Left (ParseError s)
      Right v1 := readInteger x  | Left e => Left e
      Right op := readOperator y | Left e => Left e
      Right v2 := readInteger z  | Left e => Left e
   in Right $ op v1 v2

Let's break this down a bit. On the first line, we split the input string at all whitespace occurrences. Since split returns a List1 (a type for non-empty lists exported from Data.List1 in base) but pattern matching on List is more convenient, we convert the result using Data.List1.forget. Note, how we use a pattern match on the left hand side of the assignment operator :=. This is a partial pattern match (partial meaning, that it doesn't cover all possible cases), therefore we have to deal with the other possibilities as well, which is done after the vertical line. This can be read as follows: "If the pattern match on the left hand side is successful, and we get a list of exactly three tokens, continue with the let expression, otherwise return a ParseError in a Left immediately".

The other three lines behave exactly the same: Each has a partial pattern match on the left hand side with instructions what to return in case of invalid input after the vertical bar. We will later see, that this syntax is also available in do blocks.

Note, how all of the functionality implemented so far is pure, that is, it does not describe computations with side effects. (One could argue that already the possibility of failure is an observable effect, but even then, the code above is still referentially transparent, can be easily tested at the REPL, and evaluated at compile time, which is the important thing here.)

Finally, we can wrap this functionality in an IO action, which reads a string from standard input and tries to evaluate the arithmetic expression:

exprProg : IO ()
exprProg = do
  s <- getLine
  case eval s of
    Left err  => do
      putStrLn "An error occured:"
      putStrLn (dispError err)
    Right res => putStrLn (s ++ " = " ++ show res)

Note, how in exprProg we were forced to deal with the possibility of failure and handle both constructors of Either differently in order to print a result. Note also, that do blocks are ordinary expressions, and we can, for instance, start a new do block on the right hand side of a case expression.

Exercises part 1

In these exercises, you are going to implement some small command-line applications. Some of these will potentially run forever, as they will only stop when the user enters a keyword for quitting the application. Such programs are no longer provably total. If you added the %default total pragma at the top of your source file, you'll need to annotate these functions with covering, meaning that you covered all cases in all pattern matches but your program might still loop due to unrestricted recursion.

1. Implement function rep, which will read a line of input from the terminal, evaluate it using the given function, and print the result to standard output:

   rep : (String -> String) -> IO ()
   

2. Implement function repl, which behaves just like rep but will repeat itself forever (or until being forcefully terminated):

   covering
   repl : (String -> String) -> IO ()
   

3. Implement function replTill, which behaves just like repl but will only continue looping if the given function returns a Right. If it returns a Left, replTill should print the final message wrapped in the Left and then stop.

   covering
   replTill : (String -> Either String String) -> IO ()
   

4. Write a program, which reads arithmetic expressions from standard input, evaluates them using eval, and prints the result to standard output. The program should loop until users stops it by entering "done", in which case the program should terminate with a friendly greeting. Use replTill in your implementation.

5. Implement function replWith, which behaves just like repl but uses some internal state to accumulate values. At each iteration (including the very first one!), the current state should be printed to standard output using function dispState, and the next state should be computed using function next. The loop should terminate in case of a Left and print a final message using dispResult:

   covering
   replWith :  (state      : s)
            -> (next       : s -> String -> Either res s)
            -> (dispState  : s -> String)
            -> (dispResult : res -> s -> String)
            -> IO ()
   

6. Use replWith from Exercise 5 to write a program for reading natural numbers from standard input and printing the accumulated sum of these numbers. The program should terminate in case of invalid input and if a user enters "done".

Do Blocks, Desugared

module Tutorial.IO.DoUnsugared

import Data.List1
import Data.String
import Data.Vect

import Tutorial.IO.PureSideEffects

%default total

Here's an important piece of information: There is nothing special about do blocks. They are just syntactic sugar, which is converted to a sequence of operator applications. With syntactic sugar, we mean syntax in a programming language that makes it easier to express certain things in that language without making the language itself any more powerful or expressive. Here, it means you could write all the IO programs without using do notation, but the code you'll write will sometimes be harder to read, so do blocks provide nicer syntax for these occasions.

Consider the following example program:

sugared1 : IO ()
sugared1 = do
  str1 <- getLine
  str2 <- getLine
  str3 <- getLine
  putStrLn (str1 ++ str2 ++ str3)