Gentle Introduction to Dependent

Types with Idris

Boro Sitnikovski
This book is for sale at http://leanpub.com/gidti

This version was published on 2022-01-03

This is a Leanpub book. Leanpub empowers authors and publishers with the Lean
Publishing process. Lean Publishing is the act of publishing an in-progress ebook
using lightweight tools and many iterations to get reader feedback, pivot until you
have the right book and build traction once you do.

© 2018 - 2022 Boro Sitnikovski

dedicated to my wife Dijana, and our kids
Contents

Preface and acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

1. Formal systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.1. MU puzzle example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

4. Programming in Idris . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
4.1. Basic syntax and definitions . . . . . . . . . . . . . . . . . . . . . . . . . . 8
4.1.1. Defining functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
4.1.2. Defining and inferring types . . . . . . . . . . . . . . . . . . . . . . 10
4.1.3. Anonymous lambda functions . . . . . . . . . . . . . . . . . . . . 15
4.1.4. Recursive functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
4.1.5. Recursive data types . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
4.1.6. Total and partial functions . . . . . . . . . . . . . . . . . . . . . . . 22
4.1.7. Higher-order functions . . . . . . . . . . . . . . . . . . . . . . . . . 23
4.1.8. Dependent types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
4.1.9. Implicit parameters . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4.1.10. Pattern matching expressions . . . . . . . . . . . . . . . . . . . . 29
4.1.11. Interfaces and implementations . . . . . . . . . . . . . . . . . . . 30
4.2. Curry-Howard isomorphism . . . . . . . . . . . . . . . . . . . . . . . . . 31
4.3. Quantitative Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

Further reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

About the author . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

Preface and acknowledgments
This book aims to be accessible to novices that have no prior experience beyond
high school mathematics. Thus, this book is designed to be self-contained. No
programming experience is assumed, however having some kind of programming
experience with the functional programming paradigm could make things easier to
grasp in the beginning. After you finish reading the book I recommend that you
check the “Further reading” chapter in case you are interested in diving deeper into
some of the topics discussed.
I was always curious to understand how things work. As a result, I became very
interested in mathematics while I was in high school. One of the reasons for writing
this book is that I could not find a book that explained how things work, so I had to
do a lot of research on the internet through white-papers, forums, and example code
in order to come up with a complete picture of what dependent types are and what
they are good for.
I will consider this book successful if it provides you with some additional knowledge.
I tried to write this book so that the definitions and examples provided in it show how
different pieces of the puzzle are connected to each other.
Feel free to contact me at buritomath@gmail.com for any questions you might have,
and I will do my best to answer. You can also access my blog at bor0.wordpress.com
to check out some of my latest work.
Book reviewers:

1. Nathan Bloomfield did a Ph.D. in algebra at the University of Arkansas and

taught mathematics before joining Automattic, Inc. as a programmer. He enjoys
witnessing the Intuitionist renaissance and likes how the boring parts of abstract
algebra transform into really interesting computer science. Nathan usually feels
a little out of his depth and prefers it that way.
2. Vlad Riscutia is a software engineer at Microsoft working on Office. He is
interested in programming languages and type systems, and how these can best
be leveraged to write correct code.
Preface and acknowledgments 2

3. Marin Nikolovski is working at Massive Entertainment | A Ubisoft Studio as a

Senior Web Developer on UPlay PC. He has over 10 years of experience with
designing, developing and testing software across a variety of platforms. He
takes pride in coding to consistently high standards and constantly tries to keep
up the pace with the latest developments in the IT industry.
4. Neil Mitchell is a Haskell programmer with a Ph.D. in Computer Science from
York University, where he worked on making functional programs shorter,
faster and safer. Neil is the author of popular Haskell tools such as Hoogle,
HLint, and Ghcid - all designed to help developers write good code quickly.
More recently Neil has been researching build systems with publications at
ICFP and the Haskell Symposium, and a practical system based on those ideas
named Shake.

Thanks to:

1. Irena Jazeva for the book cover design

2. The Haskell community (#haskell@freenode)
3. The Idris community (#idris@freenode)
4. The Coq community (#coq@freenode)

Thanks to my family, coworkers, and friends for all the support they give to me.
Finally, thank you for purchasing this book! I hope that you will learn new techniques
in reading this book and that it will spark up some more interest in logic, dependent
types, and type theory.
Introduction
Writing correct code in software engineering is a complex and expensive task, and too
often our written code produces inaccurate or unexpected results. There are several
ways to deal with this problem. In practice, the most common approach is to write
tests, which means that we are writing more code to test our original code. However,
these tests can only ever detect problems in specific cases. As Edsger Dijkstra noted,
“testing shows the presence, not the absence of bugs”. A less common approach is to
find a proof of correctness for our code. A software proof of correctness is a logical
proof that the software is functioning according to given specifications. With valid
proofs, we can cover all possible cases and be more confident that the code does
exactly what it is intended to do.
Idris is a general-purpose functional¹ programming language that supports depen-
dent types. The features of Idris are influenced by Haskell, another general-purpose
functional programming language. Thus, Idris shares many features with Haskell,
especially in the part of syntax and types, where Idris has a more advanced type
system. There are several other programming languages that support dependent
types², however, I chose Idris for its readable syntax.
The first version of Idris was released in 2009. It is developed by The Idris Community
and led by Dr. Edwin Brady. Seen as a programming language, it is a functional
programming language implemented with dependent types. Seen as a logical system,
it implements intuitionistic type theory, which we will cover later. Finally, we will
show how these two views relate to each other in section 4.2.
Idris allows us to express mathematical statements. By mechanically examining these
statements, it helps us find a formal proof of a program’s formal specification.
To fully understand how proofs in Idris work we will start with the foundations by
defining: formal systems, classical mathematical logic, lambda calculus, intuitionistic
logic, and type theory (which is a more “up-to-date” version of classical mathematical
logic).
¹The core concept of functional programming languages is a mathematical function.
²Several other languages with dependent types support are Coq, Agda, Lean.
1. Formal systems
Before we can construct proofs of correctness for software we need to understand
what a proof is and what it means for a proof to be valid. This is the role of formal
systems. The purpose of formal systems is to let us reason about reasoning – to
manipulate logical proofs in terms of their form, rather than their content. This level
of abstraction makes formal systems powerful tools.

Definition 1
A formal system is a model of abstract reasoning. A formal system consists
of:

1. A formal language that contains:

1. A finite set of symbols, which can be combined into finite strings
called formulas
2. A grammar, which is a set of rules that tells us which formulas
are “well-formed”
2. A set of axioms, that is, formulas we accept as “valid” without
justification
3. A set of inference rules that tell us how we can derive new valid
formulas from old ones

Inside a given formal system the grammar determines which formulas are syntac-
tically sensible, while the inference rules govern which formulas are semantically
sensible. The difference between these two is important. For example, thinking of
the English language as a (very complicated!) formal system, the sentence “Colorless
green ideas sleep furiously” is syntactically valid (since different parts of speech are
used in the right places), but is semantically nonsense.
After a formal system is defined, other formal systems can extend it. For example,
set theory is based on first-order logic, which is based on propositional logic which
represents a formal system. We’ll discuss this theory briefly in the next chapter.
1. Formal systems 5

Definition 2
For a given formal system, the system is incomplete if there are statements
that are true but which cannot be proved to be true inside that system.
Conversely, the system is complete if all true statements can be proved.

The statement “This statement is not provable” can either be true or false. In the
case it is true, then it is not provable. Alternatively, in the case it is false then it is
provable, but we’re trying to prove something false. Thus the system is incomplete
because some truths are unprovable.

Definition 3
For a given formal system, the system is inconsistent if there is a theorem
in that system that is contradictory. Conversely, the system is consistent
if there are no contradictory theorems.

A simple example is the statement “This statement is false”. This statement is true if
and only if³ it is false, and therefore it is neither true nor false.
In general, we often put our focus on which parts of mathematics can be formalized
in concrete formal systems, rather than trying to find a theory in which all of
mathematics can be developed. The reason for that is Gödel’s incompleteness
theorem. This theorem states that there doesn’t exist⁴ a formal system that is both
complete and consistent. As a result, it is better to reason about a formal system
outside of the system (at the metalanguage level), since the object level (rules within
the system) can be limiting. As the famous saying goes to “think outside of the box”,
and similarly to how we sometimes do meta-thinking to improve ourselves.
In conclusion, formal systems are our attempt to abstract models, whenever we
reverse engineer nature in an attempt to understand it better. They may be imperfect
but are nevertheless useful tools for reasoning.
³The word iff is an abbreviation for “If and only if” and means that two statements are logically equivalent.
⁴Note that this theorem only holds for systems that allow expressing arithmetic of natural numbers (e.g. Peano,
set theory, but first-order logic also has some paradoxes if we allow self-referential statements). This is so because the
incompleteness theorem relies on the Gödel numbering concept, which allows a formal system to reason about itself by
using symbols in the system to map expressions in that same system. For example, 0 is mapped to 1, S is 2, = is 3, so
0 = S0 ⇐⇒ (1, 3, 2, 1). Using this we can express statements about the system within the system - self-referential
statements. We will look into these systems in the next chapter.
1. Formal systems 6

1.1. MU puzzle example

The MU puzzle is a formal system that we’ll have a look at as an example.

Definition 4
We’re given a starting string MI, combined with a few inference rules, or
transformation rules:
No. Rule Description Example
1 xI → xIU Append U at a string ending in MI to MIU
I
2 Mx → Mxx Double the string after M MIU to MIUIU
3 xIIIy → xUy Replace III inside a string MUIIIU to MUUU
with U
4 xUUy → xy Remove UU from inside a string MUUU to MU

In the inference rules the symbols M, I, and U are part of the system, while x is a
variable that stands for any symbol(s). For example, MI matches rule 2 for x = I, and
it can also match rule 1 for x = M. Another example is MII that matches rule 2 for x
= II and rule 1 for x = MI.

We will show (or prove) how we can get from MI to MIIU using the inference rules:

1. MI (axiom)
2. MII (rule 2, x = I)
3. MIIII (rule 2, x = II)
4. MIIIIIIII (rule 2, x = IIII)
5. MUIIIII (rule 3, x = M, y = IIIII)
6. MUUII (rule 3, x = MU, y = II)
7. MII (rule 4, x = M, y = II)
8. MIIU (rule 1, x = MI)

We can represent the formal description of this system as follows:

1. Formal language
1. Formal systems 7

1. Set of symbols is {M, I, U }

2. A string is well-formed if the first letter is M and there are no other M letters.
Examples: M, MIUIU, MUUUIII
2. MI is the starting string, i.e. axiom
3. The rules of inference are defined in Definition 4

Can we get from MI to MU with this system?

To answer this, we will use an invariant⁵ with mathematical induction to
prove our claim.

Note that, to be able to apply rule 3, we need to have the number of subsequent I’s
to be divisible by 3. Let’s have our invariant say that “There is no sequence of I’s in
the string that with length divisible by 3”:

1. For the starting axiom, we have one I. Invariant OK.

2. Applying rule 2 will be doubling the number of I’s, so we can have: I, II, IIII,
IIIIIII (in particular, 2n I’s). Invariant OK.
3. Applying rule 3 will be reducing the number of I’s by 3. But note that 2n − 3 is
still not divisible by 3⁶. Invariant OK.

We’ve shown that with the starting axiom MI it is not possible to get to MU because no
sequence of steps can turn a string with one I into a string with no Is. But if we look
carefully, we’ve used a different formal system to reason about MU (i.e. divisibility by
3, which is not part of the MU system). This is because the puzzle cannot be solved in
its own system. Otherwise, an algorithm would keep trying different inference rules
of MU indefinitely (not knowing that MU is impossible).
Every useful formal system has this limitation. As we’ve seen, Gödel’s theorem
shows that there’s no formal system that can contain all possible truths, because
it cannot prove some truths about its own structure. Thus, having experience with
different formal systems and combining them as needed can be useful.
⁵An invariant is a property that holds whenever we apply any of the inference rules.
⁶After having introduced ourselves to proofs, you will be given an exercise to prove this fact.
4. Programming in Idris
In this chapter, we will introduce Idris’ syntax, by defining functions and types.
Depending on what level of abstraction we are working on, types and proofs can
give us a kind of security based on some truths we take for granted (axioms). In fact,
this is how we develop code on a daily basis, as software engineers. We have a list of
axioms, for example, a foreach loop in a programming language, and starting from
it we build abstractions, expecting this foreach to behave in a certain way. However,
this security is not always easy to achieve. For example, consider a scenario where
we have a button that is supposed to download a PDF document. In order to prove
that it works as expected, we must first pick the abstraction level we will be working
on, and then proceed by defining software requirements (what is a PDF, what is a
download). So, we first have to define our specifications, and then we can proceed
with proving correctness.
Idris, even though a research language, still has its own uses. It is a Turing complete
language, which means that it has the same expressive power as other programming
languages, for example, Java, or C++.
To start with, Idris can be downloaded and installed via www.idris-lang.org/download.

4.1. Basic syntax and definitions

There are two working modes in Idris: REPL (read-evaluate-print-loop) i.e. interac-
tive mode, and compilation of code. We will mostly work in the interactive mode in
this chapter.
You can copy any of the example codes to some file, say, test.idr and launch Idris
in REPL mode by writing idris test.idr. This will allow you to interact with Idris
given the definitions in the file. If you change the contents of the file, that is, update
the definitions, you can use the command :r while in REPL mode to reload the
definitions.
 4. Programming in Idris 9

4.1.1. Defining functions

Let’s begin by defining a simple function.

1 add_1 : Nat -> Nat

2 add_1 x = x + 1

With the code above we’re defining a function f (x) = x+1, where x is natural number
and f (x) (the result) is also a natural number⁷. The first line add_1 : Nat -> Nat is
called a type signature, and specifies the type of our function; in this case a function
that takes a natural number and returns a natural number. The second line add_1 x
= x + 1 is the definition of the function, which states that if add_1 is called with a
number x, the result would be x + 1. As can be seen by the example, every function
has to be provided a type definition. We can interact as follows in the REPL mode:

1 Idris> add_1 5
2 6 : Nat

Idris responds to us that as a result, we get 6, which is of type Nat. Constants are
defined similarly; we can think of them as functions with no arguments.

1 number_1 : Nat
2 number_1 = 1

As in Haskell, we can use pattern matching. What happens during this phase is Idris
does a check (match) against the definitions of the function and uses the definition
of the function that matches the value.

⁷It is worth noting that in Haskell we have types and kinds. Kinds are similar to types, that is, they are defined as
one level above types in simply-typed lambda calculus. For example, types such as Nat have a kind Nat :: * and it’s
stated that Nat is of kind *. Types such as Nat -> Nat have a kind of * -> *. Since in Idris the types are first-class citizens,
there is no distinction between types and kinds.
 4. Programming in Idris 10

1 is_it_zero : Nat -> Bool

2 is_it_zero Z = True
3 is_it_zero x = False

We’ve just defined a function that accepts a natural number and returns a boolean
value (True or False). On the first line, we specify its type. On the second line, we
pattern match against the input Z and return True in that case. On the third line,
we pattern match against the input x (which is all remaining inputs except Z). In
this case, we return False. The code above, depending on the input, will branch the
computation to the corresponding definition. Note that Z corresponds to 0 for the
type Nat.

Exercise 1
Write a function my_identity which accepts a natural number and returns
the same number.

Exercise 2
Write a function five_if_zero which accepts a natural number and returns
5 when called with an argument of 0, otherwise returns the same number.
For example, five_if_zero 0 should return 5. five_if_zero 123 should
return 123.

4.1.2. Defining and inferring types

In Idris, types are first-class citizens. This means that types can be computed and
passed to other functions. We define new types by using the keyword data. All
concrete types (like Nat) and type constructors (like List) begin with an uppercase
letter, while lowercase letters are reserved for polymorphic types⁸. There are a couple
of ways to define types. One example is by using the so-called Haskell98 syntax:

⁸A polymorphic type can accept additional types as arguments, which are either defined by the programmer or
primitive ones.
 4. Programming in Idris 11

1 data A a b = A_inst a b

This will create a polymorphic type that accepts two type arguments, a and b. Valid
constructed types are A Nat Bool, A Nat Nat, etc. A is a type constructor (a function
that returns a type) and A_inst⁹ is a value constructor (a function that returns a value
of type A a b).

1 Idris> A_inst True True

2 A_inst True True : A Bool Bool
3 Idris> A_inst Z True
4 A_inst 0 True : A Nat Bool

Note how the type changes depending on what values we pass to the constructor,
due to polymorphism.
Here’s an equivalent definition by using the GADT (Generalized Algebraic Data Types)
syntax:

1 data A : Type -> Type -> Type where

2 A_inst : a -> b -> A a b

This is equivalent to the following definition, where we define an empty data

structure along with an axiom for the value constructor:

1 data A : Type -> Type -> Type

2 postulate A_inst : a -> b -> A a b

With the postulate keyword we can define axioms which are functions that satisfy
the types without giving an actual argument for construction. With the command :t
we can check the type of an expression, so as a result, we get:

⁹The value and type constructors must be named differently since types and values are at the same level in Idris.
 4. Programming in Idris 12

1 Idris> :t A
2 A : Type -> Type -> Type
3 Idris> :t A_inst
4 A_inst : a -> b -> A a b

That is, we show the type definitions for both the newly-defined type and its value
constructor. Note how we created a product type here. Idris has a built-in¹⁰ notion of
pairs, which is a data type that can be defined in terms of products. For example, (1,
2) is one pair. We can also define tuples with (1, "Hi", True), which is equivalent
to (1, ("Hi", True)), i.e. a pair where the first element is a number, and the second
element is a pair. Note that the types (a, b) -> c (curried) and a -> b -> c
(uncurried) represent the same thing.
Analogously, if we want to create a sum type, we could do the following:

1 data B a b = B_inst_left a | B_inst_right b

This is equivalent to:

1 data B : Type -> Type -> Type where

2 B_inst_left : a -> B a b
3 B_inst_right : b -> B a b

With either of these definitions in scope, we get:

1 Idris> :t B
2 B : Type -> Type -> Type
3 Idris> :t B_inst_left
4 B_inst_left : a -> B a b
5 Idris> :t B_inst_right
6 B_inst_right : b -> B a b

The functions B_inst_left and B_inst_right are also known as introduction rules.
For extracting values from data types such as B a b, also known as elimination rules,
we can use pattern matching¹¹. As an example, to extract a from B a b, we can use
¹⁰By built-in, we usually mean it’s part of Idris’ library. We can always implement it ourselves if we need to.
¹¹Although product and sum types are very general, due to polymorphism, we can say something very specific about
the structure of their values. For instance, suppose we’ve defined a type like so: data C a b c = C_left a | C_right
(b,c). A value of type C can only come into existence in one of two ways: as a value of the form C_left x for a value x
: a, or as a value of the form C_right (y,z) for values y : b and z : c.
 4. Programming in Idris 13

the following function:

1 f : B a b -> a
2 f (B_inst_left a) = a

Note how we used the data type at the function type level and the value constructor
in the function definition to pattern match against.
Natural numbers can be defined as data Nat = Z | S Nat, where we either have a
zero or a successor of a natural number. Note how this type is not polymorphic (it
doesn’t accept any variables after the type name). Natural numbers are built-in as a
type in Idris.
We can use the operator == to compare two numbers. Note that == is still a function,
but it’s an infix one. This means that unlike other functions that we define which are
prefix, i.e. start at the beginning of the expression, == needs to appear between the
parameters. For example:

1 Idris> 1 == 1
2 True : Bool

Idris has several built-in primitive types, including: Bool, Char, List, String (list of
characters), Integer, etc. The only value constructors for the type Bool are True and
False. The difference between a Nat and an Integer is that Integer can also contain
negative values. Here are some examples of interacting with these types:

1 Idris> "Test"
2 "Test" : String
3 Idris> '!'
4 '!' : Char
5 Idris> 1
6 1 : Integer
7 Idris> '1'
8 '1' : Char
9 Idris> [1, 2, 3]
10 [1, 2, 3] : List Integer

By using the :doc command, we can get detailed information about a data type:
 4. Programming in Idris 14

1 Idris> :doc Nat

2 Data type Prelude.Nat.Nat : Type
3 Natural numbers: unbounded, unsigned integers which can be pattern
4 matched.
5
6 Constructors:
7 Z : Nat
8 Zero
9
10 S : Nat -> Nat
11 Successor

In order to make Idris infer the necessary type of the function that needs to be built,
we can take advantage of holes. A hole is any variable that starts with a question
mark. For example, if we have the following definition:

1 test : Bool -> Bool

2 test p = ?hole1

We can now ask Idris to tell us the type of hole1, that is, with :t hole1 we can
see that Idris inferred that the specific result is expected to be of type Bool. This is
useful because it allows us to write programs incrementally (piece by piece) instead
of constructing the program all at once.

Exercise 3
Define your own custom type. One example is data Person = PersonInst
String Nat, where String represents the Person’s name and Nat represents
the Person’s age. Use the constructor to generate some objects of that type.
Afterward, use :t to check the types of the type and value constructors.

Exercise 4
Come up with a function that works with your custom type (for example,
it extracts some value) by pattern matching against its value constructor(s).
 4. Programming in Idris 15

Exercise 5
Repeat Exercise 4 and use holes to check the types of the expressions used
in your function definition.

4.1.3. Anonymous lambda functions

With the syntax let X in Y we’re defining a set of variables X which are only visible
in the body of Y. As an example, here is one way to use this syntax:

1 Idris> let f = 1 in f
2 1 : Integer

Alternatively, the REPL has a command :let that allows us to set a variable without
evaluating it right away, that can be used at a later point:

1 Idris> :let f = 1
2 Idris> f
3 1 : Integer

What’s the difference between let and :let?

let is an extension of the lambda calculus syntax. The expression let x =
y in e is equivalent to (\x . e) y. It is useful since it makes it easy to
shorten a lambda expression by factoring out common subexpressions.
:let is different in that it is just used to bind new names at the top level of
an interactive Idris session.

Lambda (anonymous) functions are defined with the syntax \a, b, ..., n => ....
For example:
 4. Programming in Idris 16

1 Idris> let addThree = (\x, y, z => x + y + z) in addThree 1 2 3

2 6 : Integer

With the example above, we defined a function addThree that accepts three param-
eters and as a result it sums them. However, if we do not pass all parameters to a
function, it will result in:

1 Idris> let addThree = (\x, y, z => x + y + z) in addThree 1 2

2 \z => prim__addBigInt 3 z : Integer -> Integer

We can see (from the type) that as a result, we get another function.

Definition 1
Currying is a concept that allows us to evaluate a function with multiple
parameters as a sequence of functions, each having a single parameter.

Function application in Idris is left-associative (just like in lambda calculus), which

means that if we try to evaluate addThree 1 2 3, then it will be evaluated as
(((addThree 1) 2) 3). A combination of left-associative functions and currying
(i.e. partial evaluation of function) is what allows us to write addThree 1 2 3, which
is much more readable.
Arrow types are right-associative (just like in lambda calculus), which means that
addThree 1 : a -> a -> a is equivalent to addThree 1 : (a -> (a -> a)). If we had
written a type of (a -> a) -> a instead, then this function would accept as its first
parameter a function that takes an a and returns an a, and then the original function
also returns an a. This is how we can define higher-order functions which we will
discuss later. Note how a starts with a lowercase letter, thus it is a polymorphic type.
The if...then...else syntax is defined as follows:
 4. Programming in Idris 17

1 Idris> if 1 == 1 then 'a' else 'b'

2 'a' : Char
3 Idris> if 2 == 1 then 'a' else 'b'
4 'b' : Char

Exercise 6
Write a lambda function that returns True if the parameter passed to it is
42 and False otherwise.

4.1.4. Recursive functions

By Definition 19 of chapter 2, recursive functions are those functions that refer to
themselves. One example is the function even : Nat -> Bool, a function that checks
if a natural number is even or not. It can be defined as follows:

1 even : Nat -> Bool

2 even Z = True
3 even (S k) = not (even k)

The definition states that 0 is an even number, and that n + 1 is even or not depending
on the parity (evenness) of n. As a result, we get:

1 Idris> even 3
2 False : Bool
3 Idris> even 4
4 True : Bool
5 Idris> even 5
6 False : Bool

The way even 5 unfolds in Idris is as follows:

 4. Programming in Idris 18

1 even 5 =
2 not (even 4) =
3 not (not (even 3)) =
4 not (not (not (even 2))) =
5 not (not (not (not (even 1)))) =
6 not (not (not (not (not (even 0))))) =
7 not (not (not (not (not True)))) =
8 not (not (not (not False))) =
9 not (not (not True)) =
10 not (not False) =
11 not True =
12 False

We see how this exhibits a recursive behavior since the recursive cases were reduced
to the base case in an attempt to get a result. With this example, we can see the power
of recursion and how it allows us to process values in a repeating manner.
A recursive function can generate an iterative or a recursive process:

1. An iterative process¹² (tail recursion) is a process where the return value at any
point in computation is captured completely by its parameters
2. A recursive one, in contrast, is one where the return value is not captured
at any point in computation by the parameters, and so it relies on postponed
evaluations

In the example above, even generates a recursive process since it needs to go down
to the base case, and then build its way back up to do the calculations that were
postponed. Alternatively, we can rewrite even so that it captures the return value by
introducing another variable, as such:

¹²The key idea is not that a tail-recursive function is an iterative loop, but that a smart enough compiler can pretend
that it is and evaluate it using constant function stack space.
 4. Programming in Idris 19

1 even : Nat -> Bool -> Bool

2 even Z t = t
3 even (S k) t = even k (not t)

In this case, we can refer to the return value of the function (second parameter) at
any point in the computation. As a consequence, this function generates an iterative
process, since the results are captured in the parameters. Note how we brought down
the base case to refer to the parameter, instead of a constant True. Here is how Idris
evaluates even 5 True:

1 even 5 True =
2 even 4 False =
3 even 3 True =
4 even 2 False =
5 even 1 True =
6 even 0 False =
7 False

To conclude, iterative processes take fewer calculation steps and are usually more
performant than recursive processes. Recursive functions combined with pattern
matching are one of the most powerful tools in Idris since they allow for computation.
They are also useful for proving mathematical theorems with induction, as we will
see in the examples later.

Exercise 7
{
1, if n = 0
Factorial is defined as: f act(n) =
n · f act(n − 1), otherwise

Unfold the evaluation of f act(5) on paper, and then implement it in Idris

and confirm that Idris also computes the same value.
Hint: The type is fact : Nat -> Nat and you should pattern match against
Z (Nat value constructor for 0) and (S n) (successor).
 4. Programming in Idris 20

Exercise 8
Re-write the factorial function to generate an iterative process.
Hint: The type is fact_iter : Nat -> Nat -> Nat and you should
pattern match against Z acc (number zero, and accumulator) and (S n)
acc (successor, and accumulator).

4.1.5. Recursive data types

We can think of type constructors as functions at the type level. Taking the concept
of recursion to this context yields recursive types.

Definition 2
A recursive data type is a data type where some of its constructors have a
reference to the same data type.

We will start by defining a recursive data type, which is a data type that in the
constructor refers to itself. In fact, earlier in this book we already gave a recursive
definition - Nat. As a motivating example, we will try to define the representation of
lists. For this data type, we’ll use a combination of sum and product types. A list is
defined as either End (end of the list) or Cons (construct), which is a value appended
to another MyList:

1 data MyList a = Cons a (MyList a) | End

This means that the type MyList has two constructors, End and Cons. If it’s End, then
it’s the end of the list (and does not accept any more values). However, if it’s Cons,
then we need to append another value (e.g. Cons 3), but afterward, we have to specify
another value of type MyList a (which can be End or another Cons). This definition
allows us to define a list. As an example, this is how we would represent (1, 2) using
our Cons End representation:
 4. Programming in Idris 21

1 Idris> :t Cons 1 (Cons 2 End)

2 Cons 1 (Cons 2 End) : MyList Integer
3 Idris> :t Cons 'a' (Cons 'b' End)
4 Cons 'a' (Cons 'b' End) : MyList Char

Note how Idris automatically infers the polymorphic type to MyList Integer and
MyList Char. In particular, these lists are homogeneous; all the items in a MyList a
must have type a.
Here is one way of implementing the concatenation function, which given two lists,
should produce a list with the elements appended:

1 add' : MyList a -> MyList a -> MyList a

2 add' End ys = ys
3 add' (Cons x xs) ys = Cons x (add' xs ys)

The first line of the code says that add' is a function that accepts two polymorphic
lists (MyList Nat, MyList Char, etc), and produces the same list as a result. The
second line of the code pattern matches against the first list and when it’s empty we
just return the second list. The third line of the code also pattern matches against the
first list, but this time it covers the Cons case. So whenever there is a Cons in the first
list, as a result, we return this element Cons x appended recursively to add' xs ys,
where xs is the remainder of the first list and ys is the second list. Example usage:

1 Idris> add' (Cons 1 (Cons 2 (Cons 3 End))) (Cons 4 End)

2 Cons 1 (Cons 2 (Cons 3 (Cons 4 End))) : MyList Integer

Exercise 9
Unfold add' (Cons 1 (Cons 2 (Cons 3 End))) (Cons 4 End) on paper to
get a better understanding of how this definition appends two lists.

Exercise 10
Come up with a definition for length', which should return the number of
elements, given a list.
Hint: The type is length' : MyList a -> Nat
4. Programming in Idris 22

Exercise 11
Come up with a definition for even_members, which should return a new
list with even natural numbers only.
Hint: The type is even_members : MyList Nat -> MyList Nat. You can
re-use the definition of even we’ve discussed earlier.

Exercise 12
Come up with a definition for sum', which should return a number that
will be the sum of all elements in a list of natural numbers.
Hint: The type is sum' : MyList Nat -> Nat.

4.1.6. Total and partial functions

Definition 3
A total function is a function that terminates (or returns a value) for all
possible inputs.

A partial function is the opposite of a total function. If a function is total, its type
can be understood as a precise description of what that function can do. Idris
differentiates total from partial functions but allows defining both¹³. As an example,
if we assume that we have a function that returns a String, then:

1. If it’s total, it will return a String in finite time

2. If it’s partial, then unless it crashes or enters in an infinite loop, it will return a
String

In Idris, to define partial/total functions we just put the keyword partial/total in

front of the function definition. For example, for the following program we define
two functions test and test2, a partial and a total one respectively:
¹³Partial (non-terminating) functions are what make Idris Turing complete.
 4. Programming in Idris 23

1 partial
2 test : Nat -> String
3 test Z = "Hi"
4
5 total
6 test2 : Nat -> String
7 test2 Z = "Hi"
8 test2 _ = "Hello"

If we try to interact with these functions, we get the following results:

1 Idris> test 0
2 "Hi" : String
3 Idris> test 1
4 test 1 : String
5 Idris> test2 0
6 "Hi" : String
7 Idris> test2 1
8 "Hello" : String

We can note that the evaluation of test 1 does not produce a computed value as
a result. Note that at compile-time, Idris will evaluate the types only for total
functions.

Exercise 13
Try to define a function to be total, and at the same time make sure you
are not covering all input cases. Note what errors will Idris return in this
case.

4.1.7. Higher-order functions

Definition 4
A higher-order function is a function that takes one or more functions as
parameters or returns a function as a result.
 4. Programming in Idris 24

There are three built-in higher-order functions that are generally useful: map, filter,
fold (left and right). Here’s the description of each:

1. map is a function that takes as input a function with a single parameter and a
list and returns a list where all members of the list have this function applied
to them
2. filter is a function that takes as input a function (predicate) with a single
parameter (that returns a Bool) and a list and only returns those members in
the list whose predicate evaluates to True
3. fold is a function that takes as input a combining function that accepts two
parameters (current value and accumulator), an initial value and a list and
returns a value combined with this function. There are two types of folds, a
left and a right one, which combines from the left and the right respectively

As an example usage:

1 Idris> map (\x => x + 1) [1, 2, 3]

2 [2, 3, 4] : List Integer
3 Idris> filter (\x => x > 1) [1, 2, 3]
4 [2, 3] : List Integer
5 Idris> foldl (\x, y => x + y) 0 [1, 2, 3]
6 6 : Integer
7 Idris> foldr (\x, y => x + y) 0 [1, 2, 3]
8 6 : Integer

We can actually implement the map function ourselves:

1 mymap : (a -> a) -> List a -> List a

2 mymap _ [] = []
3 mymap f (x::xs) = (f x) :: (mymap f xs)

Note that :: is used by the built-in List type, and is equivalent to Cons we’ve used
earlier. However, since :: is an infix operator, it has to go between the two arguments.
The value [] represents the empty list and is equivalent to End. In addition, the built-
in List type is polymorphic.
4. Programming in Idris 25

Exercise 14
Do a few different calculations with mymap in order to get a deeper
understanding of how it works.

Exercise 15
Implement a function myfilter that acts just like the filter function.
Hint: Use :t filter to get its type.

Exercise 16
Given foldl (\x, y => [y] ++ x) [] [1, 2, 3] and foldr (\x, y => y
++ [x]) [] [1, 2, 3]:

1. Evaluate both of them in Idris to see the values produced.

2. Try to understand the differences between the two expressions.
3. Remove the square brackets [ and ] in the lambda body to see what
errors Idris produces.
4. Evaluate them on paper to figure out why they produce the given
results.

4.1.8. Dependent types

We will implement the List n data type that we discussed in section 3.3, which
should limit the length of a list at the type level. Idris already has a built-in list like
this called Vect, so to not conflict we’ll name it MyVect. We can implement it as
follows:
 4. Programming in Idris 26

1 data MyVect : (n : Nat) -> Type where

2 Empty : MyVect 0
3 Cons : (x : Nat) -> (xs : MyVect len) -> MyVect (S len)

We created a new type called MyVect which accepts a natural number n and returns
a Type, that is joined with two value constructors:

1. Empty - which is just the empty vector (list)

2. Cons : (x : Nat) -> (xs : MyVect len) -> MyVect (S len) - which, given
a natural number x and a vector xs of length len, will return a vector of length
S len, that is, len + 1.

Note how we additionally specified names to the parameters (n : Nat, xs : MyVect

len, etc.). This can be useful if we want to reference those parameters elsewhere in
the type definition.
If we now use the following code snippet, it will pass the compile-time checks:

1 x : MyVect 2
2 x = Cons 1 (Cons 2 Empty)

However, if we try to use this code snippet instead:

1 x : MyVect 3
2 x = Cons 1 (Cons 2 Empty)

we will get the following error:

1 Type mismatch between

2 MyVect 0 (Type of Empty)
3 and
4 MyVect 1 (Expected type)

Which is a way of Idris telling us that our types do not match and that it cannot
verify the “proof” provided.
 4. Programming in Idris 27

In this example, we implemented a dependent type that puts the length of a list at
the type level. In other programming languages that do not support dependent types,
this is usually checked at the code level (run-time) and compile-time checks are not
able to verify this.
One example where such a guarantee might be useful is in preventing buffer
overflows. We could encode the dimension of an array at the type level, and statically
guarantee that array reads and writes only happen within bounds.

Exercise 17
Come up with a function isSingleton that accepts a Bool and returns a
Type. This function should return an object of type Nat in the True case,
and MyVect Nat otherwise. Further, implement a function mkSingle that
accepts a Bool, and returns isSingleton True or isSingleton False, and
as a computed value will either return 0 or Empty.
Hint: The data definitions are isSingleton : Bool -> Type and mkSingle
: (x : Bool) -> isSingleton x respectively.

4.1.9. Implicit parameters

Implicit parameters (arguments) allow us to bring values from the type level to the
program level. At the program level, by using curly braces we allow them to be used
in the definition of the function. Let’s take a look at the following example, which
uses our dependent type MyVect that we defined earlier:

1 lengthMyVect : MyVect n -> Nat

2 lengthMyVect {n = k} list = k

In this case, we defined a function lengthMyVect that takes a MyVect and returns a
natural number. The value n in the definition of the function will be the same as the
value of n at the type level. They are called implicit parameters because the caller
of this function needn’t pass these parameters. In the function definition, we define
implicit parameters with curly braces and we also need to specify the list parameter
which is of type MyVect n to pattern match against it. But, note how we don’t refer
to the list parameter in the computation part of this function and instead, we can use
an underscore (which represents an unused parameter) to get to:
 4. Programming in Idris 28

1 lengthMyVect : MyVect n -> Nat

2 lengthMyVect {n = k} _ = k

We can also have implicit parameters at the type level. As a matter of fact, an
equivalent type definition of that function is:

1 lengthMyVect : {n : Nat} -> MyVect n -> Nat

If we ask Idris to give us the type of this function, we will get the following for either
of the type definitions above:

1 Idris> :t lengthMyVect
2 lengthMyVect : MyVect n -> Nat

However, we can use the command :set showimplicits which will show the
implicits on the type level. If we do that, we will get the following for either of the
type definitions above:

1 Idris> :set showimplicits

2 Idris> :t lengthMyVect
3 lengthMyVect : {n : Nat} -> MyVect n -> Nat

To pass values for implicit arguments, we can use the following syntax:

1 Idris> lengthMyVect {n = 1} (Cons 1 Empty)

2 1 : Nat

Exercise 18
Try to evaluate the following code and observe the results:

1 lengthMyVect {n = 2} (Cons 1 Empty)

 4. Programming in Idris 29

4.1.10. Pattern matching expressions

We’ve seen how pattern matching is a powerful concept, in that it allows us to pattern
match against value constructors. For example, we can write a filtering function
that given a list of naturals produces a list of even naturals, by re-using the earlier
definition of even:

1 total even_members : MyList Nat -> MyList Nat

2 even_members End = End
3 even_members (Cons x l') = if (even x)
4 then (Cons x (even_members l'))
5 else even_members l'

The function above is a recursive one, and depending on the value of even x it will
branch the recursion. Since pattern matching works against value constructors, and
even x is a function call, we can’t easily pattern match against it. We used even x in
the function body to do the check. Idris provides another additional keyword with
that allows us to pattern match a value of some expression. The keyword with has
the following syntax:

1 function (pattern_match_1) with (expression)

2 pattern_match_1' | (value of expression to match) = ...
3 pattern_match_2' | (value of expression to match) = ...
4 ...

Note how we have to specify new pattern matching clauses after the line that uses
the with keyword. This is so because we won’t have the original pattern match in
context. Given this, an alternative definition of the function above is:

1 total even_members' : MyList Nat -> MyList Nat

2 even_members' End = End
3 even_members' (Cons x l') with (even x)
4 even_members' (Cons x l') | True = Cons x (even_members' l')
5 even_members' (Cons _ l') | False = (even_members' l')
 4. Programming in Idris 30

In this function, we defined two new pattern matches after the line that uses the
with keyword. Since we don’t have x and l' in this new pattern matching context,
we have to rewrite them on the left side of the pipe, and on the right side of the
pipe we pattern match against the value of even x, and then branch the recursion
(computation).

4.1.11. Interfaces and implementations

Interfaces are defined using the interface keyword and they allow us to add
constraints to types that implement them¹⁴. As an example, we’ll take a look at the
Eq interface:

1 interface Eq a where
2 (==) : a -> a -> Bool
3 (/=) : a -> a -> Bool
4 -- Minimal complete definition:
5 -- (==) or (/=)
6 x /= y = not (x == y)
7 x == y = not (x /= y)

Note how we can specify comments in the code by using two dashes. Comments are
ignored by the Idris compiler and are only useful to the reader of the code.
The definition says that for a type to implement the Eq interface, there must be
an implementation of the functions == and /= for that specific type. Additionally,
the interface also contains definitions for the functions, but this is optional. Since
the definition of == depends on /= (and vice-versa), it will be sufficient to provide
only one of them in the implementation, and the other one will be automatically
generated.
As an example, let’s assume that we have a data type:

¹⁴They are equivalent to Haskell’s class keyword. Interfaces in Idris are very similar to OOP’s interfaces.
 4. Programming in Idris 31

1 data Foo : Type where

2 Fooinst : Nat -> String -> Foo

To implement Eq for Foo, we can use the following code:

1 implementation Eq Foo where

2 (Fooinst x1 str1) ==
3 (Fooinst x2 str2) = (x1 == x2) && (str1 == str2)

We use == for Nat and String since this is already defined in Idris itself. With this,
we can easily use == and /= on Fooinst:

1 Idris> Fooinst 3 "orange" == Fooinst 6 "apple"

2 False : Bool
3 Idris> Fooinst 3 "orange" /= Fooinst 6 "apple"
4 True : Bool

Nats implement the built-in Num interface, which is what allows us to use 0 and Z
interchangeably.

Exercise 19
Implement your own data type Person that accepts a person’s name and
age, and implement an interface for comparing Persons.
Hint: One valid data type is:

1 data Person = Personinst String Int

4.2. Curry-Howard isomorphism

The Curry-Howard isomorphism (also known as Curry-Howard correspondence) is
the direct relationship between computer programs and mathematical proofs. It is
 4. Programming in Idris 32

named after the mathematician Haskell Curry and logician William Howard. In other
words, a mathematical proof is represented by a computer program and the formula
that we’re proving is the type of that program. As an example, we can take a look at
the function swap that is defined as follows:

1 swap : (a, b) -> (b, a)

2 swap (a, b) = (b, a)

The isomorphism says that this function has an equivalent form of mathematical
proof. Although it may not be immediately obvious, let’s consider the following
proof: Given P ∧ Q, prove that Q ∧ P . In order to prove it, we have to use the inference
rules and-introduction and and-elimination, which are defined as follows:

1. And-introduction means that if we are given P , Q, then we can construct a

proof for P ∧ Q
2. Left and-elimination means that if we are given P ∧ Q, we can conclude P
3. Right and-elimination means that if we are given P ∧ Q, we can conclude Q

If we want to implement this proof in Idris, we can represent it as a product type as

follows:

1 data And a b = And_intro a b

2
3 and_comm : And a b -> And b a
4 and_comm (And_intro a b) = And_intro b a

As we’ve discussed, we can use product types to encode pairs. We can note the
following similarities with our earlier definition of swap:

1. And_intro x y is equivalent to constructing a product type (x, y)

2. Left-elimination, which is a pattern match of And_intro a _ is equivalent to
the first element of the product type
3. Right-elimination, which is a pattern match of And_intro _ b is equivalent to
the second element of the product type

As long as Idris’ type checker terminates, we can be certain that the program provides
a mathematical proof of its type. This is why Idris’ type checker only evaluates total
functions, to keep the type checking decidable.
 4. Programming in Idris 33

4.3. Quantitative Type Theory

This book was written using Idris 1, however, in 2020 a new version, Idris 2 was
released which is based on Quantitative Type Theory. Most of the examples in
this book should be compatible with Idris 2. However, some Idris 2 code will not be
compatible with Idris 1. Idris 2 is recommended as it also might contain some bug
fixes.
Quantitative type theory gives more computational power at the type level. It allows
us to specify a quantity for each variable:

• 0 - which means that the variable is not used at run-time

• 1 - which means that the variable is used only once at run-time
• Unrestricted (default) - which is the same behavior as Idris 1

Consider the lengthMyVect example from before. If we change its definition from k
to k + k, the type checker will not complain:

1 lengthMyVect : {n : Nat} -> MyVect n -> Nat

2 lengthMyVect {n = k} _ = k + k

However, if we specify that the variable n can be used only once:

1 lengthMyVect : {1 n : Nat} -> MyVect n -> Nat

Then the type checker will throw an error for k + k, but not for k.
Further reading
Morris, D. W., Morris, J., Proofs and Concepts, 2016
Velleman, J. D., How to Prove It: A Structured Approach, 1994
Megill, N., Metamath, 1997
Halmos, P., Naive Set Theory, 1960
Lipovaca, M., Learn You a Haskell for Great Good, 2011
The Idris Community, Programming in Idris: A Tutorial, 2015
Wadler, P., Propositions as Types, 2014
Pierce, B., Logical Foundations, 2011
Pierce, B., Types and Programming Languages, 2002
Löh, A., McBride C., Swierstra W., A tutorial implementation of a dependently typed
lambda calculus, 2010
Martin-Löf, P., Intuitionistic Type Theory, 1984
Hofstadter, D., Gödel, Escher, Bach, 1979
Sitnikovski, B., Tutorial implementation of Hoare logic in Haskell, 2021
Smullyan, R., The Gödelian Puzzle Book, 2013
About the author
Boro Sitnikovski has over 10 years of experience working professionally as a Software
Engineer. He started programming using the Assembly programming language on an
Intel x86 at the age of 10. While in high school, he won several prizes for competitive
programming, varying from fourth, third, and first place.
He is an Informatics graduate; his Bachelor’s thesis was titled “Programming in
Haskell using algebraic data structures”, and his Master’s thesis was titled “Formal
verification of Instruction Sets in Virtual Machines”. He has also published papers
on software verification. Other research interests include programming languages,
mathematics, logic, algorithms, and writing correct software.
He is a strong believer in the open-source philosophy and contributes to various
open-source projects.
In his spare time, he enjoys time with his family.