# Documentation for the Idris 2 Language¶

Note

The documentation for Idris 2 has been published under the Creative
Commons CC0 License. As such to the extent possible under law, *The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.

More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/

## A Crash Course in Idris 2¶

This is a crash course in Idris 2 (sort of a tutorial, but rather less gentle I’m afraid!). It provides a brief introduction to programming in the Idris Language. It covers the core language features, assuming some experience with an existing functional programming language such as Haskell or OCaml.

This has been revised and updated from the Idris 1 tutorial. For details of changes since Idris 1, see Changes since Idris 1.

Note

The documentation for Idris has been published under the Creative
Commons CC0 License. As such to the extent possible under law, *The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.

More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

### Introduction¶

In conventional programming languages, there is a clear distinction
between *types* and *values*. For example, in Haskell, the following are types, representing
integers, characters, lists of characters, and lists of any value
respectively:

`Int`

,`Char`

,`[Char]`

,`[a]`

Correspondingly, the following values are examples of inhabitants of those types:

`42`

,`’a’`

,`"Hello world!"`

,`[2,3,4,5,6]`

In a language with *dependent types*, however, the distinction is less
clear. Dependent types allow types to “depend” on values — in other
words, types are a *first class* language construct and can be
manipulated like any other value. The standard example is the type of
lists of a given length [1], `Vect n a`

, where `a`

is the element
type and `n`

is the length of the list and can be an arbitrary term.

When types can contain values, and where those values describe
properties, for example the length of a list, the type of a function
can begin to describe its own properties. Take for example the
concatenation of two lists. This operation has the property that the
resulting list’s length is the sum of the lengths of the two input
lists. We can therefore give the following type to the `app`

function, which concatenates vectors:

```
app : Vect n a -> Vect m a -> Vect (n + m) a
```

This tutorial introduces Idris, a general purpose functional programming language with dependent types. The goal of the Idris project is to build a dependently typed language suitable for verifiable general purpose programming. To this end, Idris is a compiled language which aims to generate efficient executable code. It also has a lightweight foreign function interface which allows easy interaction with external libraries.

#### Intended Audience¶

This tutorial is intended as a brief introduction to the language, and is aimed at readers already familiar with a functional language such as Haskell or OCaml. In particular, a certain amount of familiarity with Haskell syntax is assumed, although most concepts will at least be explained briefly. The reader is also assumed to have some interest in using dependent types for writing and verifying software.

For a more in-depth introduction to Idris, which proceeds at a much slower pace, covering interactive program development, with many more examples, see Type-Driven Development with Idris by Edwin Brady, available from Manning.

#### Example Code¶

This tutorial includes some example code, which has been tested
against Idris 2. These files are available with the Idris 2 distribution,
so that you can try them out easily. They can be found under
`samples`

. It is, however, strongly recommended that you type
them in yourself, rather than simply loading and reading them.

Footnotes

[1] | Typically, and perhaps confusingly, referred to in the dependently typed programming literature as “vectors”. |

### Getting Started¶

#### Installing from Source¶

##### Prerequisites¶

Idris 2 is implemented in Idris 2 itself, so to bootstrap it you can build from generated Scheme sources. To do this, you need either Chez Scheme (default, and currently preferred since it is the fastest) or Racket. You can get one of these from:

Both are also available from MacPorts/Homebrew and all major Linux distributions.

**Note**: If you install Chez Scheme from source files, building it locally, make sure
you run `./configure --threads`

to build multithreading support in.

##### Downloading and Installing¶

You can download the Idris 2 source from the Idris web site or get the latest development version from idris-lang/Idris2 on Github. This includes the Idris 2 source code and the Scheme code generated from that. Once you have unpacked the source, you can install it as follows:

```
make bootstrap SCHEME=chez
```

Where chez is the executable name of the Chez Scheme compiler. This will
vary from system to system, but is often one of `scheme`

, `chezscheme`

, or
`chezscheme9.5`

. If you are building via Racket, you can install it as
follows:

```
make bootstrap-racket
```

Once you’ve successfully bootstrapped with any of the above commands, you can
install with the command `make install`

. This will, by default, install into
`${HOME}/.idris2`

. You can change this by editing the options in
`config.mk`

. For example, to install into `/usr/local`

, you can edit the
`PREFIX`

as follows:

```
PREFIX ?= /usr/local
```

#### Installing from a Package Manager¶

##### Installing Using Homebrew¶

If you are Homebrew user you can install Idris 2 together with all the requirements by running following command:

```
brew install idris2
```

#### Checking Installation¶

To check that installation has succeeded, and to write your first
Idris program, create a file called `hello.idr`

containing the
following text:

```
module Main
main : IO ()
main = putStrLn "Hello world"
```

If you are familiar with Haskell, it should be fairly clear what the
program is doing and how it works, but if not, we will explain the
details later. You can compile the program to an executable by
entering `idris2 hello.idr -o hello`

at the shell prompt. This will,
by default, create an executable called `hello`

, which invokes a generated
and compiled Chez Schem program, in the destination directory `build/exec`

which you can run:

```
$ idris2 hello.idr -o hello
$ ./build/exec/hello
Hello world
```

(On Macos you may first need to install realpath: ``brew install coreutils``

)

Please note that the dollar sign `$`

indicates the shell prompt!
Some useful options to the Idris command are:

`-o prog`

to compile to an executable called`prog`

.`--check`

type check the file and its dependencies without starting the interactive environment.`--package pkg`

add package as dependency, e.g.`--package contrib`

to make use of the contrib package.`--help`

display usage summary and command line options.

You can find out more about compiling to executables in Section Compiling to Executables.

#### The Interactive Environment¶

Entering `idris2`

at the shell prompt starts up the interactive
environment. You should see something like the following:

```
$ idris2
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.3.0
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
Main>
```

This gives a `ghci`

style interface which allows evaluation of, as
well as type checking of, expressions; theorem proving, compilation;
editing; and various other operations. The command `:?`

gives a list
of supported commands. Below, we see an example run in
which `hello.idr`

is loaded, the type of `main`

is checked and
then the program is compiled to the executable file `hello`

,
available in the destination directory `build/exec/`

. Type
checking a file, if successful, creates a bytecode version of the file (in this
case `build/ttc/hello.ttc`

) to speed up loading in future. The bytecode is
regenerated if the source file changes.

```
$ idris2 hello.idr
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.3.0
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
Main> :t main
Main.main : IO ()
Main> :c hello main
File build/exec/hello written
Main> :q
Bye for now!
```

### Types and Functions¶

#### Primitive Types¶

Idris defines several primitive types: `Int`

, `Integer`

and
`Double`

for numeric operations, `Char`

and `String`

for text
manipulation, and `Ptr`

which represents foreign pointers. There are
also several data types declared in the library, including `Bool`

,
with values `True`

and `False`

. We can declare some constants with
these types. Enter the following into a file `Prims.idr`

and load it
into the Idris interactive environment by typing `idris2 Prims.idr`

:

```
module Prims
x : Int
x = 94
foo : String
foo = "Sausage machine"
bar : Char
bar = 'Z'
quux : Bool
quux = False
```

An Idris file consists of an optional module declaration (here
`module Prims`

) followed by an optional list of imports and a
collection of declarations and definitions. In this example no imports
have been specified. However Idris programs can consist of several
modules and the definitions in each module each have their own
namespace. This is discussed further in Section
Modules and Namespaces. When writing Idris programs both the order in which
definitions are given and indentation are significant. Functions and
data types must be defined before use, incidentally each definition must
have a type declaration, for example see `x : Int`

, ```
foo :
String
```

, from the above listing. New declarations must begin at the
same level of indentation as the preceding declaration.
Alternatively, a semicolon `;`

can be used to terminate declarations.

A library module `prelude`

is automatically imported by every
Idris program, including facilities for IO, arithmetic, data
structures and various common functions. The prelude defines several
arithmetic and comparison operators, which we can use at the prompt.
Evaluating things at the prompt gives an answer, for example:

```
Prims> 13+9*9
94 : Integer
Prims> x == 9*9+13
True
```

All of the usual arithmetic and comparison operators are defined for
the primitive types. They are overloaded using interfaces, as we
will discuss in Section Interfaces and can be extended to
work on user defined types. Boolean expressions can be tested with the
`if...then...else`

construct, for example:

```
*prims> if x == 8 * 8 + 30 then "Yes!" else "No!"
"Yes!"
```

#### Data Types¶

Data types are declared in a similar way and with similar syntax to Haskell. Natural numbers and lists, for example, can be declared as follows:

```
data Nat = Z | S Nat -- Natural numbers
-- (zero and successor)
data List a = Nil | (::) a (List a) -- Polymorphic lists
```

The above declarations are taken from the standard library. Unary
natural numbers can be either zero (`Z`

), or the successor of
another natural number (`S k`

). Lists can either be empty (`Nil`

)
or a value added to the front of another list (`x :: xs`

). In the
declaration for `List`

, we used an infix operator `::`

. New
operators such as this can be added using a fixity declaration, as
follows:

```
infixr 10 ::
```

Functions, data constructors and type constructors may all be given
infix operators as names. They may be used in prefix form if enclosed
in brackets, e.g. `(::)`

. Infix operators can use any of the
symbols:

```
:+-*\/=.?|&><!@$%^~#
```

Some operators built from these symbols can’t be user defined. These are

`%`

, `\`

, `:`

, `=`

, `|`

, `|||`

, `<-`

, `->`

, `=>`

, `?`

,
`!`

, `&`

, `**`

, `..`

#### Functions¶

Functions are implemented by pattern matching, again using a similar
syntax to Haskell. The main difference is that Idris requires type
declarations for all functions, using a single colon `:`

(rather
than Haskell’s double colon `::`

). Some natural number arithmetic
functions can be defined as follows, again taken from the standard
library:

```
-- Unary addition
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
-- Unary multiplication
mult : Nat -> Nat -> Nat
mult Z y = Z
mult (S k) y = plus y (mult k y)
```

The standard arithmetic operators `+`

and `*`

are also overloaded
for use by `Nat`

, and are implemented using the above functions.
Unlike Haskell, there is no restriction on whether types and function
names must begin with a capital letter or not. Function names
(`plus`

and `mult`

above), data constructors (`Z`

, `S`

,
`Nil`

and `::`

) and type constructors (`Nat`

and `List`

) are
all part of the same namespace. By convention, however,
data types and constructor names typically begin with a capital letter.
We can test these functions at the Idris prompt:

```
Main> plus (S (S Z)) (S (S Z))
4
Main> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
12
```

Like arithmetic operations, integer literals are also overloaded using interfaces, meaning that we can also test the functions as follows:

```
Idris> plus 2 2
4
Idris> mult 3 (plus 2 2)
12
```

You may wonder, by the way, why we have unary natural numbers when our
computers have perfectly good integer arithmetic built in. The reason
is primarily that unary numbers have a very convenient structure which
is easy to reason about, and easy to relate to other data structures
as we will see later. Nevertheless, we do not want this convenience to
be at the expense of efficiency. Fortunately, Idris knows about
the relationship between `Nat`

(and similarly structured types) and
numbers. This means it can optimise the representation, and functions
such as `plus`

and `mult`

.

`where`

clauses¶

Functions can also be defined *locally* using `where`

clauses. For
example, to define a function which reverses a list, we can use an
auxiliary function which accumulates the new, reversed list, and which
does not need to be visible globally:

```
reverse : List a -> List a
reverse xs = revAcc [] xs where
revAcc : List a -> List a -> List a
revAcc acc [] = acc
revAcc acc (x :: xs) = revAcc (x :: acc) xs
```

Indentation is significant — functions in the `where`

block must be
indented further than the outer function.

Note

Scope

Any names which are visible in the outer scope are also visible in
the `where`

clause (unless they have been redefined, such as `xs`

here). A name which appears in the type will be in scope in the
`where`

clause.

As well as functions, `where`

blocks can include local data
declarations, such as the following where `MyLT`

is not accessible
outside the definition of `foo`

:

```
foo : Int -> Int
foo x = case isLT of
Yes => x*2
No => x*4
where
data MyLT = Yes | No
isLT : MyLT
isLT = if x < 20 then Yes else No
```

Functions defined in a `where`

clause need a type
declaration just like any top level function. Here is another example
of how this works in practice:

```
even : Nat -> Bool
even Z = True
even (S k) = odd k where
odd : Nat -> Bool
odd Z = False
odd (S k) = even k
test : List Nat
test = [c (S 1), c Z, d (S Z)]
where c : Nat -> Nat
c x = 42 + x
d : Nat -> Nat
d y = c (y + 1 + z y)
where z : Nat -> Nat
z w = y + w
```

##### Totality and Covering¶

By default, functions in Idris must be `covering`

. That is, there must be
patterns which cover all possible values of the inputs types. For example,
the following definition will give an error:

```
fromMaybe : Maybe a -> a
fromMaybe (Just x) = x
```

This gives an error because `fromMaybe Nothing`

is not defined. Idris
reports:

```
frommaybe.idr:1:1--2:1:fromMaybe is not covering. Missing cases:
fromMaybe Nothing
```

You can override this with a `partial`

annotation:

```
partial fromMaybe : Maybe a -> a
fromMaybe (Just x) = x
```

However, this is not advisable, and in general you should only do this during
the initial development of a function, or during debugging. If you try to
evaluate `fromMaybe Nothing`

at run time you will get a run time error.

##### Holes¶

Idris programs can contain *holes* which stand for incomplete parts of
programs. For example, we could leave a hole for the greeting in our
“Hello world” program:

```
main : IO ()
main = putStrLn ?greeting
```

The syntax `?greeting`

introduces a hole, which stands for a part of
a program which is not yet written. This is a valid Idris program, and you
can check the type of `greeting`

:

```
Main> :t greeting
-------------------------------------
greeting : String
```

Checking the type of a hole also shows the types of any variables in scope.
For example, given an incomplete definition of `even`

:

```
even : Nat -> Bool
even Z = True
even (S k) = ?even_rhs
```

We can check the type of `even_rhs`

and see the expected return type,
and the type of the variable `k`

:

```
Main> :t even_rhs
k : Nat
-------------------------------------
even_rhs : Bool
```

Holes are useful because they help us write functions *incrementally*.
Rather than writing an entire function in one go, we can leave some parts
unwritten and use Idris to tell us what is necessary to complete the
definition.

#### Dependent Types¶

##### First Class Types¶

In Idris, types are first class, meaning that they can be computed and manipulated (and passed to functions) just like any other language construct. For example, we could write a function which computes a type:

```
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
```

This function calculates the appropriate type from a `Bool`

which flags
whether the type should be a singleton or not. We can use this function
to calculate a type anywhere that a type can be used. For example, it
can be used to calculate a return type:

```
mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []
```

Or it can be used to have varying input types. The following function
calculates either the sum of a list of `Nat`

, or returns the given
`Nat`

, depending on whether the singleton flag is true:

```
sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs
```

##### Vectors¶

A standard example of a dependent data type is the type of “lists with
length”, conventionally called vectors in the dependent type
literature. They are available as part of the Idris library, by
importing `Data.Vect`

, or we can declare them as follows:

```
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
```

Note that we have used the same constructor names as for `List`

.
Ad-hoc name overloading such as this is accepted by Idris,
provided that the names are declared in different namespaces (in
practice, normally in different modules). Ambiguous constructor names
can normally be resolved from context.

This declares a family of types, and so the form of the declaration is
rather different from the simple type declarations above. We
explicitly state the type of the type constructor `Vect`

— it takes
a `Nat`

and a type as an argument, where `Type`

stands for the
type of types. We say that `Vect`

is *indexed* over `Nat`

and
*parameterised* by `Type`

. Each constructor targets a different part
of the family of types. `Nil`

can only be used to construct vectors
with zero length, and `::`

to construct vectors with non-zero
length. In the type of `::`

, we state explicitly that an element of
type `a`

and a tail of type `Vect k a`

(i.e., a vector of length
`k`

) combine to make a vector of length `S k`

.

We can define functions on dependent types such as `Vect`

in the same
way as on simple types such as `List`

and `Nat`

above, by pattern
matching. The type of a function over `Vect`

will describe what
happens to the lengths of the vectors involved. For example, `++`

,
defined as follows, appends two `Vect`

:

```
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: xs ++ ys
```

The type of `(++)`

states that the resulting vector’s length will be
the sum of the input lengths. If we get the definition wrong in such a
way that this does not hold, Idris will not accept the definition.
For example:

```
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
```

When run through the Idris type checker, this results in the following:

```
$ idris2 Vect.idr --check
1/1: Building Vect (Vect.idr)
Vect.idr:7:26--8:1:While processing right hand side of Main.++ at Vect.idr:7:1--8:1:
When unifying plus k k and plus k m
Mismatch between:
k
and
m
```

This error message suggests that there is a length mismatch between
two vectors — we needed a vector of length `k + m`

, but provided a
vector of length `k + k`

.

##### The Finite Sets¶

Finite sets, as the name suggests, are sets with a finite number of
elements. They are available as part of the Idris library, by
importing `Data.Fin`

, or can be declared as follows:

```
data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
```

From the signature, we can see that this is a type constructor that takes a `Nat`

, and produces a type.
So this is not a set in the sense of a collection that is a container of objects,
rather it is the canonical set of unnamed elements, as in “the set of 5 elements,” for example.
Effectively, it is a type that captures integers that fall into the range of zero to `(n - 1)`

where
`n`

is the argument used to instantiate the `Fin`

type.
For example, `Fin 5`

can be thought of as the type of integers between 0 and 4.

Let us look at the constructors in greater detail.

`FZ`

is the zeroth element of a finite set with `S k`

elements;
`FS n`

is the `n+1`

th element of a finite set with `S k`

elements. `Fin`

is indexed by a `Nat`

, which represents the number
of elements in the set. Since we can’t construct an element of an
empty set, neither constructor targets `Fin Z`

.

As mentioned above, a useful application of the `Fin`

family is to
represent bounded natural numbers. Since the first `n`

natural
numbers form a finite set of `n`

elements, we can treat `Fin n`

as
the set of integers greater than or equal to zero and less than `n`

.

For example, the following function which looks up an element in a
`Vect`

, by a bounded index given as a `Fin n`

, is defined in the
prelude:

```
index : Fin n -> Vect n a -> a
index FZ (x :: xs) = x
index (FS k) (x :: xs) = index k xs
```

This function looks up a value at a given location in a vector. The
location is bounded by the length of the vector (`n`

in each case),
so there is no need for a run-time bounds check. The type checker
guarantees that the location is no larger than the length of the
vector, and of course no less than zero.

Note also that there is no case for `Nil`

here. This is because it
is impossible. Since there is no element of `Fin Z`

, and the
location is a `Fin n`

, then `n`

can not be `Z`

. As a result,
attempting to look up an element in an empty vector would give a
compile time type error, since it would force `n`

to be `Z`

.

##### Implicit Arguments¶

Let us take a closer look at the type of `index`

:

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

It takes two arguments, an element of the finite set of `n`

elements,
and a vector with `n`

elements of type `a`

. But there are also two
names, `n`

and `a`

, which are not declared explicitly. These are
*implicit* arguments to `index`

. We could also write the type of
`index`

as:

```
index : forall a, n . Fin n -> Vect n a -> a
```

Implicit arguments, given with the `forall`

declaration,
are not given in applications of `index`

; their values can be
inferred from the types of the `Fin n`

and `Vect n a`

arguments. Any name beginning with a lower case letter which appears
as a parameter or index in a
type declaration, which is not applied to any arguments, will
*always* be automatically
bound as an implicit argument. Implicit arguments can still be given
explicitly in applications, using `{a=value}`

and `{n=value}`

, for
example:

```
index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
```

In fact, any argument, implicit or explicit, may be given a name. We
could have declared the type of `index`

as:

```
index : (i : Fin n) -> (xs : Vect n a) -> a
```

It is a matter of taste whether you want to do this — sometimes it can help document a function by making the purpose of an argument more clear.

The names of implicit arguments are in scope in the body of the function, although they cannot be used at run time. There is much more to say about implicit arguments - we will discuss the question of what is available at run time, among other things, in Section Multiplicities

###### Note: Declaration Order and `mutual`

blocks¶

In general, functions and data types must be defined before use, since
dependent types allow functions to appear as part of types, and type
checking can rely on how particular functions are defined (though this
is only true of total functions; see Section Totality Checking).
However, this restriction can be relaxed by using a `mutual`

block,
which allows data types and functions to be defined simultaneously:

```
mutual
even : Nat -> Bool
even Z = True
even (S k) = odd k
odd : Nat -> Bool
odd Z = False
odd (S k) = even k
```

In a `mutual`

block, first all of the type declarations are added,
then the function bodies. As a result, none of the function types can
depend on the reduction behaviour of any of the functions in the
block.

#### I/O¶

Computer programs are of little use if they do not interact with the
user or the system in some way. The difficulty in a pure language such
as Idris — that is, a language where expressions do not have
side-effects — is that I/O is inherently side-effecting. So, Idris provides
a parameterised type `IO`

which *describes* the interactions that the
run-time system will perform when executing a function:

```
data IO a -- description of an IO operation returning a value of type a
```

We’ll leave the definition of `IO`

abstract, but effectively it
describes what the I/O operations to be executed are, rather than how
to execute them. The resulting operations are executed externally, by
the run-time system. We’ve already seen one I/O program:

```
main : IO ()
main = putStrLn "Hello world"
```

The type of `putStrLn`

explains that it takes a string, and returns
an I/O action which produces an element of the unit type `()`

. There is a
variant `putStr`

which decribes the output of a string without a newline:

```
putStrLn : String -> IO ()
putStr : String -> IO ()
```

We can also read strings from user input:

```
getLine : IO String
```

A number of other I/O operations are available. For example, by adding
`import System.File`

to your program, you get access to functions for
reading and writing files, including:

```
data File -- abstract
data Mode = Read | Write | ReadWrite
openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
closeFile : File -> IO ()
fGetLine : (h : File) -> IO (Either FileError String)
fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
fEOF : File -> IO Bool
```

Note that several of these return `Either`

, since they may fail.

#### “`do`

” notation¶

I/O programs will typically need to sequence actions, feeding the
output of one computation into the input of the next. `IO`

is an
abstract type, however, so we can’t access the result of a computation
directly. Instead, we sequence operations with `do`

notation:

```
greet : IO ()
greet = do putStr "What is your name? "
name <- getLine
putStrLn ("Hello " ++ name)
```

The syntax `x <- iovalue`

executes the I/O operation `iovalue`

, of
type `IO a`

, and puts the result, of type `a`

into the variable
`x`

. In this case, `getLine`

returns an `IO String`

, so `name`

has type `String`

. Indentation is significant — each statement in
the do block must begin in the same column. The `pure`

operation
allows us to inject a value directly into an IO operation:

```
pure : a -> IO a
```

As we will see later, `do`

notation is more general than this, and
can be overloaded.

You can try executing `greet`

at the Idris 2 REPL by running the command
`:exec greet`

:

#### Laziness¶

Normally, arguments to functions are evaluated before the function
itself (that is, Idris uses *eager* evaluation). However, this is
not always the best approach. Consider the following function:

```
ifThenElse : Bool -> a -> a -> a
ifThenElse True t e = t
ifThenElse False t e = e
```

This function uses one of the `t`

or `e`

arguments, but not both.
We would prefer if *only* the argument which was used was evaluated. To achieve
this, Idris provides a `Lazy`

primitive, which allows evaluation to be
suspended. It is a primitive, but conceptually we can think of it as follows:

```
data Lazy : Type -> Type where
Delay : (val : a) -> Lazy a
Force : Lazy a -> a
```

A value of type `Lazy a`

is unevaluated until it is forced by
`Force`

. The Idris type checker knows about the `Lazy`

type,
and inserts conversions where necessary between `Lazy a`

and `a`

,
and vice versa. We can therefore write `ifThenElse`

as follows,
without any explicit use of `Force`

or `Delay`

:

```
ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True t e = t
ifThenElse False t e = e
```

#### Infinite data Types¶

Infinite data types (codata) allow us to define infinite data structures by marking recursive arguments as potentially infinite. One example of an infinite type is Stream, which is defined as follows.

```
data Stream : Type -> Type where
(::) : (e : a) -> Inf (Stream a) -> Stream a
```

The following is an example of how the codata type `Stream`

can be used to
form an infinite data structure. In this case we are creating an infinite stream
of ones.

```
ones : Stream Nat
ones = 1 :: ones
```

#### Useful Data Types¶

Idris includes a number of useful data types and library functions
(see the `libs/`

directory in the distribution, and the
documentation). This
section describes a few of these, and how to import them.

`List`

and `Vect`

¶

We have already seen the `List`

and `Vect`

data types:

```
data List a = Nil | (::) a (List a)
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
```

You can get access to `Vect`

with `import Data.Vect`

.
Note that the constructor names are the same for each — constructor
names (in fact, names in general) can be overloaded, provided that
they are declared in different namespaces (see Section
Modules and Namespaces), and will typically be resolved according to
their type. As syntactic sugar, any type with the constructor names
`Nil`

and `::`

can be written in list form. For example:

`[]`

means`Nil`

`[1,2,3]`

means`1 :: 2 :: 3 :: Nil`

The library also defines a number of functions for manipulating these
types. `map`

is overloaded both for `List`

and `Vect`

(we’ll see more
details of precisely how later when we cover interfaces in
Section Interfaces) and applies a function to every element of the
list or vector.

```
map : (a -> b) -> List a -> List b
map f [] = []
map f (x :: xs) = f x :: map f xs
map : (a -> b) -> Vect n a -> Vect n b
map f [] = []
map f (x :: xs) = f x :: map f xs
```

For example, given the following vector of integers, and a function to double an integer:

```
intVec : Vect 5 Int
intVec = [1, 2, 3, 4, 5]
double : Int -> Int
double x = x * 2
```

the function `map`

can be used as follows to double every element in
the vector:

```
*UsefulTypes> show (map double intVec)
"[2, 4, 6, 8, 10]" : String
```

For more details of the functions available on `List`

and
`Vect`

, look in the library files:

`libs/base/Data/List.idr`

`libs/base/Data/Vect.idr`

Functions include filtering, appending, reversing, and so on.

###### Aside: Anonymous functions and operator sections¶

There are neater ways to write the above expression. One way would be to use an anonymous function:

```
*UsefulTypes> show (map (\x => x * 2) intVec)
"[2, 4, 6, 8, 10]" : String
```

The notation `\x => val`

constructs an anonymous function which takes
one argument, `x`

and returns the expression `val`

. Anonymous
functions may take several arguments, separated by commas,
e.g. `\x, y, z => val`

. Arguments may also be given explicit types,
e.g. `\x : Int => x * 2`

, and can pattern match,
e.g. `\(x, y) => x + y`

. We could also use an operator section:

```
*UsefulTypes> show (map (* 2) intVec)
"[2, 4, 6, 8, 10]" : String
```

`(*2)`

is shorthand for a function which multiplies a number
by 2. It expands to `\x => x * 2`

. Similarly, `(2*)`

would expand
to `\x => 2 * x`

.

##### Maybe¶

`Maybe`

, defined in the Prelude, describes an optional value. Either there is
a value of the given type, or there isn’t:

```
data Maybe a = Just a | Nothing
```

`Maybe`

is one way of giving a type to an operation that may
fail. For example, looking something up in a `List`

(rather than a
vector) may result in an out of bounds error:

```
list_lookup : Nat -> List a -> Maybe a
list_lookup _ Nil = Nothing
list_lookup Z (x :: xs) = Just x
list_lookup (S k) (x :: xs) = list_lookup k xs
```

The `maybe`

function is used to process values of type `Maybe`

,
either by applying a function to the value, if there is one, or by
providing a default value:

```
maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
```

Note that the types of the first two arguments are wrapped in
`Lazy`

. Since only one of the two arguments will actually be used,
we mark them as `Lazy`

in case they are large expressions where it
would be wasteful to compute and then discard them.

##### Tuples¶

Values can be paired with the following built-in data type:

```
data Pair a b = MkPair a b
```

As syntactic sugar, we can write `(a, b)`

which, according to
context, means either `Pair a b`

or `MkPair a b`

. Tuples can
contain an arbitrary number of values, represented as nested pairs:

```
fred : (String, Int)
fred = ("Fred", 42)
jim : (String, Int, String)
jim = ("Jim", 25, "Cambridge")
```

```
*UsefulTypes> fst jim
"Jim" : String
*UsefulTypes> snd jim
(25, "Cambridge") : (Int, String)
*UsefulTypes> jim == ("Jim", (25, "Cambridge"))
True : Bool
```

##### Dependent Pairs¶

Dependent pairs allow the type of the second element of a pair to depend on the value of the first element:

```
data DPair : (a : Type) -> (p : a -> Type) -> Type where
MkDPair : {p : a -> Type} -> (x : a) -> p x -> DPair a p
```

Again, there is syntactic sugar for this. `(x : a ** p)`

is the type
of a pair of A and P, where the name `x`

can occur inside `p`

.
`( x ** p )`

constructs a value of this type. For example, we can
pair a number with a `Vect`

of a particular length:

```
vec : (n : Nat ** Vect n Int)
vec = (2 ** [3, 4])
```

If you like, you can write it out the long way; the two are equivalent:

```
vec : DPair Nat (\n => Vect n Int)
vec = MkDPair 2 [3, 4]
```

The type checker could infer the value of the first element
from the length of the vector. We can write an underscore `_`

in
place of values which we expect the type checker to fill in, so the
above definition could also be written as:

```
vec : (n : Nat ** Vect n Int)
vec = (_ ** [3, 4])
```

We might also prefer to omit the type of the first element of the pair, since, again, it can be inferred:

```
vec : (n ** Vect n Int)
vec = (_ ** [3, 4])
```

One use for dependent pairs is to return values of dependent types
where the index is not necessarily known in advance. For example, if
we filter elements out of a `Vect`

according to some predicate, we
will not know in advance what the length of the resulting vector will
be:

```
filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
```

If the `Vect`

is empty, the result is:

```
filter p Nil = (_ ** [])
```

In the `::`

case, we need to inspect the result of a recursive call
to `filter`

to extract the length and the vector from the result. To
do this, we use a `case`

expression, which allows pattern matching on
intermediate values:

```
filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter p Nil = (_ ** [])
filter p (x :: xs)
= case filter p xs of
(_ ** xs') => if p x then (_ ** x :: xs')
else (_ ** xs')
```

Dependent pairs are sometimes referred to as “Sigma types”.

##### Records¶

*Records* are data types which collect several values (the record’s *fields*)
together. Idris provides syntax for defining records and automatically
generating field access and update functions. Unlike the syntax used for data
structures, records in Idris follow a different syntax to that seen with
Haskell. For example, we can represent a person’s name and age in a record:

```
record Person where
constructor MkPerson
firstName, middleName, lastName : String
age : Int
fred : Person
fred = MkPerson "Fred" "Joe" "Bloggs" 30
```

The constructor name is provided using the `constructor`

keyword, and the
*fields* are then given which are in an indented block following the where
keyword (here, `firstName`

, `middleName`

, `lastName`

, and `age`

). You
can declare multiple fields on a single line, provided that they have the same
type. The field names can be used to access the field values:

```
*Record> fred.firstName
"Fred" : String
*Record> fred.age
30 : Int
*Record> :t (.firstName)
Main.Person.(.firstName) : Person -> String
```

We can use prefix field projections, like in Haskell:

```
*Record> firstName fred
"Fred" : String
*Record> age fred
30 : Int
*Record> :t firstName
firstName : Person -> String
```

Prefix field projections can be disabled per record definition
using pragma `%prefix_record_projections off`

, which makes
all subsequently defined records generate only dotted projections.
This pragma has effect until the end of the module
or until the closest occurrence of `%prefix_record_projections on`

.

We can also use the field names to update a record (or, more precisely, produce a copy of the record with the given fields updated):

```
*Record> record { firstName = "Jim" } fred
MkPerson "Jim" "Joe" "Bloggs" 30 : Person
*Record> record { firstName = "Jim", age $= (+ 1) } fred
MkPerson "Jim" "Joe" "Bloggs" 31 : Person
```

The syntax `record { field = val, ... }`

generates a function which
updates the given fields in a record. `=`

assigns a new value to a field,
and `$=`

applies a function to update its value.

Each record is defined in its own namespace, which means that field names can be reused in multiple records.

Records, and fields within records, can have dependent types. Updates are allowed to change the type of a field, provided that the result is well-typed.

```
record Class where
constructor ClassInfo
students : Vect n Person
className : String
```

It is safe to update the `students`

field to a vector of a different
length because it will not affect the type of the record:

```
addStudent : Person -> Class -> Class
addStudent p c = record { students = p :: students c } c
```

```
*Record> addStudent fred (ClassInfo [] "CS")
ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
```

We could also use `$=`

to define `addStudent`

more concisely:

```
addStudent' : Person -> Class -> Class
addStudent' p c = record { students $= (p ::) } c
```

###### Nested record projection¶

Nested record fields can be accessed using the dot notation:

```
x.a.b.c
map (.a.b.c) xs
```

For the dot notation, there must be no spaces after the dots but there may be
spaces before the dots. The composite projection must be parenthesised,
otherwise `map .a.b.c xs`

would be understood as `map.a.b.c xs`

.

Nested record fields can be accessed using the prefix notation, too:

```
(c . b . a) x
map (c . b . a) xs
```

Dots with spaces around them stand for function composition operators.

###### Nested record update¶

Idris also provides a convenient syntax for accessing and updating
nested records. For example, if a field is accessible with the
expression `x.a.b.c`

, it can be updated using the following
syntax:

```
record { a.b.c = val } x
```

This returns a new record, with the field accessed by the path
`a.b.c`

set to `val`

. The syntax is first class, i.e. ```
record {
a.b.c = val }
```

itself has a function type.

The `$=`

notation is also valid for nested record updates.

##### Dependent Records¶

Records can also be dependent on values. Records have *parameters*, which
cannot be updated like the other fields. The parameters appear as arguments
to the resulting type, and are written following the record type
name. For example, a pair type could be defined as follows:

```
record Prod a b where
constructor Times
fst : a
snd : b
```

Using the `Class`

record from earlier, the size of the class can be
restricted using a `Vect`

and the size included in the type by parameterising
the record with the size. For example:

```
record SizedClass (size : Nat) where
constructor SizedClassInfo
students : Vect size Person
className : String
```

In the case of `addStudent`

earlier, we can still add a student to a
`SizedClass`

since the size is implicit, and will be updated when a student
is added:

```
addStudent : Person -> SizedClass n -> SizedClass (S n)
addStudent p c = record { students = p :: students c } c
```

In fact, the dependent pair type we have just seen is, in practice, defined
as a record, with fields `fst`

and `snd`

which allow projecting values
out of the pair:

```
record DPair a (p : a -> Type) where
constructor MkDPair
fst : a
snd : p fst
```

It is possible to use record update syntax to update dependent fields, provided that all related fields are updated at once. For example:

```
cons : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
cons val xs
= record { fst = S (fst xs),
snd = (val :: snd xs) } xs
```

Or even:

```
cons' : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
cons' val
= record { fst $= S,
snd $= (val ::) }
```

#### More Expressions¶

`let`

bindings¶

Intermediate values can be calculated using `let`

bindings:

```
mirror : List a -> List a
mirror xs = let xs' = reverse xs in
xs ++ xs'
```

We can do pattern matching in `let`

bindings too. For
example, we can extract fields from a record as follows, as well as by
pattern matching at the top level:

```
data Person = MkPerson String Int
showPerson : Person -> String
showPerson p = let MkPerson name age = p in
name ++ " is " ++ show age ++ " years old"
```

##### List comprehensions¶

Idris provides *comprehension* notation as a convenient shorthand
for building lists. The general form is:

```
[ expression | qualifiers ]
```

This generates the list of values produced by evaluating the
`expression`

, according to the conditions given by the comma
separated `qualifiers`

. For example, we can build a list of
Pythagorean triples as follows:

```
pythag : Int -> List (Int, Int, Int)
pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
x*x + y*y == z*z ]
```

The `[a..b]`

notation is another shorthand which builds a list of
numbers between `a`

and `b`

. Alternatively `[a,b..c]`

builds a
list of numbers between `a`

and `c`

with the increment specified
by the difference between `a`

and `b`

. This works for type `Nat`

,
`Int`

and `Integer`

, using the `enumFromTo`

and `enumFromThenTo`

function from the prelude.

`case`

expressions¶

Another way of inspecting intermediate values is to use a `case`

expression.
The following function, for example, splits a string into two at a given
character:

```
splitAt : Char -> String -> (String, String)
splitAt c x = case break (== c) x of
(x, y) => (x, strTail y)
```

`break`

is a library function which breaks a string into a pair of
strings at the point where the given function returns true. We then
deconstruct the pair it returns, and remove the first character of the
second string.

A `case`

expression can match several cases, for example, to inspect
an intermediate value of type `Maybe a`

. Recall `list_lookup`

which looks up an index in a list, returning `Nothing`

if the index
is out of bounds. We can use this to write `lookup_default`

, which
looks up an index and returns a default value if the index is out of
bounds:

```
lookup_default : Nat -> List a -> a -> a
lookup_default i xs def = case list_lookup i xs of
Nothing => def
Just x => x
```

If the index is in bounds, we get the value at that index, otherwise we get a default value:

```
*UsefulTypes> lookup_default 2 [3,4,5,6] (-1)
5 : Integer
*UsefulTypes> lookup_default 4 [3,4,5,6] (-1)
-1 : Integer
```

#### Totality¶

Idris distinguishes between *total* and *partial* functions.
A total function is a function that either:

- Terminates for all possible inputs, or
- Produces a non-empty, finite, prefix of a possibly infinite result

If a function is total, we can consider its type a precise description of what
that function will do. For example, if we have a function with a return
type of `String`

we know something different, depending on whether or not
it’s total:

- If it’s total, it will return a value of type
`String`

in finite time; - If it’s partial, then as long as it doesn’t crash or enter an infinite loop,
it will return a
`String`

.

Idris makes this distinction so that it knows which functions are safe to evaluate while type checking (as we’ve seen with First Class Types). After all, if it tries to evaluate a function during type checking which doesn’t terminate, then type checking won’t terminate! Therefore, only total functions will be evaluated during type checking. Partial functions can still be used in types, but will not be evaluated further.

### Interfaces¶

We often want to define functions which work across several different
data types. For example, we would like arithmetic operators to work on
`Int`

, `Integer`

and `Double`

at the very least. We would like
`==`

to work on the majority of data types. We would like to be able
to display different types in a uniform way.

To achieve this, we use *interfaces*, which are similar to type classes in
Haskell or traits in Rust. To define an interface, we provide a collection of
overloadable functions. A simple example is the `Show`

interface, which is defined in the prelude and provides an interface for
converting values to `String`

:

```
interface Show a where
show : a -> String
```

This generates a function of the following type (which we call a
*method* of the `Show`

interface):

```
show : Show a => a -> String
```

We can read this as: “under the constraint that `a`

has an implementation
of `Show`

, take an input `a`

and return a `String`

.” An implementation
of an interface is defined by giving definitions of the methods of the interface.
For example, the `Show`

implementation for `Nat`

could be defined as:

```
Show Nat where
show Z = "Z"
show (S k) = "s" ++ show k
```

```
Main> show (S (S (S Z)))
"sssZ" : String
```

Only one implementation of an interface can be given for a type — implementations may
not overlap. Implementation declarations can themselves have constraints.
To help with resolution, the arguments of an implementation must be
constructors (either data or type constructors) or variables
(i.e. you cannot give an implementation for a function). For
example, to define a `Show`

implementation for vectors, we need to know
that there is a `Show`

implementation for the element type, because we are
going to use it to convert each element to a `String`

:

```
Show a => Show (Vect n a) where
show xs = "[" ++ show' xs ++ "]" where
show' : forall n . Vect n a -> String
show' Nil = ""
show' (x :: Nil) = show x
show' (x :: xs) = show x ++ ", " ++ show' xs
```

Note that we need the explicit `forall n .`

in the `show'`

function
because otherwise the `n`

is already in scope, and fixed to the value of
the top level `n`

.

#### Default Definitions¶

The Prelude defines an `Eq`

interface which provides methods for
comparing values for equality or inequality, with implementations for all of
the built-in types:

```
interface Eq a where
(==) : a -> a -> Bool
(/=) : a -> a -> Bool
```

To declare an implementation for a type, we have to give definitions of all
of the methods. For example, for an implementation of `Eq`

for `Nat`

:

```
Eq Nat where
Z == Z = True
(S x) == (S y) = x == y
Z == (S y) = False
(S x) == Z = False
x /= y = not (x == y)
```

It is hard to imagine many cases where the `/=`

method will be
anything other than the negation of the result of applying the `==`

method. It is therefore convenient to give a default definition for
each method in the interface declaration, in terms of the other method:

```
interface Eq a where
(==) : a -> a -> Bool
(/=) : a -> a -> Bool
x /= y = not (x == y)
x == y = not (x /= y)
```

A minimal complete implementation of `Eq`

requires either
`==`

or `/=`

to be defined, but does not require both. If a method
definition is missing, and there is a default definition for it, then
the default is used instead.

#### Extending Interfaces¶

Interfaces can also be extended. A logical next step from an equality
relation `Eq`

is to define an ordering relation `Ord`

. We can
define an `Ord`

interface which inherits methods from `Eq`

as well as
defining some of its own:

```
data Ordering = LT | EQ | GT
```

```
interface Eq a => Ord a where
compare : a -> a -> Ordering
(<) : a -> a -> Bool
(>) : a -> a -> Bool
(<=) : a -> a -> Bool
(>=) : a -> a -> Bool
max : a -> a -> a
min : a -> a -> a
```

The `Ord`

interface allows us to compare two values and determine their
ordering. Only the `compare`

method is required; every other method
has a default definition. Using this we can write functions such as
`sort`

, a function which sorts a list into increasing order,
provided that the element type of the list is in the `Ord`

interface. We
give the constraints on the type variables left of the fat arrow
`=>`

, and the function type to the right of the fat arrow:

```
sort : Ord a => List a -> List a
```

Functions, interfaces and implementations can have multiple constraints. Multiple constraints are written in brackets in a comma separated list, for example:

```
sortAndShow : (Ord a, Show a) => List a -> String
sortAndShow xs = show (sort xs)
```

Constraints are, like types, first class objects in the language. You can see this at the REPL:

```
Main> :t Ord
Prelude.Ord : Type -> Type
```

So, `(Ord a, Show a)`

is an ordinary pair of `Types`

, with two constraints
as the first and second element of the pair.

##### Note: Interfaces and `mutual`

blocks¶

Idris is strictly “define before use”, except in `mutual`

blocks.
In a `mutual`

block, Idris elaborates in two passes: types on the first
pass and definitions on the second. When the mutual block contains an
interface declaration, it elaborates the interface header but none of the
method types on the first pass, and elaborates the method types and any
default definitions on the second pass.

#### Quantities for Parameters¶

By default parameters that are not explicitly ascribed a type in an `interface`

declaration are assigned the quantity `0`

. This means that the parameter is not
available to use at runtime in the methods’ definitions.

For instance, `Show a`

gives rise to a `0`

-quantified type variable `a`

in
the type of the `show`

method:

```
Main> :set showimplicits
Main> :t show
Prelude.show : {0 a : Type} -> Show a => a -> String
```

However some use cases require that some of the parameters are available at runtime.
We may for instance want to declare an interface for `Storable`

types. The constraint
`Storable a size`

means that we can store values of type `a`

in a `Buffer`

in
exactly `size`

bytes.

If the user provides a method to read a value for such a type `a`

at a given offset,
then we can read the `k`

th element stored in the buffer by computing the appropriate
offset from `k`

and `size`

. This is demonstrated by providing a default implementation
for the method `peekElementOff`

implemented in terms of `peekByteOff`

and the parameter
`size`

.

```
data ForeignPtr : Type -> Type where
MkFP : Buffer -> ForeignPtr a
interface Storable (0 a : Type) (size : Nat) | a where
peekByteOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
peekElemOff fp k = peekByteOff fp (k * cast size)
```

Note that `a`

is explicitly marked as runtime irrelevant so that it is erased by the
compiler. Equivalently we could have written `interface Storable a (size : Nat)`

.
The meaning of `| a`

is explained in Determining Parameters.

#### Functors and Applicatives¶

So far, we have seen single parameter interfaces, where the parameter
is of type `Type`

. In general, there can be any number of parameters
(even zero), and the parameters can have *any* type. If the type
of the parameter is not `Type`

, we need to give an explicit type
declaration. For example, the `Functor`

interface is defined in the
prelude:

```
interface Functor (0 f : Type -> Type) where
map : (m : a -> b) -> f a -> f b
```

A functor allows a function to be applied across a structure, for
example to apply a function to every element in a `List`

:

```
Functor List where
map f [] = []
map f (x::xs) = f x :: map f xs
```

```
Idris> map (*2) [1..10]
[2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer
```

Having defined `Functor`

, we can define `Applicative`

which
abstracts the notion of function application:

```
infixl 2 <*>
interface Functor f => Applicative (0 f : Type -> Type) where
pure : a -> f a
(<*>) : f (a -> b) -> f a -> f b
```

#### Monads and `do`

-notation¶

The `Monad`

interface allows us to encapsulate binding and computation,
and is the basis of `do`

-notation introduced in Section
“do” notation. It extends `Applicative`

as defined above, and is
defined as follows:

```
interface Applicative m => Monad (m : Type -> Type) where
(>>=) : m a -> (a -> m b) -> m b
```

Inside a `do`

block, the following syntactic transformations are
applied:

`x <- v; e`

becomes`v >>= (\x => e)`

`v; e`

becomes`v >>= (\_ => e)`

`let x = v; e`

becomes`let x = v in e`

`IO`

has an implementation of `Monad`

, defined using primitive functions.
We can also define an implementation for `Maybe`

, as follows:

```
Monad Maybe where
Nothing >>= k = Nothing
(Just x) >>= k = k x
```

Using this we can, for example, define a function which adds two
`Maybe Int`

, using the monad to encapsulate the error handling:

```
m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = do x' <- x -- Extract value from x
y' <- y -- Extract value from y
pure (x' + y') -- Add them
```

This function will extract the values from `x`

and `y`

, if they
are both available, or return `Nothing`

if one or both are not (“fail fast”). Managing the
`Nothing`

cases is achieved by the `>>=`

operator, hidden by the
`do`

notation.

```
Main> m_add (Just 82) (Just 22)
Just 94
Main> m_add (Just 82) Nothing
Nothing
```

The translation of `do`

notation is entirely syntactic, so there is no
need for the `(>>=)`

operator to be the operator defined in the `Monad`

interface. Idris will, in general, try to disambiguate which `(>>=)`

you
mean by type, but you can explicitly choose with qualified do notation,
for example:

```
m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = Prelude.do
x' <- x -- Extract value from x
y' <- y -- Extract value from y
pure (x' + y') -- Add them
```

The `Prelude.do`

means that Idris will use the `(>>=)`

operator defined
in the `Prelude`

.

##### Pattern Matching Bind¶

Sometimes we want to pattern match immediately on the result of a function
in `do`

notation. For example, let’s say we have a function `readNumber`

which reads a number from the console, returning a value of the form
`Just x`

if the number is valid, or `Nothing`

otherwise:

```
import Data.Strings
readNumber : IO (Maybe Nat)
readNumber = do
input <- getLine
if all isDigit (unpack input)
then pure (Just (stringToNatOrZ input))
else pure Nothing
```

If we then use it to write a function to read two numbers, returning
`Nothing`

if neither are valid, then we would like to pattern match
on the result of `readNumber`

:

```
readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
do x <- readNumber
case x of
Nothing => pure Nothing
Just x_ok => do y <- readNumber
case y of
Nothing => pure Nothing
Just y_ok => pure (Just (x_ok, y_ok))
```

If there’s a lot of error handling, this could get deeply nested very quickly!
So instead, we can combine the bind and the pattern match in one line. For example,
we could try pattern matching on values of the form `Just x_ok`

:

```
readNumbers : IO (Maybe (Nat, Nat))
readNumbers
= do Just x_ok <- readNumber
Just y_ok <- readNumber
pure (Just (x_ok, y_ok))
```

There is still a problem, however, because we’ve now omitted the case for
`Nothing`

so `readNumbers`

is no longer total! We can add the `Nothing`

case back as follows:

```
readNumbers : IO (Maybe (Nat, Nat))
readNumbers
= do Just x_ok <- readNumber
| Nothing => pure Nothing
Just y_ok <- readNumber
| Nothing => pure Nothing
pure (Just (x_ok, y_ok))
```

The effect of this version of `readNumbers`

is identical to the first (in
fact, it is syntactic sugar for it and directly translated back into that form).
The first part of each statement (`Just x_ok <-`

and `Just y_ok <-`

) gives
the preferred binding - if this matches, execution will continue with the rest
of the `do`

block. The second part gives the alternative bindings, of which
there may be more than one.

`!`

-notation¶

In many cases, using `do`

-notation can make programs unnecessarily
verbose, particularly in cases such as `m_add`

above where the value
bound is used once, immediately. In these cases, we can use a
shorthand version, as follows:

```
m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = pure (!x + !y)
```

The notation `!expr`

means that the expression `expr`

should be
evaluated and then implicitly bound. Conceptually, we can think of
`!`

as being a prefix function with the following type:

```
(!) : m a -> a
```

Note, however, that it is not really a function, merely syntax! In
practice, a subexpression `!expr`

will lift `expr`

as high as
possible within its current scope, bind it to a fresh name `x`

, and
replace `!expr`

with `x`

. Expressions are lifted depth first, left
to right. In practice, `!`

-notation allows us to program in a more
direct style, while still giving a notational clue as to which
expressions are monadic.

For example, the expression:

```
let y = 94 in f !(g !(print y) !x)
```

is lifted to:

```
let y = 94 in do y' <- print y
x' <- x
g' <- g y' x'
f g'
```

##### Monad comprehensions¶

The list comprehension notation we saw in Section
More Expressions is more general, and applies to anything which
has an implementation of both `Monad`

and `Alternative`

:

```
interface Applicative f => Alternative (0 f : Type -> Type) where
empty : f a
(<|>) : f a -> f a -> f a
```

In general, a comprehension takes the form ```
[ exp | qual1, qual2, …,
qualn ]
```

where `quali`

can be one of:

- A generator
`x <- e`

- A
*guard*, which is an expression of type`Bool`

- A let binding
`let x = e`

To translate a comprehension `[exp | qual1, qual2, …, qualn]`

, first
any qualifier `qual`

which is a *guard* is translated to ```
guard
qual
```

, using the following function:

```
guard : Alternative f => Bool -> f ()
```

Then the comprehension is converted to `do`

notation:

```
do { qual1; qual2; ...; qualn; pure exp; }
```

Using monad comprehensions, an alternative definition for `m_add`

would be:

```
m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = [ x' + y' | x' <- x, y' <- y ]
```

#### Interfaces and IO¶

In general, `IO`

operations in the libraries aren’t written using `IO`

directly, but rather via the `HasIO`

interface:

```
interface Monad io => HasIO io where
liftIO : (1 _ : IO a) -> io a
```

`HasIO`

explains, via `liftIO`

, how to convert a primitive `IO`

operation
to an operation in some underlying type, as long as that type has a `Monad`

implementation. These interface allows a programmer to define some more
expressive notion of interactive program, while still giving direct access to
`IO`

primitives.

#### Idiom brackets¶

While `do`

notation gives an alternative meaning to sequencing,
idioms give an alternative meaning to *application*. The notation and
larger example in this section is inspired by Conor McBride and Ross
Paterson’s paper “Applicative Programming with Effects” [1].

First, let us revisit `m_add`

above. All it is really doing is
applying an operator to two values extracted from `Maybe Int`

. We
could abstract out the application:

```
m_app : Maybe (a -> b) -> Maybe a -> Maybe b
m_app (Just f) (Just a) = Just (f a)
m_app _ _ = Nothing
```

Using this, we can write an alternative `m_add`

which uses this
alternative notion of function application, with explicit calls to
`m_app`

:

```
m_add' : Maybe Int -> Maybe Int -> Maybe Int
m_add' x y = m_app (m_app (Just (+)) x) y
```

Rather than having to insert `m_app`

everywhere there is an
application, we can use idiom brackets to do the job for us.
To do this, we can give `Maybe`

an implementation of `Applicative`

as follows, where `<*>`

is defined in the same way as `m_app`

above (this is defined in the Idris library):

```
Applicative Maybe where
pure = Just
(Just f) <*> (Just a) = Just (f a)
_ <*> _ = Nothing
```

Using `<*>`

we can use this implementation as follows, where a function
application `[| f a1 …an |]`

is translated into ```
pure f <*> a1 <*>
… <*> an
```

:

```
m_add' : Maybe Int -> Maybe Int -> Maybe Int
m_add' x y = [| x + y |]
```

##### An error-handling interpreter¶

Idiom notation is commonly useful when defining evaluators. McBride and Paterson describe such an evaluator [1], for a language similar to the following:

```
data Expr = Var String -- variables
| Val Int -- values
| Add Expr Expr -- addition
```

Evaluation will take place relative to a context mapping variables
(represented as `String`

s) to `Int`

values, and can possibly fail.
We define a data type `Eval`

to wrap an evaluator:

```
data Eval : Type -> Type where
MkEval : (List (String, Int) -> Maybe a) -> Eval a
```

Wrapping the evaluator in a data type means we will be able to provide implementations of interfaces for it later. We begin by defining a function to retrieve values from the context during evaluation:

```
fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where
fetchVal : List (String, Int) -> Maybe Int
fetchVal [] = Nothing
fetchVal ((v, val) :: xs) = if (x == v)
then (Just val)
else (fetchVal xs)
```

When defining an evaluator for the language, we will be applying functions in
the context of an `Eval`

, so it is natural to give `Eval`

an implementation
of `Applicative`

. Before `Eval`

can have an implementation of
`Applicative`

it is necessary for `Eval`

to have an implementation of
`Functor`

:

```
Functor Eval where
map f (MkEval g) = MkEval (\e => map f (g e))
Applicative Eval where
pure x = MkEval (\e => Just x)
(<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
app : Maybe (a -> b) -> Maybe a -> Maybe b
app (Just fx) (Just gx) = Just (fx gx)
app _ _ = Nothing
```

Evaluating an expression can now make use of the idiomatic application to handle errors:

```
eval : Expr -> Eval Int
eval (Var x) = fetch x
eval (Val x) = [| x |]
eval (Add x y) = [| eval x + eval y |]
runEval : List (String, Int) -> Expr -> Maybe Int
runEval env e = case eval e of
MkEval envFn => envFn env
```

For example:

```
InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "y"))
Just 94
InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "z"))
Nothing
```

#### Named Implementations¶

It can be desirable to have multiple implementations of an interface for the
same type, for example to provide alternative methods for sorting or printing
values. To achieve this, implementations can be *named* as follows:

```
[myord] Ord Nat where
compare Z (S n) = GT
compare (S n) Z = LT
compare Z Z = EQ
compare (S x) (S y) = compare @{myord} x y
```

This declares an implementation as normal, but with an explicit name,
`myord`

. The syntax `compare @{myord}`

gives an explicit implementation to
`compare`

, otherwise it would use the default implementation for `Nat`

. We
can use this, for example, to sort a list of `Nat`

in reverse.
Given the following list:

```
testList : List Nat
testList = [3,4,1]
```

We can sort it using the default `Ord`

implementation, by using the `sort`

function available with `import Data.List`

, then we can try with the named
implementation `myord`

as follows, at the Idris prompt:

```
Main> show (sort testList)
"[1, 3, 4]"
Main> show (sort @{myord} testList)
"[4, 3, 1]"
```

Sometimes, we also need access to a named parent implementation. For example,
the prelude defines the following `Semigroup`

interface:

```
interface Semigroup ty where
(<+>) : ty -> ty -> ty
```

Then it defines `Monoid`

, which extends `Semigroup`

with a “neutral”
value:

```
interface Semigroup ty => Monoid ty where
neutral : ty
```

We can define two different implementations of `Semigroup`

and
`Monoid`

for `Nat`

, one based on addition and one on multiplication:

```
[PlusNatSemi] Semigroup Nat where
(<+>) x y = x + y
[MultNatSemi] Semigroup Nat where
(<+>) x y = x * y
```

The neutral value for addition is `0`

, but the neutral value for multiplication
is `1`

. It’s important, therefore, that when we define implementations
of `Monoid`

they extend the correct `Semigroup`

implementation. We can
do this with a `using`

clause in the implementation as follows:

```
[PlusNatMonoid] Monoid Nat using PlusNatSemi where
neutral = 0
[MultNatMonoid] Monoid Nat using MultNatSemi where
neutral = 1
```

The `using PlusNatSemi`

clause indicates that `PlusNatMonoid`

should
extend `PlusNatSemi`

specifically.

#### Determining Parameters¶

When an interface has more than one parameter, it can help resolution if the parameters used to find an implementation are restricted. For example:

```
interface Monad m => MonadState s (0 m : Type -> Type) | m where
get : m s
put : s -> m ()
```

In this interface, only `m`

needs to be known to find an implementation of
this interface, and `s`

can then be determined from the implementation. This
is declared with the `| m`

after the interface declaration. We call `m`

a
*determining parameter* of the `MonadState`

interface, because it is the
parameter used to find an implementation. This is similar to the concept of
*functional dependencies* in Haskell.

[1] | (1, 2) Conor McBride and Ross Paterson. 2008. Applicative programming
with effects. J. Funct. Program. 18, 1 (January 2008),
1-13. DOI=10.1017/S0956796807006326
https://dx.doi.org/10.1017/S0956796807006326 |

### Modules and Namespaces¶

An Idris program consists of a collection of modules. Each module
includes an optional `module`

declaration giving the name of the
module, a list of `import`

statements giving the other modules which
are to be imported, and a collection of declarations and definitions of
types, interfaces and functions. For example, the listing below gives a
module which defines a binary tree type `BTree`

(in a file
`BTree.idr`

):

```
module BTree
public export
data BTree a = Leaf
| Node (BTree a) a (BTree a)
export
insert : Ord a => a -> BTree a -> BTree a
insert x Leaf = Node Leaf x Leaf
insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
else (Node l v (insert x r))
export
toList : BTree a -> List a
toList Leaf = []
toList (Node l v r) = BTree.toList l ++ (v :: BTree.toList r)
export
toTree : Ord a => List a -> BTree a
toTree [] = Leaf
toTree (x :: xs) = insert x (toTree xs)
```

The modifiers `export`

and `public export`

say which names are visible
from other namespaces. These are explained further below.

Then, this gives a main program (in a file
`bmain.idr`

) which uses the `BTree`

module to sort a list:

```
module Main
import BTree
main : IO ()
main = do let t = toTree [1,8,2,7,9,3]
print (BTree.toList t)
```

The same names can be defined in multiple modules: names are *qualified* with
the name of the module. The names defined in the `BTree`

module are, in full:

`BTree.BTree`

`BTree.Leaf`

`BTree.Node`

`BTree.insert`

`BTree.toList`

`BTree.toTree`

If names are otherwise unambiguous, there is no need to give the fully
qualified name. Names can be disambiguated either by giving an explicit
qualification, using the `with`

keyword, or according to their type.

The `with`

keyword in expressions comes in two variants:

`with BTree.insert (insert x empty)`

for one name`with [BTree.insert, BTree.empty] (insert x empty)`

for multiple names

This is particularly useful with `do`

notation, where it can often improve
error messages: `with MyModule.(>>=) do ...`

There is no formal link between the module name and its filename,
although it is generally advisable to use the same name for each. An
`import`

statement refers to a filename, using dots to separate
directories. For example, `import foo.bar`

would import the file
`foo/bar.idr`

, which would conventionally have the module declaration
`module foo.bar`

. The only requirement for module names is that the
main module, with the `main`

function, must be called
`Main`

— although its filename need not be `Main.idr`

.

#### Export Modifiers¶

Idris allows for fine-grained control over the visibility of a
namespace’s contents. By default, all names defined in a namespace are kept
private. This aids in specification of a minimal interface and for
internal details to be left hidden. Idris allows for functions,
types, and interfaces to be marked as: `private`

, `export`

, or
`public export`

. Their general meaning is as follows:

`private`

meaning that it is not exported at all. This is the default.`export`

meaning that its top level type is exported.`public export`

meaning that the entire definition is exported.

A further restriction in modifying the visibility is that definitions must not
refer to anything within a lower level of visibility. For example, ```
public
export
```

definitions cannot use `private`

or `export`

names, and `export`

types cannot use `private`

names. This is to prevent private names leaking
into a module’s interface.

##### Meaning for Functions¶

`export`

the type is exported`public export`

the type and definition are exported, and the definition can be used after it is imported. In other words, the definition itself is considered part of the module’s interface. The long name`public export`

is intended to make you think twice about doing this.

Note

Type synonyms in Idris are created by writing a function. When
setting the visibility for a module, it is usually a good idea to
`public export`

all type synonyms if they are to be used outside
the module. Otherwise, Idris won’t know what the synonym is a
synonym for.

Since `public export`

means that a function’s definition is exported,
this effectively makes the function definition part of the module’s API.
Therefore, it’s generally a good idea to avoid using `public export`

for
functions unless you really mean to export the full definition.

Note

*For beginners*:
If the function needs to be accessed only at runtime, use `export`

.
However, if it’s also meant to be used at *compile* time (e.g. to prove
a theorem), use `public export`

.
For example, consider the function `plus : Nat -> Nat -> Nat`

discussed
previously, and the following theorem: `thm : plus Z m = m`

.
In order to prove it, the type checker needs to reduce `plus Z m`

to `m`

(and hence obtain `thm : m = m`

).
To achieve this, it will need access to the *definition* of `plus`

,
which includes the equation `plus Z m = m`

.
Therefore, in this case, `plus`

has to be marked as `public export`

.

##### Meaning for Data Types¶

For data types, the meanings are:

`export`

the type constructor is exported`public export`

the type constructor and data constructors are exported

##### Meaning for Interfaces¶

For interfaces, the meanings are:

`export`

the interface name is exported`public export`

the interface name, method names and default definitions are exported

##### Propagating Inner Module API’s¶

Additionally, a module can re-export a module it has imported, by using
the `public`

modifier on an `import`

. For example:

```
module A
import B
import public C
```

The module `A`

will export the name `a`

, as well as any public or
abstract names in module `C`

, but will not re-export anything from
module `B`

.

##### Renaming imports¶

Sometimes it is convenient to be able to access the names in another module via a different namespace (typically, a shorter one). For this, you can use import…as. For example:

```
module A
import Data.List as L
```

This module `A`

has access to the exported names from module `Data.List`

,
but can also explicitly access them via the module name `L`

. `import...as`

can also be combined with `import public`

to create a module which exports
a larger API from other sub-modules:

```
module Books
import public Books.Hardback as Books
import public Books.Comic as Books
```

Here, any module which imports `Books`

will have access to the exported
interfaces of `Books.Hardback`

and `Books.Comic`

both under the namespace
`Books`

.

#### Explicit Namespaces¶

Defining a module also defines a namespace implicitly. However,
namespaces can also be given *explicitly*. This is most useful if you
wish to overload names within the same module:

```
module Foo
namespace X
export
test : Int -> Int
test x = x * 2
namespace Y
export
test : String -> String
test x = x ++ x
```

This (admittedly contrived) module defines two functions with fully
qualified names `Foo.X.test`

and `Foo.Y.test`

, which can be
disambiguated by their types:

```
*Foo> test 3
6 : Int
*Foo> test "foo"
"foofoo" : String
```

The export rules, `public export`

and `export`

, are *per namespace*,
not *per file*, so the two `test`

definitions above need the `export`

flag to be visible outside their own namespaces.

#### Parameterised blocks¶

Groups of functions can be parameterised over a number of arguments
using a `parameters`

declaration, for example:

```
parameters (x : Nat, y : Nat)
addAll : Nat -> Nat
addAll z = x + y + z
```

The effect of a `parameters`

block is to add the declared parameters
to every function, type and data constructor within the
block. Specifically, adding the parameters to the front of the
argument list. Outside the block, the parameters must be given
explicitly. The `addAll`

function, when called from the REPL, will
thus have the following type signature.

```
*params> :t addAll
addAll : Nat -> Nat -> Nat -> Nat
```

and the following definition.

```
addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat
addAll x y z = x + y + z
```

Parameters blocks can be nested, and can also include data declarations, in which case the parameters are added explicitly to all type and data constructors. They may also be dependent types with implicit arguments:

```
parameters (y : Nat, xs : Vect x a)
data Vects : Type -> Type where
MkVects : Vect y a -> Vects a
append : Vects a -> Vect (x + y) a
append (MkVects ys) = xs ++ ys
```

To use `Vects`

or `append`

outside the block, we must also give the
`xs`

and `y`

arguments. Here, we can use placeholders for the values
which can be inferred by the type checker:

```
Main> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
"[1, 2, 3, 4, 5, 6]"
```

### Multiplicities¶

Idris 2 is
based on Quantitative Type Theory (QTT), a core language
developed by Bob Atkey and Conor McBride. In practice, this means that every
variable in Idris 2 has a *quantity* associated with it. A quantity is one of:

`0`

, meaning that the variable is*erased*at run time`1`

, meaning that the variable is used*exactly once*at run time*Unrestricted*, which is the same behaviour as Idris 1

We can see the multiplicities of variables by inspecting holes. For example,
if we have the following skeleton definition of `append`

on vectors…

```
append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs
```

…we can look at the hole `append_rhs`

:

```
Main> :t append_rhs
0 m : Nat
0 a : Type
0 n : Nat
ys : Vect m a
xs : Vect n a
-------------------------------------
append_rhs : Vect (plus n m) a
```

The `0`

next to `m`

, `a`

and `n`

mean that they are in scope, but there
will be `0`

occurrences at run-time. That is, it is **guaranteed** that they
will be erased at run-time.

Multiplicities can be explicitly written in function types as follows:

`ignoreN : (0 n : Nat) -> Vect n a -> Nat`

- this function cannot look at`n`

at run time`duplicate : (1 x : a) -> (a, a)`

- this function must use`x`

exactly once (so good luck implementing it, by the way. There is no implementation because it would need to use`x`

twice!)

If there is no multiplicity annotation, the argument is unrestricted.
If, on the other hand, a name is implicitly bound (like `a`

in both examples above)
the argument is erased. So, the above types could also be written as:

`ignoreN : {0 a : _} -> (0 n : Nat) -> Vect n a -> Nat`

`duplicate : {0 a : _} -> (1 x : a) -> (a, a)`

This section describes what this means for your Idris 2 programs in practice, with several examples. In particular, it describes:

- Erasure - how to know what is relevant at run time and what is erased
- Linearity - using the type system to encode
*resource usage protocols* - Pattern Matching on Types - truly first class types

The most important of these for most programs, and the thing you’ll need to know about if converting Idris 1 programs to work with Idris 2, is erasure. The most interesting, however, and the thing which gives Idris 2 much more expressivity, is linearity, so we’ll start there.

#### Linearity¶

The `1`

multiplicity expresses that a variable must be used exactly once.
By “used” we mean either:

- if the variable is a data type or primitive value, it is pattern matched against, ex. by being the subject of a
*case*statement, or a function argument that is pattern matched against, etc., - if the variable is a function, that function is applied (i.e. ran with an argument)

First, we’ll see how this works on some small examples of functions and data types, then see how it can be used to encode resource protocols.

Above, we saw the type of `duplicate`

. Let’s try to write it interactively,
and see what goes wrong. We’ll start by giving the type and a skeleton
definition with a hole

```
duplicate : (1 x : a) -> (a, a)
duplicate x = ?help
```

Checking the type of a hole tells us the multiplicity of each variable in
scope. If we check the type of `?help`

we’ll see that we can’t
use `a`

at run time, and we have to use `x`

exactly once:

```
Main> :t help
0 a : Type
1 x : a
-------------------------------------
help : (a, a)
```

If we use `x`

for one part of the pair…

```
duplicate : (1 x : a) -> (a, a)
duplicate x = (x, ?help)
```

…then the type of the remaining hole tells us we can’t use it for the other:

```
Main> :t help
0 a : Type
0 x : a
-------------------------------------
help : a
```

The same happens if we try defining `duplicate x = (?help, x)`

(try it!).

In order to avoid parsing ambiguities, if you give an explicit multiplicity
for a variable as with the argument to `duplicate`

, you need to give it
a name too. But, if the name isn’t used in the scope of the type, you
can use `_`

instead of a name, as follows:

```
duplicate : (1 _ : a) -> (a, a)
```

The intution behind multiplicity `1`

is that if we have a function with
a type of the following form…

```
f : (1 x : a) -> b
```

…then the guarantee given by the type system is that *if* `f x`

*is used
exactly once, then* `x`

*is used exactly once*. So, if we insist on
trying to define `duplicate`

…:

```
duplicate x = (x, x)
```

…then Idris will complain:

```
pmtype.idr:2:15--8:1:While processing right hand side of Main.duplicate at pmtype.idr:2:1--8:1:
There are 2 uses of linear name x
```

A similar intuition applies for data types. Consider the following types,
`Lin`

which wraps an argument that must be used once, and `Unr`

which
wraps an argument with unrestricted use

```
data Lin : Type -> Type where
MkLin : (1 _ : a) -> Lin a
data Unr : Type -> Type where
MkUnr : a -> Unr a
```

If `MkLin x`

is used once, then `x`

is used once. But if `MkUnr x`

is
used once, there is no guarantee on how often `x`

is used. We can see this a
bit more clearly by starting to write projection functions for `Lin`

and
`Unr`

to extract the argument

```
getLin : (1 _ : Lin a) -> a
getLin (MkLin x) = ?howmanyLin
getUnr : (1 _ : Unr a) -> a
getUnr (MkUnr x) = ?howmanyUnr
```

Checking the types of the holes shows us that, for `getLin`

, we must use
`x`

exactly once (Because the `val`

argument is used once,
by pattern matching on it as `MkLin x`

, and if `MkLin x`

is used once,
`x`

must be used once):

```
Main> :t howmanyLin
0 a : Type
1 x : a
-------------------------------------
howmanyLin : a
```

For `getUnr`

, however, we still have to use `val`

once, again by pattern
matching on it, but using `MkUnr x`

once doesn’t place any restrictions on
`x`

. So, `x`

has unrestricted use in the body of `getUnr`

:

```
Main> :t howmanyUnr
0 a : Type
x : a
-------------------------------------
howmanyUnr : a
```

If `getLin`

has an unrestricted argument…

```
getLin : Lin a -> a
getLin (MkLin x) = ?howmanyLin
```

…then `x`

is unrestricted in `howmanyLin`

:

```
Main> :t howmanyLin
0 a : Type
x : a
-------------------------------------
howmanyLin : a
```

Remember the intuition from the type of `MkLin`

is that if `MkLin x`

is
used exactly once, `x`

is used exactly once. But, we didn’t say that
`MkLin x`

would be used exactly once, so there is no restriction on `x`

.

##### Resource protocols¶

One way to take advantage of being able to express linear usage of an argument
is in defining resource usage protocols, where we can use linearity to ensure
that any unique external resource has only one instance, and we can use
functions which are linear in their arguments to represent state transitions on
that resource. A door, for example, can be in one of two states, `Open`

or
`Closed`

```
data DoorState = Open | Closed
data Door : DoorState -> Type where
MkDoor : (doorId : Int) -> Door st
```

(Okay, we’re just pretending here - imagine the `doorId`

is a reference
to an external resource!)

We can define functions for opening and closing the door which explicitly describe how they change the state of a door, and that they are linear in the door

```
openDoor : (1 d : Door Closed) -> Door Open
closeDoor : (1 d : Door Open) -> Door Closed
```

Remember, the intuition is that if `openDoor d`

is used exactly once,
then `d`

is used exactly once. So, provided that a door `d`

has
multiplicity `1`

when it’s created, we *know* that once we call
`openDoor`

on it, we won’t be able to use `d`

again. Given that
`d`

is an external resource, and `openDoor`

has changed it’s state,
this is a good thing!

We can ensure that any door we create has multiplicity `1`

by
creating them with a `newDoor`

function with the following type

```
newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()
```

That is, `newDoor`

takes a function, which it runs exactly once. That
function takes a door, which is used exactly once. We’ll run it in
`IO`

to suggest that there is some interaction with the outside world
going on when we create the door. Since the multiplicity `1`

means the
door has to be used exactly once, we need to be able to delete the door
when we’re finished

```
deleteDoor : (1 d : Door Closed) -> IO ()
```

So an example correct door protocol usage would be

```
doorProg : IO ()
doorProg
= newDoor $ \d =>
let d' = openDoor d
d'' = closeDoor d' in
deleteDoor d''
```

It’s instructive to build this program interactively, with holes along
the way, and see how the multiplicities of `d`

, `d'`

etc change. For
example

```
doorProg : IO ()
doorProg
= newDoor $ \d =>
let d' = openDoor d in
?whatnow
```

Checking the type of `?whatnow`

shows that `d`

is now spent, but we
still have to use `d'`

exactly once:

```
Main> :t whatnow
0 d : Door Closed
1 d' : Door Open
-------------------------------------
whatnow : IO ()
```

Note that the `0`

multiplicity for `d`

means that we can still *talk*
about it - in particular, we can still reason about it in types - but we
can’t use it again in a relevant position in the rest of the program.
It’s also fine to shadow the name `d`

throughout

```
doorProg : IO ()
doorProg
= newDoor $ \d =>
let d = openDoor d
d = closeDoor d in
deleteDoor d
```

If we don’t follow the protocol correctly - create the door, open it, close it, then delete it - then the program won’t type check. For example, we can try not to delete the door before finishing

```
doorProg : IO ()
doorProg
= newDoor $ \d =>
let d' = openDoor d
d'' = closeDoor d' in
putStrLn "What could possibly go wrong?"
```

This gives the following error:

```
Door.idr:15:19--15:38:While processing right hand side of Main.doorProg at Door.idr:13:1--17:1:
There are 0 uses of linear name d''
```

There’s a lot more to be said about the details here! But, this shows at
a high level how we can use linearity to capture resource usage protocols
at the type level. If we have an external resource which is guaranteed to
be used linearly, like `Door`

, we don’t need to run operations on that
resource in an `IO`

monad, since we’re already enforcing an ordering on
operations and don’t have access to any out of date resource states. This is
similar to the way interactive programs work in
the Clean programming language, and in
fact is how `IO`

is implemented internally in Idris 2, with a special
`%World`

type for representing the state of the outside world that is
always used linearly

```
public export
data IORes : Type -> Type where
MkIORes : (result : a) -> (1 x : %World) -> IORes a
export
data IO : Type -> Type where
MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
```

Having multiplicities in the type system raises several interesting questions, such as:

- Can we use linearity information to inform memory management and, for example, have type level guarantees about functions which will not need to perform garbage collection?
- How should multiplicities be incorporated into interfaces such as
`Functor`

,`Applicative`

and`Monad`

? - If we have
`0`

, and`1`

as multiplicities, why stop there? Why not have`2`

,`3`

and more (like Granule) - What about multiplicity polymorphism, as in the Linear Haskell proposal?
- Even without all of that, what can we do
*now*?

#### Erasure¶

The `1`

multiplicity give us many possibilities in the kinds of
properties we can express. But, the `0`

multiplicity is perhaps more
important in that it allows us to be precise about which values are
relevant at run time, and which are compile time only (that is, which are
erased). Using the `0`

multiplicity means a function’s type now tells us
exactly what it needs at run time.

For example, in Idris 1 you could get the length of a vector as follows

```
vlen : Vect n a -> Nat
vlen {n} xs = n
```

This is fine, since it runs in constant time, but the trade off is that
`n`

has to be available at run time, so at run time we always need the length
of the vector to be available if we ever call `vlen`

. Idris 1 can infer whether
the length is needed, but there’s no easy way for a programmer to be sure.

In Idris 2, we need to state explicitly that `n`

is needed at run time

```
vlen : {n : Nat} -> Vect n a -> Nat
vlen xs = n
```

(Incidentally, also note that in Idris 2, names bound in types are also available in the definition without explicitly rebinding them.)

This also means that when you call `vlen`

, you need the length available. For
example, this will give an error

```
sumLengths : Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen ys
```

Idris 2 reports:

```
vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:
m is not accessible in this context
```

This means that it needs to use `m`

as an argument to pass to `vlen xs`

,
where it needs to be available at run time, but `m`

is not available in
`sumLengths`

because it has multiplicity `0`

.

We can see this more clearly by replacing the right hand side of
`sumLengths`

with a hole…

```
sumLengths : Vect m a -> Vect n a -> Nat
sumLengths xs ys = ?sumLengths_rhs
```

…then checking the hole’s type at the REPL:

```
Main> :t sumLengths_rhs
0 n : Nat
0 a : Type
0 m : Nat
ys : Vect n a
xs : Vect m a
-------------------------------------
sumLengths_rhs : Nat
```

Instead, we need to give bindings for `m`

and `n`

with
unrestricted multiplicity

```
sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen xs
```

Remember that giving no multiplicity on a binder, as with `m`

and `n`

here,
means that the variable has unrestricted usage.

If you’re converting Idris 1 programs to work with Idris 2, this is probably the biggest thing you need to think about. It is important to note, though, that if you have bound implicits, such as…

```
excitingFn : {t : _} -> Coffee t -> Moonbase t
```

…then it’s a good idea to make sure `t`

really is needed, or performance
might suffer due to the run time building the instance of `t`

unnecessarily!

One final note on erasure: it is an error to try to pattern match on an
argument with multiplicity `0`

, unless its value is inferrable from
elsewhere. So, the following definition is rejected

```
badNot : (0 x : Bool) -> Bool
badNot False = True
badNot True = False
```

This is rejected with the error:

```
badnot.idr:2:1--3:1:Attempt to match on erased argument False in
Main.badNot
```

The following, however, is fine, because in `sNot`

, even though we appear
to match on the erased argument `x`

, its value is uniquely inferrable from
the type of the second argument

```
data SBool : Bool -> Type where
SFalse : SBool False
STrue : SBool True
sNot : (0 x : Bool) -> SBool x -> Bool
sNot False SFalse = True
sNot True STrue = False
```

Experience with Idris 2 so far suggests that, most of the time, as long as you’re using unbound implicits in your Idris 1 programs, they will work without much modification in Idris 2. The Idris 2 type checker will point out where you require an unbound implicit argument at run time - sometimes this is both surprising and enlightening!

#### Pattern Matching on Types¶

One way to think about dependent types is to think of them as “first class” objects in the language, in that they can be assigned to variables, passed around and returned from functions, just like any other construct. But, if they’re truly first class, we should be able to pattern match on them too! Idris 2 allows us to do this. For example

```
showType : Type -> String
showType Int = "Int"
showType (List a) = "List of " ++ showType a
showType _ = "something else"
```

We can try this as follows:

```
Main> showType Int
"Int"
Main> showType (List Int)
"List of Int"
Main> showType (List Bool)
"List of something else"
```

Pattern matching on function types is interesting, because the return type
may depend on the input value. For example, let’s add a case to
`showType`

```
showType (Nat -> a) = ?help
```

Inspecting the type of `help`

tells us:

```
Main> :t help
a : Nat -> Type
-------------------------------------
help : String
```

So, the return type `a`

depends on the input value of type `Nat`

, and
we’ll need to come up with a value to use `a`

, for example

```
showType (Nat -> a) = "Function from Nat to " ++ showType (a Z)
```

Note that multiplicities on the binders, and the ability to pattern match
on *non-erased* types mean that the following two types are distinct

```
id : a -> a
notId : {a : Type} -> a -> a
```

In the case of `notId`

, we can match on `a`

and get a function which
is certainly not the identity function

```
notId {a = Int} x = x + 1
notId x = x
```

```
Main> notId 93
94
Main> notId "???"
"???"
```

There is an important consequence of being able to distinguish between relevant
and irrelevant type arguments, which is that a function is *only* parametric in
`a`

if `a`

has multiplicity `0`

. So, in the case of `notId`

, `a`

is
*not* a parameter, and so we can’t draw any conclusions about the way the
function will behave because it is polymorphic, because the type tells us it
might pattern match on `a`

.

On the other hand, it is merely a coincidence that, in non-dependently typed
languages, types are *irrelevant* and get erased, and values are *relevant*
and remain at run time. Idris 2, being based on QTT, allows us to make the
distinction between relevant and irrelevant arguments precise. Types can be
relevant, values (such as the `n`

index to vectors) can be irrelevant.

For more details on multiplicities, see Idris 2: Quantitative Type Theory in Action.

### Packages¶

Idris includes a simple build system for building packages and executables from a named package description file. These files can be used with the Idris compiler to manage the development process.

#### Package Descriptions¶

A package description includes the following:

- A header, consisting of the keyword
`package`

followed by a package name. Package names can be any valid Idris identifier. The iPKG format also takes a quoted version that accepts any valid filename. - Fields describing package contents,
`<field> = <value>`

.

At least one field must be the modules field, where the value is a
comma separated list of modules. For example, given an idris package
`maths`

that has modules `Maths.idr`

, `Maths.NumOps.idr`

,
`Maths.BinOps.idr`

, and `Maths.HexOps.idr`

, the corresponding
package file would be:

```
package maths
modules = Maths
, Maths.NumOps
, Maths.BinOps
, Maths.HexOps
```

Other examples of package files can be found in the `libs`

directory
of the main Idris repository, and in third-party libraries.

#### Using Package files¶

Idris itself is aware about packages, and special commands are
available to help with, for example, building packages, installing
packages, and cleaning packages. For instance, given the `maths`

package from earlier we can use Idris as follows:

`idris2 --build maths.ipkg`

will build all modules in the package`idris2 --install maths.ipkg`

will install the package, making it accessible by other Idris libraries and programs.`idris2 --clean maths.ipkg`

will delete all intermediate code and executable files generated when building.

Once the maths package has been installed, the command line option
`--package maths`

makes it accessible (abbreviated to `-p maths`

).
For example:

```
idris2 -p maths Main.idr
```

#### Package Dependencies Using Atom¶

If you are using the Atom editor and have a dependency on another package,
corresponding to for instance `import Lightyear`

or `import Pruviloj`

,
you need to let Atom know that it should be loaded. The easiest way to
accomplish that is with a .ipkg file. The general contents of an ipkg file
will be described in the next section of the tutorial, but for now here is
a simple recipe for this trivial case:

- Create a folder myProject.
- Add a file myProject.ipkg containing just a couple of lines:

```
package myProject
depends = pruviloj, lightyear
```

- In Atom, use the File menu to Open Folder myProject.

### Example: The Well-Typed Interpreter¶

In this section, we’ll use the features we’ve seen so far to write a
larger example, an interpreter for a simple functional programming
language, with variables, function application, binary operators and
an `if...then...else`

construct. We will use the dependent type
system to ensure that any programs which can be represented are
well-typed.

#### Representing Languages¶

First, let us define the types in the language. We have integers,
booleans, and functions, represented by `Ty`

:

```
data Ty = TyInt | TyBool | TyFun Ty Ty
```

We can write a function to translate these representations to a concrete Idris type — remember that types are first class, so can be calculated just like any other value:

```
interpTy : Ty -> Type
interpTy TyInt = Integer
interpTy TyBool = Bool
interpTy (TyFun a t) = interpTy a -> interpTy t
```

We’re going to define a representation of our language in such a way
that only well-typed programs can be represented. We’ll index the
representations of expressions by their type, **and** the types of
local variables (the context). The context can be represented using
the `Vect`

data type, so we’ll need to import `Data.Vect`

at the top of our
source file:

```
import Data.Vect
```

Expressions are indexed by the types of the local variables, and the type of the expression itself:

```
data Expr : Vect n Ty -> Ty -> Type
```

The full representation of expressions is:

```
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
Stop : HasType FZ (t :: ctxt) t
Pop : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
data Expr : Vect n Ty -> Ty -> Type where
Var : HasType i ctxt t -> Expr ctxt t
Val : (x : Integer) -> Expr ctxt TyInt
Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
Op : (interpTy a -> interpTy b -> interpTy c) ->
Expr ctxt a -> Expr ctxt b -> Expr ctxt c
If : Expr ctxt TyBool ->
Lazy (Expr ctxt a) ->
Lazy (Expr ctxt a) -> Expr ctxt a
```

The code above makes use of the `Vect`

and `Fin`

types from the
base libraries. `Fin`

is available as part of `Data.Vect`

. Throughout,
`ctxt`

refers to the local variable context.

Since expressions are indexed by their type, we can read the typing rules of the language from the definitions of the constructors. Let us look at each constructor in turn.

We use a nameless representation for variables — they are *de Bruijn
indexed*. Variables are represented by a proof of their membership in
the context, `HasType i ctxt T`

, which is a proof that variable `i`

in context `ctxt`

has type `T`

. This is defined as follows:

```
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
Stop : HasType FZ (t :: ctxt) t
Pop : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
```

We can treat *Stop* as a proof that the most recently defined variable
is well-typed, and *Pop n* as a proof that, if the `n`

th most
recently defined variable is well-typed, so is the `n+1`

th. In
practice, this means we use `Stop`

to refer to the most recently
defined variable, `Pop Stop`

to refer to the next, and so on, via
the `Var`

constructor:

```
Var : HasType i ctxt t -> Expr ctxt t
```

So, in an expression `\x. \y. x y`

, the variable `x`

would have a
de Bruijn index of 1, represented as `Pop Stop`

, and `y 0`

,
represented as `Stop`

. We find these by counting the number of
lambdas between the definition and the use.

A value carries a concrete representation of an integer:

```
Val : (x : Integer) -> Expr ctxt TyInt
```

A lambda creates a function. In the scope of a function of type ```
a ->
t
```

, there is a new local variable of type `a`

, which is expressed
by the context index:

```
Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
```

Function application produces a value of type `t`

given a function
from `a`

to `t`

and a value of type `a`

:

```
App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
```

We allow arbitrary binary operators, where the type of the operator informs what the types of the arguments must be:

```
Op : (interpTy a -> interpTy b -> interpTy c) ->
Expr ctxt a -> Expr ctxt b -> Expr ctxt c
```

Finally, `If`

expressions make a choice given a boolean. Each branch
must have the same type, and we will evaluate the branches lazily so
that only the branch which is taken need be evaluated:

```
If : Expr ctxt TyBool ->
Lazy (Expr ctxt a) ->
Lazy (Expr ctxt a) ->
Expr ctxt a
```

#### Writing the Interpreter¶

When we evaluate an `Expr`

, we’ll need to know the values in scope,
as well as their types. `Env`

is an environment, indexed over the
types in scope. Since an environment is just another form of list,
albeit with a strongly specified connection to the vector of local
variable types, we use the usual `::`

and `Nil`

constructors so
that we can use the usual list syntax. Given a proof that a variable
is defined in the context, we can then produce a value from the
environment:

```
data Env : Vect n Ty -> Type where
Nil : Env Nil
(::) : interpTy a -> Env ctxt -> Env (a :: ctxt)
lookup : HasType i ctxt t -> Env ctxt -> interpTy t
lookup Stop (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs
```

Given this, an interpreter is a function which
translates an `Expr`

into a concrete Idris value with respect to a
specific environment:

```
interp : Env ctxt -> Expr ctxt t -> interpTy t
```

The complete interpreter is defined as follows, for reference. For each constructor, we translate it into the corresponding Idris value:

```
interp env (Var i) = lookup i env
interp env (Val x) = x
interp env (Lam sc) = \x => interp (x :: env) sc
interp env (App f s) = interp env f (interp env s)
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e) = if interp env x then interp env t
else interp env e
```

Let us look at each case in turn. To translate a variable, we simply look it up in the environment:

```
interp env (Var i) = lookup i env
```

To translate a value, we just return the concrete representation of the value:

```
interp env (Val x) = x
```

Lambdas are more interesting. In this case, we construct a function which interprets the scope of the lambda with a new value in the environment. So, a function in the object language is translated to an Idris function:

```
interp env (Lam sc) = \x => interp (x :: env) sc
```

For an application, we interpret the function and its argument and apply
it directly. We know that interpreting `f`

must produce a function,
because of its type:

```
interp env (App f s) = interp env f (interp env s)
```

Operators and conditionals are, again, direct translations into the
equivalent Idris constructs. For operators, we apply the function to
its operands directly, and for `If`

, we apply the Idris
`if...then...else`

construct directly.

```
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e) = if interp env x then interp env t
else interp env e
```

#### Testing¶

We can make some simple test functions. Firstly, adding two inputs
`\x. \y. y + x`

is written as follows:

```
add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
```

More interestingly, a factorial function `fact`

(e.g. `\x. if (x == 0) then 1 else (fact (x-1) * x)`

),
can be written as:

```
fact : Expr ctxt (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var Stop) (Val 0))
(Val 1)
(Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
(Var Stop)))
```

#### Running¶

To finish, we write a `main`

program which interprets the factorial
function on user input:

```
main : IO ()
main = do putStr "Enter a number: "
x <- getLine
printLn (interp [] fact (cast x))
```

Here, `cast`

is an overloaded function which converts a value from
one type to another if possible. Here, it converts a string to an
integer, giving 0 if the input is invalid. An example run of this
program at the Idris interactive environment is:

```
$ idris2 interp.idr
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.3.0
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
Main> :exec main
Enter a number: 6
720
```

##### Aside: `cast`

¶

The prelude defines an interface `Cast`

which allows conversion
between types:

```
interface Cast from to where
cast : from -> to
```

It is a *multi-parameter* interface, defining the source type and
object type of the cast. It must be possible for the type checker to
infer *both* parameters at the point where the cast is applied. There
are casts defined between all of the primitive types, as far as they
make sense.

### Views and the “`with`

” rule¶

Warning

NOT UPDATED FOR IDRIS 2 YET

#### Dependent pattern matching¶

Since types can depend on values, the form of some arguments can be
determined by the value of others. For example, if we were to write
down the implicit length arguments to `(++)`

, we’d see that the form
of the length argument was determined by whether the vector was empty
or not:

```
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) {n=Z} [] ys = ys
(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
```

If `n`

was a successor in the `[]`

case, or zero in the `::`

case, the definition would not be well typed.

#### The `with`

rule — matching intermediate values¶

Very often, we need to match on the result of an intermediate
computation. Idris provides a construct for this, the `with`

rule, inspired by views in `Epigram`

[1], which takes account of
the fact that matching on a value in a dependently typed language can
affect what we know about the forms of other values. In its simplest
form, the `with`

rule adds another argument to the function being
defined.

We have already seen a vector filter function. This time, we define it
using `with`

as follows:

```
filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter p [] = ( _ ** [] )
filter p (x :: xs) with (filter p xs)
filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
```

Here, the `with`

clause allows us to deconstruct the result of
`filter p xs`

. The view refined argument pattern ```
filter p (x ::
xs)
```

goes beneath the `with`

clause, followed by a vertical bar
`|`

, followed by the deconstructed intermediate result ```
( _ ** xs'
)
```

. If the view refined argument pattern is unchanged from the
original function argument pattern, then the left side of `|`

is
extraneous and may be omitted:

```
filter p (x :: xs) with (filter p xs)
| ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
```

`with`

clauses can also be nested:

```
foo : Int -> Int -> Bool
foo n m with (n + 1)
foo _ m | 2 with (m + 1)
foo _ _ | 2 | 3 = True
foo _ _ | 2 | _ = False
foo _ _ | _ = False
```

If the intermediate computation itself has a dependent type, then the
result can affect the forms of other arguments — we can learn the form
of one value by testing another. In these cases, view refined argument
patterns must be explicit. For example, a `Nat`

is either even or
odd. If it is even it will be the sum of two equal `Nat`

.
Otherwise, it is the sum of two equal `Nat`

plus one:

```
data Parity : Nat -> Type where
Even : {n : _} -> Parity (n + n)
Odd : {n : _} -> Parity (S (n + n))
```

We say `Parity`

is a *view* of `Nat`

. It has a *covering function*
which tests whether it is even or odd and constructs the predicate
accordingly. Note that we’re going to need access to `n`

at run time, so
although it’s an implicit argument, it has unrestricted multiplicity.

```
parity : (n:Nat) -> Parity n
```

We’ll come back to the definition of `parity`

shortly. We can use it
to write a function which converts a natural number to a list of
binary digits (least significant first) as follows, using the `with`

rule:

```
natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
natToBin (j + j) | Even = False :: natToBin j
natToBin (S (j + j)) | Odd = True :: natToBin j
```

The value of `parity k`

affects the form of `k`

, because the
result of `parity k`

depends on `k`

. So, as well as the patterns
for the result of the intermediate computation (`Even`

and `Odd`

)
right of the `|`

, we also write how the results affect the other
patterns left of the `|`

. That is:

- When
`parity k`

evaluates to`Even`

, we can refine the original argument`k`

to a refined pattern`(j + j)`

according to`Parity (n + n)`

from the`Even`

constructor definition. So`(j + j)`

replaces`k`

on the left side of`|`

, and the`Even`

constructor appears on the right side. The natural number`j`

in the refined pattern can be used on the right side of the`=`

sign. - Otherwise, when
`parity k`

evaluates to`Odd`

, the original argument`k`

is refined to`S (j + j)`

according to`Parity (S (n + n))`

from the`Odd`

constructor definition, and`Odd`

now appears on the right side of`|`

, again with the natural number`j`

used on the right side of the`=`

sign.

Note that there is a function in the patterns (`+`

) and repeated
occurrences of `j`

- this is allowed because another argument has
determined the form of these patterns.

#### Defining `parity`

¶

The definition of `parity`

is a little tricky, and requires some knowledge of
theorem proving (see Section Theorem Proving), but for completeness, here
it is:

```
parity : (n : Nat) -> Parity n
parity Z = Even {n = Z}
parity (S Z) = Odd {n = Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | Even
= rewrite plusSuccRightSucc j j in Even {n = S j}
parity (S (S (S (j + j)))) | Odd
= rewrite plusSuccRightSucc j j in Odd {n = S j}
```

For full details on `rewrite`

in particular, please refer to the theorem
proving tutorial, in Section Theorem Proving.

[1] | Conor McBride and James McKinna. 2004. The view from the left. J. Funct. Program. 14, 1 (January 2004), 69-111. https://doi.org/10.1017/S0956796803004829 |

### Theorem Proving¶

#### Equality¶

Idris allows propositional equalities to be declared, allowing theorems about programs to be stated and proved. An equality type is defined as follows in the Prelude:

```
data Equal : a -> b -> Type where
Refl : Equal x x
```

As a notational convenience, `Equal x y`

can be written as `x = y`

.
Equalities can be proposed between any values of any types, but the only
way to construct a proof of equality is if values actually are equal.
For example:

```
fiveIsFive : 5 = 5
fiveIsFive = Refl
twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl
```

If we try…

```
twoPlusTwoBad : 2 + 2 = 5
twoPlusTwoBad = Refl
```

…then we’ll get an error:

```
Proofs.idr:8:17--10:1:While processing right hand side of Main.twoPlusTwoBad at Proofs.idr:8:1--10:1:
When unifying 4 = 4 and (fromInteger 2 + fromInteger 2) = (fromInteger 5)
Mismatch between:
4
and
5
```

#### The Empty Type¶

There is an empty type, `Void`

, which has no constructors. It is therefore
impossible to construct a canonical element of the empty type. We can therefore
use the empty type to prove that something is impossible, for example zero is
never equal to a successor:

```
disjoint : (n : Nat) -> Z = S n -> Void
disjoint n prf = replace {p = disjointTy} prf ()
where
disjointTy : Nat -> Type
disjointTy Z = ()
disjointTy (S k) = Void
```

Don’t worry if you don’t get all the details of how this works just yet -
essentially, it applies the library function `replace`

, which uses an
equality proof to transform a predicate. Here we use it to transform a
value of a type which can exist, the empty tuple, to a value of a type
which can’t, by using a proof of something which can’t exist.

Once we have an element of the empty type, we can prove anything.
`void`

is defined in the library, to assist with proofs by
contradiction.

```
void : Void -> a
```

#### Proving Theorems¶

When type checking dependent types, the type itself gets *normalised*.
So imagine we want to prove the following theorem about the reduction
behaviour of `plus`

:

```
plusReduces : (n:Nat) -> plus Z n = n
```

We’ve written down the statement of the theorem as a type, in just the same way as we would write the type of a program. In fact there is no real distinction between proofs and programs. A proof, as far as we are concerned here, is merely a program with a precise enough type to guarantee a particular property of interest.

We won’t go into details here, but the Curry-Howard correspondence [1]
explains this relationship. The proof itself is immediate, because
`plus Z n`

normalises to `n`

by the definition of `plus`

:

```
plusReduces n = Refl
```

It is slightly harder if we try the arguments the other way, because
plus is defined by recursion on its first argument. The proof also works
by recursion on the first argument to `plus`

, namely `n`

.

```
plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = Refl
plusReducesZ (S k) = cong S (plusReducesZ k)
```

`cong`

is a function defined in the library which states that equality
respects function application:

```
cong : (f : t -> u) -> a = b -> f a = f b
```

To see more detail on what’s going on, we can replace the recursive call to
`plusReducesZ`

with a hole:

```
plusReducesZ (S k) = cong S ?help
```

Then inspecting the type of the hole at the REPL shows us:

```
Main> :t help
k : Nat
-------------------------------------
help : k = (plus k Z)
```

We can do the same for the reduction behaviour of plus on successors:

```
plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = Refl
plusReducesS (S k) m = cong S (plusReducesS k m)
```

Even for small theorems like these, the proofs are a little tricky to construct in one go. When things get even slightly more complicated, it becomes too much to think about to construct proofs in this “batch mode”.

Idris provides interactive editing capabilities, which can help with building proofs. For more details on building proofs interactively in an editor, see Theorem Proving.

#### Theorems in Practice¶

The need to prove theorems can arise naturally in practice. For example,
previously (Views and the “with” rule) we implemented `natToBin`

using a function
`parity`

:

```
parity : (n:Nat) -> Parity n
```

We provided a definition for `parity`

, but without explanation. We might
have hoped that it would look something like the following:

```
parity : (n:Nat) -> Parity n
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | Even = Even {n=S j}
parity (S (S (S (j + j)))) | Odd = Odd {n=S j}
```

Unfortunately, this fails with a type error:

```
With.idr:26:17--27:3:While processing right hand side of Main.with block in 2419 at With.idr:24:3--27:3:
Can't solve constraint between:
plus j (S j)
and
S (plus j j)
```

The problem is that normalising `S j + S j`

, in the type of `Even`

doesn’t result in what we need for the type of the right hand side of
`Parity`

. We know that `S (S (plus j j))`

is going to be equal to
`S j + S j`

, but we need to explain it to Idris with a proof. We can
begin by adding some *holes* (see Totality and Covering) to the definition:

```
parity : (n:Nat) -> Parity n
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | Even = let result = Even {n=S j} in
?helpEven
parity (S (S (S (j + j)))) | Odd = let result = Odd {n=S j} in
?helpOdd
```

Checking the type of `helpEven`

shows us what we need to prove for the
`Even`

case:

```
j : Nat
result : Parity (S (plus j (S j)))
--------------------------------------
helpEven : Parity (S (S (plus j j)))
```

We can therefore write a helper function to *rewrite* the type to the form
we need:

```
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p
```

The `rewrite ... in`

syntax allows you to change the required type of an
expression by rewriting it according to an equality proof. Here, we have
used `plusSuccRightSucc`

, which has the following type:

```
plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
```

We can see the effect of `rewrite`

by replacing the right hand side of
`helpEven`

with a hole, and working step by step. Beginning with the following:

```
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = ?helpEven_rhs
```

We can look at the type of `helpEven_rhs`

:

```
j : Nat
p : Parity (S (plus j (S j)))
--------------------------------------
helpEven_rhs : Parity (S (S (plus j j)))
```

Then we can `rewrite`

by applying `plusSuccRightSucc j j`

, which gives
an equation `S (j + j) = j + S j`

, thus replacing `S (j + j)`

(or,
in this case, `S (plus j j)`

since `S (j + j)`

reduces to that) in the
type with `j + S j`

:

```
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs
```

Checking the type of `helpEven_rhs`

now shows what has happened, including
the type of the equation we just used (as the type of `_rewrite_rule`

):

```
Main> :t helpEven_rhs
j : Nat
p : Parity (S (plus j (S j)))
-------------------------------------
helpEven_rhs : Parity (S (plus j (S j)))
```

Using `rewrite`

and another helper for the `Odd`

case, we can complete
`parity`

as follows:

```
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p
helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p
parity : (n:Nat) -> Parity n
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | Even = helpEven j (Even {n = S j})
parity (S (S (S (j + j)))) | Odd = helpOdd j (Odd {n = S j})
```

Full details of `rewrite`

are beyond the scope of this introductory tutorial,
but it is covered in the theorem proving tutorial (see Theorem Proving).

#### Totality Checking¶

If we really want to trust our proofs, it is important that they are
defined by *total* functions — that is, a function which is defined for
all possible inputs and is guaranteed to terminate. Otherwise we could
construct an element of the empty type, from which we could prove
anything:

```
-- making use of 'hd' being partially defined
empty1 : Void
empty1 = hd [] where
hd : List a -> a
hd (x :: xs) = x
-- not terminating
empty2 : Void
empty2 = empty2
```

Internally, Idris checks every definition for totality, and we can check at
the prompt with the `:total`

command. We see that neither of the above
definitions is total:

```
Void> :total empty1
Void.empty1 is not covering due to call to function empty1:hd
Void> :total empty2
Void.empty2 is possibly not terminating due to recursive path Void.empty2
```

Note the use of the word “possibly” — a totality check can never be certain due to the undecidability of the halting problem. The check is, therefore, conservative. It is also possible (and indeed advisable, in the case of proofs) to mark functions as total so that it will be a compile time error for the totality check to fail:

```
total empty2 : Void
empty2 = empty2
```

Reassuringly, our proof in Section The Empty Type that the zero and successor constructors are disjoint is total:

```
Main> :total disjoint
Main.disjoint is Total
```

The totality check is, necessarily, conservative. To be recorded as
total, a function `f`

must:

- Cover all possible inputs
- Be
*well-founded*— i.e. by the time a sequence of (possibly mutually) recursive calls reaches`f`

again, it must be possible to show that one of its arguments has decreased. - Not use any data types which are not
*strictly positive* - Not call any non-total functions

##### Directives and Compiler Flags for Totality¶

Warning

Not all of this is implemented yet for Idris 2

By default, Idris allows all well-typed definitions, whether total or not. However, it is desirable for functions to be total as far as possible, as this provides a guarantee that they provide a result for all possible inputs, in finite time. It is possible to make total functions a requirement, either:

- By using the
`--total`

compiler flag. - By adding a
`%default total`

directive to a source file. All definitions after this will be required to be total, unless explicitly flagged as`partial`

.

All functions *after* a `%default total`

declaration are required to
be total. Correspondingly, after a `%default partial`

declaration, the
requirement is relaxed.

Finally, the compiler flag `--warnpartial`

causes to print a warning
for any undeclared partial function.

##### Totality checking issues¶

Please note that the totality checker is not perfect! Firstly, it is
necessarily conservative due to the undecidability of the halting
problem, so many programs which *are* total will not be detected as
such. Secondly, the current implementation has had limited effort put
into it so far, so there may still be cases where it believes a function
is total which is not. Do not rely on it for your proofs yet!

##### Hints for totality¶

In cases where you believe a program is total, but Idris does not agree, it is
possible to give hints to the checker to give more detail for a termination
argument. The checker works by ensuring that all chains of recursive calls
eventually lead to one of the arguments decreasing towards a base case, but
sometimes this is hard to spot. For example, the following definition cannot be
checked as `total`

because the checker cannot decide that `filter (< x) xs`

will always be smaller than `(x :: xs)`

:

```
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
= qsort (filter (< x) xs) ++
(x :: qsort (filter (>= x) xs))
```

The function `assert_smaller`

, defined in the prelude, is intended to
address this problem:

```
assert_smaller : a -> a -> a
assert_smaller x y = y
```

It simply evaluates to its second argument, but also asserts to the
totality checker that `y`

is structurally smaller than `x`

. This can
be used to explain the reasoning for totality if the checker cannot work
it out itself. The above example can now be written as:

```
total
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
= qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
(x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
```

The expression `assert_smaller (x :: xs) (filter (<= x) xs)`

asserts
that the result of the filter will always be smaller than the pattern
`(x :: xs)`

.

In more extreme cases, the function `assert_total`

marks a
subexpression as always being total:

```
assert_total : a -> a
assert_total x = x
```

In general, this function should be avoided, but it can be very useful when reasoning about primitives or externally defined functions (for example from a C library) where totality can be shown by an external argument.

[1] | Timothy G. Griffin. 1989. A formulae-as-type notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ‘90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714 https://doi.acm.org/10.1145/96709.96714 |

### Interactive Editing¶

By now, we have seen several examples of how Idris’ dependent type
system can give extra confidence in a function’s correctness by giving
a more precise description of its intended behaviour in its *type*. We
have also seen an example of how the type system can help with embedded DSL
development by allowing a programmer to describe the type system of an
object language. However, precise types give us more than verification
of programs — we can also use the type system to help write programs which
are *correct by construction*, interactively.

The Idris REPL provides several commands for inspecting and modifying parts of programs, based on their types, such as case splitting on a pattern variable, inspecting the type of a hole, and even a basic proof search mechanism. In this section, we explain how these features can be exploited by a text editor, and specifically how to do so in Vim. An interactive mode for Emacs is also available (though not yet updated for Idris 2).

#### Editing at the REPL¶

Note

The Idris2 repl does not support readline in the interest of
keeping dependencies minimal. Unfortunately this precludes some
niceties such as line editing, persistent history and completion.
A useful work around is to install rlwrap,
this utility provides all the aforementioned features simply by
invoking the Idris2 repl as an argument to the utility `rlwrap idris2`

The REPL provides a number of commands, which we will describe shortly, which generate new program fragments based on the currently loaded module. These take the general form:

```
:command [line number] [name]
```

That is, each command acts on a specific source line, at a specific
name, and outputs a new program fragment. Each command has an
alternative form, which *updates* the source file in-place:

```
:command! [line number] [name]
```

It is also possible to invoke Idris in a mode which runs a REPL command,
displays the result, then exits, using `idris2 --client`

. For example:

```
$ idris2 --client ':t plus'
Prelude.plus : Nat -> Nat -> Nat
$ idris2 --client '2+2'
4
```

A text editor can take advantage of this, along with the editing commands, in order to provide interactive editing support.

#### Editing Commands¶

##### :addclause¶

The `:addclause n f`

command, abbreviated `:ac n f`

, creates a
template definition for the function named `f`

declared on line
`n`

. For example, if the code beginning on line 94 contains:

```
vzipWith : (a -> b -> c) ->
Vect n a -> Vect n b -> Vect n c
```

then `:ac 94 vzipWith`

will give:

```
vzipWith f xs ys = ?vzipWith_rhs
```

The names are chosen according to hints which may be given by a programmer, and then made unique by the machine by adding a digit if necessary. Hints can be given as follows:

```
%name Vect xs, ys, zs, ws
```

This declares that any names generated for types in the `Vect`

family
should be chosen in the order `xs`

, `ys`

, `zs`

, `ws`

.

##### :casesplit¶

The `:casesplit n x`

command, abbreviated `:cs n x`

, splits the
pattern variable `x`

on line `n`

into the various pattern forms it
may take, removing any cases which are impossible due to unification
errors. For example, if the code beginning on line 94 is:

```
vzipWith : (a -> b -> c) ->
Vect n a -> Vect n b -> Vect n c
vzipWith f xs ys = ?vzipWith_rhs
```

then `:cs 96 xs`

will give:

```
vzipWith f [] ys = ?vzipWith_rhs_1
vzipWith f (x :: xs) ys = ?vzipWith_rhs_2
```

That is, the pattern variable `xs`

has been split into the two
possible cases `[]`

and `x :: xs`

. Again, the names are chosen
according to the same heuristic. If we update the file (using
`:cs!`

) then case split on `ys`

on the same line, we get:

```
vzipWith f [] [] = ?vzipWith_rhs_3
```

That is, the pattern variable `ys`

has been split into one case
`[]`

, Idris having noticed that the other possible case ```
y ::
ys
```

would lead to a unification error.

##### :addmissing¶

The `:addmissing n f`

command, abbreviated `:am n f`

, adds the
clauses which are required to make the function `f`

on line `n`

cover all inputs. For example, if the code beginning on line 94 is:

```
vzipWith : (a -> b -> c) ->
Vect n a -> Vect n b -> Vect n c
vzipWith f [] [] = ?vzipWith_rhs_1
```

then `:am 96 vzipWith`

gives:

```
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
```

That is, it notices that there are no cases for empty vectors, generates the required clauses, and eliminates the clauses which would lead to unification errors.

##### :proofsearch¶

The `:proofsearch n f`

command, abbreviated `:ps n f`

, attempts to
find a value for the hole `f`

on line `n`

by proof search,
trying values of local variables, recursive calls and constructors of
the required family. Optionally, it can take a list of *hints*, which
are functions it can try applying to solve the hole. For
example, if the code beginning on line 94 is:

```
vzipWith : (a -> b -> c) ->
Vect n a -> Vect n b -> Vect n c
vzipWith f [] [] = ?vzipWith_rhs_1
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
```

then `:ps 96 vzipWith_rhs_1`

will give

```
[]
```

This works because it is searching for a `Vect`

of length 0, of
which the empty vector is the only possibility. Similarly, and perhaps
surprisingly, there is only one possibility if we try to solve ```
:ps
97 vzipWith_rhs_2
```

:

```
f x y :: vzipWith f xs ys
```

This works because `vzipWith`

has a precise enough type: The
resulting vector has to be non-empty (a `::`

); the first element
must have type `c`

and the only way to get this is to apply `f`

to
`x`

and `y`

; finally, the tail of the vector can only be built
recursively.

##### :makewith¶

The `:makewith n f`

command, abbreviated `:mw n f`

, adds a
`with`

to a pattern clause. For example, recall `parity`

. If line
10 is:

```
parity (S k) = ?parity_rhs
```

then `:mw 10 parity`

will give:

```
parity (S k) with (_)
parity (S k) | with_pat = ?parity_rhs
```

If we then fill in the placeholder `_`

with `parity k`

and case
split on `with_pat`

using `:cs 11 with_pat`

we get the following
patterns:

```
parity (S (plus n n)) | even = ?parity_rhs_1
parity (S (S (plus n n))) | odd = ?parity_rhs_2
```

Note that case splitting has normalised the patterns here (giving
`plus`

rather than `+`

). In any case, we see that using
interactive editing significantly simplifies the implementation of
dependent pattern matching by showing a programmer exactly what the
valid patterns are.

#### Interactive Editing in Vim¶

The editor mode for Vim provides syntax highlighting, indentation and interactive editing support using the commands described above. Interactive editing is achieved using the following editor commands, each of which update the buffer directly:

`\a`

adds a template definition for the name declared on the- current line (using
`:addclause`

).

`\c`

case splits the variable at the cursor (using`:casesplit`

).

`\m`

adds the missing cases for the name at the cursor (using`:addmissing`

).

`\w`

adds a`with`

clause (using`:makewith`

).`\s`

invokes a proof search to solve the hole under the- cursor (using
`:proofsearch`

).

There are also commands to invoke the type checker and evaluator:

`\t`

displays the type of the (globally visible) name under the- cursor. In the case of a hole, this displays the context and the expected type.

`\e`

prompts for an expression to evaluate.`\r`

reloads and type checks the buffer.

Corresponding commands are also available in the Emacs mode. Support
for other editors can be added in a relatively straightforward manner
by using `idris2 -–client`

.
More sophisticated support can be added by using the IDE protocol (yet to
be documented for Idris 2, but which mostly extends to protocol documented for
Idris 1.

### Miscellany¶

In this section we discuss a variety of additional features:

- auto, implicit, and default arguments;
- literate programming; and
- the universe hierarchy.

#### Implicit arguments¶

We have already seen implicit arguments, which allows arguments to be omitted when they can be inferred by the type checker [1], e.g.

```
index : forall a, n . Fin n -> Vect n a -> a
```

##### Auto implicit arguments¶

In other situations, it may be possible to infer arguments not by type
checking but by searching the context for an appropriate value, or
constructing a proof. For example, the following definition of `head`

which requires a proof that the list is non-empty:

```
isCons : List a -> Bool
isCons [] = False
isCons (x :: xs) = True
head : (xs : List a) -> (isCons xs = True) -> a
head (x :: xs) _ = x
```

If the list is statically known to be non-empty, either because its
value is known or because a proof already exists in the context, the
proof can be constructed automatically. Auto implicit arguments allow
this to happen silently. We define `head`

as follows:

```
head : (xs : List a) -> {auto p : isCons xs = True} -> a
head (x :: xs) = x
```

The `auto`

annotation on the implicit argument means that Idris
will attempt to fill in the implicit argument by searching for a value
of the appropriate type. In fact, internally, this is exactly how interface
resolution works. It will try the following, in order:

- Local variables, i.e. names bound in pattern matches or
`let`

bindings, with exactly the right type. - The constructors of the required type. If they have arguments, it will search recursively up to a maximum depth of 100.
- Local variables with function types, searching recursively for the arguments.
- Any function with the appropriate return type which is marked with the
`%hint`

annotation.

In the case that a proof is not found, it can be provided explicitly as normal:

```
head xs {p = ?headProof}
```

##### Default implicit arguments¶

Besides having Idris automatically find a value of a given type, sometimes we
want to have an implicit argument with a specific default value. In Idris, we can
do this using the `default`

annotation. While this is primarily intended to assist
in automatically constructing a proof where auto fails, or finds an unhelpful value,
it might be easier to first consider a simpler case, not involving proofs.

If we want to compute the n’th fibonacci number (and defining the 0th fibonacci number as 0), we could write:

```
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
```

After this definition, `fibonacci 5`

is equivalent to `fibonacci {lag=0} {lead=1} 5`

,
and will return the 5th fibonacci number. Note that while this works, this is not the
intended use of the `default`

annotation. It is included here for illustrative purposes
only. Usually, `default`

is used to provide things like a custom proof search script.

#### Literate programming¶

Like Haskell, Idris supports *literate* programming. If a file has
an extension of `.lidr`

then it is assumed to be a literate file. In
literate programs, everything is assumed to be a comment unless the line
begins with a greater than sign `>`

, for example:

```
> module literate
This is a comment. The main program is below
> main : IO ()
> main = putStrLn "Hello literate world!\n"
```

An additional restriction is that there must be a blank line between a
program line (beginning with `>`

) and a comment line (beginning with
any other character).

#### Cumulativity¶

Warning

NOT YET IN IDRIS 2

Since values can appear in types and *vice versa*, it is natural that
types themselves have types. For example:

```
*universe> :t Nat
Nat : Type
*universe> :t Vect
Vect : Nat -> Type -> Type
```

But what about the type of `Type`

? If we ask Idris it reports:

```
*universe> :t Type
Type : Type 1
```

If `Type`

were its own type, it would lead to an inconsistency due to
Girard’s paradox,
so internally there is a *hierarchy* of types (or *universes*):

```
Type : Type 1 : Type 2 : Type 3 : ...
```

Universes are *cumulative*, that is, if `x : Type n`

we can also have
that `x : Type m`

, as long as `n < m`

. The typechecker generates
such universe constraints and reports an error if any inconsistencies
are found. Ordinarily, a programmer does not need to worry about this,
but it does prevent (contrived) programs such as the following:

```
myid : (a : Type) -> a -> a
myid _ x = x
idid : (a : Type) -> a -> a
idid = myid _ myid
```

The application of `myid`

to itself leads to a cycle in the universe
hierarchy — `myid`

’s first argument is a `Type`

, which cannot be
at a lower level than required if it is applied to itself.

[1] | https://github.com/david-christiansen/idris-type-providers |

### Further Reading¶

Further information about Idris programming, and programming with dependent types in general, can be obtained from various sources:

- Type-Driven Development with Idris by Edwin Brady, available from Manning.
- The Idris web site (https://www.idris-lang.org/) and by asking questions on the mailing list.
- The IRC channel
`#idris`

, on webchat.freenode.net. - The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further user provided information, in particular:
- Examining the prelude and exploring the
`samples`

in the distribution. The Idris 2 source can be found online at: - Existing projects on the
`Idris Hackers`

web space: - Various papers (e.g. [1], [2], and [3]). Although these mostly describe older versions of Idris.

[1] | Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems programming with embedded domain specific languages. In Proceedings of the 14th international conference on Practical Aspects of Declarative Languages (PADL’12), Claudio Russo and Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg, 242-257. DOI=10.1007/978-3-642-27694-1_18 https://dx.doi.org/10.1007/978-3-642-27694-1_18 |

[2] | Edwin C. Brady. 2011. IDRIS —: systems programming meets full dependent types. In Proceedings of the 5th ACM workshop on Programming languages meets program verification (PLPV ‘11). ACM, New York, NY, USA, 43-54. DOI=10.1145/1929529.1929536 https://doi.acm.org/10.1145/1929529.1929536 |

[3] | Edwin C. Brady and Kevin Hammond. 2010. Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation. In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (ICFP ‘10). ACM, New York, NY, USA, 297-308. DOI=10.1145/1863543.1863587 https://doi.acm.org/10.1145/1863543.1863587 |

## Compiling to Executables¶

Note

The documentation for Idris has been published under the Creative
Commons CC0 License. As such to the extent possible under law, *The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.

More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

Idris 2 (the language) is designed to be independent of any specific code generator. Still, since the point of writing a program is to be able to run it, it’s important to know how to do so! By default, Idris compiles to executables via Chez Scheme.

You can compile to an executable as follows, at the REPL:

```
Main> :c execname expr
```

…where `execname`

is the name of the executable file to generate, and
`expr`

is the Idris expression which will be executed. `expr`

must have
type `IO ()`

. This will result in an executable file `execname`

, in a
directory `build/exec`

, relative to the current working directory.

You can also execute expressions directly:

```
Main> :exec expr
```

Again, `expr`

must have type `IO ()`

.

Finally, you can compile to an executable from the command line by adding
the `-o <output file>`

option:

```
$ idris2 hello.idr -o hello
```

This will compile the expression `Main.main`

, generating an executable
`hello`

(with an extension depending on the code generator) in the
`build/exec`

directory.

There are five code generators provided in Idris 2, and (later) there will be a system for plugging in new code generators for a variety of targets. The default is to compile via Chez Scheme, with an alternative via Racket or Gambit. You can set the code generator at the REPL with the :set codegen command, or via the IDRIS2_CG environment variable.

### Chez Scheme Code Generator¶

The Chez Scheme code generator is the default, or it can be accessed via a REPL command:

```
Main> :set cg chez
```

By default, therefore, to run Idris programs you will need to install Chez Scheme. Chez Scheme is open source, and available via most OS package managers.

You can compile an expression `expr`

of type `IO ()`

to an executable as
follows, at the REPL:

```
Main> :c execname expr
```

…where `execname`

is the name of the executable file. This will generate
the following:

- A shell script
`build/exec/execname`

which invokes the program - A subdirectory
`build/exec/execname_app`

which contains all the data necessary to run the program. This includes the Chez Scheme source (`execname.ss`

), the compiled Chez Scheme code (`execname.so`

) and any shared libraries needed for foreign function definitions.

The executable `execname`

is relocatable to any subdirectory, provided that
`execname_app`

is also in the same subdirectory.

You can also execute an expression directly:

```
Main> :exec expr
```

Again, `expr`

must have type `IO ()`

. This will generate a temporary
executable script `_tmpchez`

in the `build/exec`

directory, and execute
that.

Chez Scheme is the default code generator, so if you invoke `idris2`

with the
`-o execname`

flag, it will generate an executable script
`build/exec/execname`

, again with support files in `build/exec/execname_app`

.

#### Chez Directives¶

`--directive extraRuntime=<path>`

Embed Scheme source from

`<path>`

directly into generated output. Can be specified more than once, in which case all given files will be included in the order specified.; extensions.scm (define (my-mul a b) (* a b))

-- Main.idr %foreign "scheme:my-mul" myMul : Int -> Int -> Int

### Racket Code Generator¶

The Racket code generator is accessed via a REPL command:

```
Main> :set cg racket
```

Alternatively, you can set it via the `IDRIS2_CG`

environment variable:

```
$ export IDRIS2_CG=racket
```

You can compile an expression `expr`

of type `IO ()`

to an executable as
follows, at the REPL:

```
Main> :c execname expr
```

…where `execname`

is the name of the executable file. This will generate
the following:

- A shell script
`build/exec/execname`

which invokes the program - A subdirectory
`build/exec/execname_app`

which contains all the data necessary to run the program. This includes the Racket source (`execname.rkt`

), the compiled Racket code (`execname`

or`execname.exe`

on Windows) and any shared libraries needed for foreign function definitions.

The executable `execname`

is relocatable to any subdirectory, provided that
`execname_app`

is also in the same subdirectory.

You can also execute an expression directly:

```
Main> :exec expr
```

Again, `expr`

must have type `IO ()`

. This will generate a temporary
executable script `_tmpracket`

in the `build/exec`

directory, and execute
that, without compiling to a binary first (so the resulting Racket code is
interpreted).

#### Racket Directives¶

`--directive extraRuntime=<path>`

Embed Scheme source from

`<path>`

directly into generated output. Can be specified more than once, in which case all given files will be included in the order specified.; extensions.scm (define (my-mul a b) (* a b))

-- Main.idr %foreign "scheme:my-mul" myMul : Int -> Int -> Int

### Gambit Scheme Code Generator¶

The Gambit Scheme code generator can be accessed via the REPL command:

```
Main> :set cg gambit
```

Alternatively, you can set it via the `IDRIS2_CG`

environment variable:

```
$ export IDRIS2_CG=gambit
```

To run Idris programs with this generator, you will need to install Gambit Scheme. Gambit Scheme is free software, and available via most package managers.

You can compile an expression `expr`

of type `IO ()`

to an executable as
follows, at the REPL:

```
Main> :c execname expr
```

…where `execname`

is the name of the executable file. This will generate
the following:

- An executable binary
`build/exec/execname`

of the program. - A Gambit Scheme source file
`build/exec/execname.scm`

, from which the binary is generated.

You can also execute an expression directly:

```
Main> :exec expr
```

Again, `expr`

must have type `IO ()`

. This will generate a temporary
Scheme file, and execute the Gambit interpreter on it.

#### Gambit Directives¶

`--directive extraRuntime=<path>`

Embed Scheme source from

`<path>`

directly into generated output. Can be specified more than once, in which case all given files will be included in the order specified.; extensions.scm (define (my-mul a b) (* a b))

-- Main.idr %foreign "scheme:my-mul" myMul : Int -> Int -> Int

$ idris2 --codegen chez --directive extraRuntime=/path/to/extensions.scm -o main Main.idr

`--directive C`

Compile to C.

#### Gambit Environment Configurations¶

`GAMBIT_GSC_BACKEND`

The

`GAMBIT_GSC_BACKEND`

variable controls which C compiler Gambit will use during compilation. E.g. to use clang:$ export GAMBIT_GSC_BACKEND=clang

Gambit after version v4.9.3 supports the

`-cc`

option, which configures the compiler backend Gambit will use to build the binary. Currently to get this functionality Gambit needs to be built from source, since it is not yet available in a released version.

### Javascript and Node Code Generators¶

There two javascript code generators `node`

and `javascript`

. There are two
differences between the two: the `javascript`

code generator when called to
output an HTML file will also generate a basic HTML document with the
generated code inside a `<script>`

tag; the other distinction is on the ffi
that will be explained below.

#### Javascript FFI Specifiers¶

There are three main kinds of javascript ffi specifiers `javascript`

,
`node`

and `browser`

. `javascript`

is for foreigns that are available on
node and the browser, `node`

for foreigns that are only available on node and
`browser`

for browser only foreigns.

For `node`

there are two ways of defining a foreign:

```
%foreign "node:lambda: n => process.env[n]"
prim_getEnv : String -> PrimIO (Ptr String)
```

here `lambda`

means that we are providing the definition as a lambda
expression.

```
%foreign "node:lambda:fp=>require('fs').fstatSync(fp.fd, {bigint: true}).size"
prim__fileSize : FilePtr -> PrimIO Int
```

`require`

can be used to import javascript modules.

For completion below an example of a foreign available only with `browser`

codegen:

```
%foreign "browser:lambda:x=>{document.body.innerHTML = x}"
prim__setBodyInnerHTML : String -> PrimIO ()
```

##### Short Example¶

An interesting example is creating a foreign for the setTimeout function:

```
%foreign "javascript:lambda:(callback, delay)=>setTimeout(callback, Number(delay))"
prim__setTimeout : (PrimIO ()) -> Int -> PrimIO ()
setTimeout : HasIO io => IO () -> Int -> io ()
setTimeout callback delay = primIO $ prim__setTimeout (toPrim callback) delay
```

An important note here is that the codegen is using `BigInt`

to represent
idris `Int`

, that’s why we need to apply `Number`

to the `delay`

.

#### Browser Example¶

To build JavaScript aimed to use in the browser, the code must be compiled with the javascript codegen option. The compiler produces a JavaScript or an HTML file. The browser needs an HTML file to load. This HTML file can be created in two ways

- If the
`.html`

suffix is given to the output file the compiler generates an HTML file which includes a wrapping around the generated JavaScript. - If
*no*`.html`

suffix is given, the generated file only contains the JavaScript code. In this case manual wrapping is needed.

Example of the wrapper HTML:

```
<html>
<head><meta charset='utf-8'></head>
<body>
<script type='text/javascript'>
JS code goes here
</script>
</body>
</html>
```

As our intention is to develop something that runs in the browser questions naturally arise:

- How to interact with HTML elements?
- More importantly, when does the generated Idris code start?

##### Starting point of the Idris generated code¶

The generated JavaScript for your program contains an entry point. The `main`

function is compiled
to a JavaScript top-level expression, which will be evaluated during the loading of the `script`

tag and that is the entry point for Idris generated program starting in the browser.

##### Interaction with HTML elements¶

As sketched in the Short Example section, the FFI must be used when interaction happens between Idris
generated code and the rest of the Browser/JS ecosystem. Information handled by the FFI is
separated into two categories. Primitive types in Idris FFI, such as Int, and everything else.
The everything else part is accessed via AnyPtr. The `%foreign`

construction should be used
to give implementation on the JavaScript side. And an Idris function declaration to give `Type`

declaration on the Idris side. The syntax is `%foreign "browser:lambda:js-lambda-expression"`

.
On the Idris side, primitive types and `PrimIO t`

types should be used as parameters,
when defining `%foreign`

. This declaration is a helper function which needs to be called
behind the `primIO`

function. More on this can be found in the FFI chapter.

##### Examples for JavaScript FFI¶

##### console.log¶

```
%foreign "browser:lambda: x => console.log(x)"
prim__consoleLog : String -> PrimIO ()
consoleLog : HasIO io => String -> io ()
consoleLog x = primIO $ prim__consoleLog x
```

String is a primitive type in Idris and it is represented as a JavaScript String. There is no need for any conversion between the Idris and the JavaScript.

##### setInterval¶

```
%foreign "browser:lambda: (a,i)=>setInterval(a,Number(i))"
prim__setInterval : PrimIO () -> Int -> PrimIO ()
setInterval : (HasIO io) => IO () -> Int -> io ()
setInterval a i = primIO $ prim__setInterval (toPrim a) i
```

The `setInterval`

JavaScript function executes the given function in every `x`

millisecond.
We can use Idris generated functions in the callback as far as they have the type `IO ()`

.
But there is a difference in the parameter for the time interval. On the JavaScript side it
expects a number, meanwhile `Int`

in Idris is represented as a `BigInt`

in JavaScript,
for that reason the implementation of the `%foreign`

needs to make the conversion.

##### HTML Dom elements¶

Lets turn our attention to the Dom elements and events. As said above, anything that is not a
primitive type should be handled via the `AnyPtr`

type in the FFI. Anything complex that is
returned by a JavaScript function should be captured in an `AnyPtr`

value. It is advisory to
separate the `AnyPtr`

values into categories.

```
data DomNode = MkNode AnyPtr
%foreign "browser:lambda: () => document.body"
prim__body : () -> PrimIO AnyPtr
body : HasIO io => io DomNode
body = map MkNode $ primIO $ prim__body ()
```

We create a `DomNode`

type which holds an `AnyPtr`

. The `prim__body`

function wraps a
lambda function with no parameters. In the Idris function `body`

we pass an extra `()`

parameter
and the we wrap the result in the `DomNode`

type using the `MkNode`

data constructor.

##### Primitive values originated in JavaScript¶

As a countinuation of the previous example, the `width`

attribute of a DOM element can be
retrieved via the FFI.

```
%foreign "browser:lambda: n=>(BigInt(n.width))"
prim__width : AnyPtr -> PrimIO Int
width : HasIO io => DomNode -> io Int
width (MkNode p) = primIO $ prim__width p
```

Note the `BigInt`

conversation from the JavaScript. The `n.width`

returns a JavaScript
`Number`

and the corresponding `Int`

of Idris is repersented as a `BigInt`

in JavaScript.
The implementor of the FFI function must keep these conversions in mind.

##### Handling JavaScript events¶

```
data DomEvent = MkEvent AnyPtr
%foreign "browser:lambda: (event, callback, node) => node.addEventListener(event, x=>callback(x)())"
prim__addEventListener : String -> (AnyPtr -> PrimIO ()) -> AnyPtr -> PrimIO ()
addEventListener : HasIO io => String -> DomNode -> (DomEvent -> IO ()) -> io ()
addEventListener event (MkNode n) callback =
primIO $ prim__addEventListener event (\ptr => toPrim $ callback $ MkEvent ptr) n
```

In this example shows how to attach an event handler to a particular DOM element. Values of events
are also associated with `AnyPtr`

on the Idris side. To seperate `DomNode`

form `DomEvent`

we create two different types. Also it demonstrates how a simple callback function defined in
Idris can be used on the JavaScript side.

### C with Reference Counting¶

There is an experimental code generator which compiles to an executable via C, using a reference counting garbage collector. This is intended as a lightweight (i.e. minimal dependencies) code generator that can be ported to multiple platforms, especially those with memory constraints.

Performance is not as good as the Scheme based code generators, partly because the reference counting has not yet had any optimisation, and partly because of the limitations of C. However, the main goal is portability: the generated code should run on any platform that supports a C compiler.

This code generator can be accessed via the REPL command:

```
Main> :set cg refc
```

Alternatively, you can set it via the `IDRIS2_CG`

environment variable:

```
$ export IDRIS2_CG=refc
```

The C compiler it invokes is determined by either the `IDRIS2_CC`

or `CC`

environment variables. If neither is set, it uses `cc`

.

This code generator does not yet support :exec, just :c.

Also note that, if you link with any dynamic libraries for interfacing with
C, you will need to arrange for them to be accessible via `LD_LIBRARY_PATH`

when running the executable. The default Idris 2 support libraries are
statically linked.

### Building Idris 2 with new backends¶

The way to extend Idris 2 with new backends is to use it as
a library. The module `Idris.Driver`

exports the function
`mainWithCodegens`

, that takes a list of `(String, Codegen)`

,
starting idris with these codegens in addition to the built-in ones. The first
codegen in the list will be set as the default codegen.

#### Getting started¶

To use Idris 2 as a library you need to install it with (at the top level of the Idris2 repo)

```
make install-api
```

Now create a file containing

```
module Main
import Core.Context
import Compiler.Common
import Idris.Driver
compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmpDir outputDir term file = do coreLift $ putStrLn "I'd rather not."
pure $ Nothing
execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute defs tmpDir term = do coreLift $ putStrLn "Maybe in an hour."
lazyCodegen : Codegen
lazyCodegen = MkCG compile execute
main : IO ()
main = mainWithCodegens [("lazy", lazyCodegen)]
```

Build it with

```
$ idris2 -p idris2 -p contrib -p network Lazy.idr -o lazy-idris2
```

Now you have an idris2 with an added backend.

```
$ ./build/exec/lazy-idris2
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.2.0-bd9498c00
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
With codegen for: lazy
Main>
```

It will not be overly eager to actually compile any code with the new backend though

```
$ ./build/exec/lazy-idris2 --cg lazy Hello.idr -o hello
I'd rather not.
$
```

##### About the directories¶

The code generator can assume that both `tmpDir`

and `outputDir`

exist. `tmpDir`

is intended for temporary files, while `outputDir`

is the location to put the desired
output files. By default, `tmpDir`

and `outputDir`

point to the same directory
(`build/exec`

). The directories can be set from the package description (See Section
Packages) or via command line options (Listed in `idris2 --help`

).

There are also external code generators that aren’t part of the main Idris 2 repository and can be found on Idris 2 wiki:

## Changes since Idris 1¶

Idris 2 is mostly backwards compatible with Idris 1, with some minor exceptions. This document describes the changes, approximately in order of likelihood of encountering them in practice. New features are described at the end, in Section New features.

The Section Type Driven Development with Idris: Updates Required describes how these changes affect the code in the book Type-Driven Development with Idris by Edwin Brady, available from Manning.

Note

The documentation for Idris has been published under the Creative
Commons CC0 License. As such to the extent possible under law, *The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.

More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

### New Core Language: Quantities in Types¶

Idris 2 is based on Quantitative Type Theory (QTT), a core language
developed by Bob Atkey and Conor McBride. In practice, this means that every
variable in Idris 2 has a *quantity* associated with it. A quantity is one of:

`0`

, meaning that the variable is*erased*at run time`1`

, meaning that the variable is used*exactly once*at run time*Unrestricted*, which is the same behaviour as Idris 1

For more details on this, see Section Multiplicities. In practice, this might cause some Idris 1 programs not to type check in Idris 2 due to attempting to use an argument which is erased at run time.

#### Erasure¶

In Idris, names which begin with a lower case letter are automatically bound
as implicit arguments in types, for example in the following skeleton
definition, `n`

, `a`

and `m`

are implicitly bound:

```
append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs
```

One of the difficulties in compiling a dependently typed programming language
is deciding which arguments are used at run time and which can safely be
erased. More importantly, it’s one of the difficulties when programming: how
can a programmer *know* when an argument will be erased?

In Idris 2, a variable’s quantity tells us whether it will be available at
run time or not. We can see the quantities of the variables in scope in
`append_rhs`

by inspecting the hole at the REPL:

```
Main> :t append_rhs
0 m : Nat
0 a : Type
0 n : Nat
ys : Vect m a
xs : Vect n a
-------------------------------------
append_rhs : Vect (plus n m) a
```

The `0`

next to `m`

, `a`

and `n`

mean that they are in scope, but there
will be `0`

occurrences at run-time. That is, it is *guaranteed* that they
will be erased at run-time.

This does lead to some potential difficulties when converting Idris 1 programs, if you are using implicit arguments at run time. For example, in Idris 1 you can get the length of a vector as follows:

```
vlen : Vect n a -> Nat
vlen {n} xs = n
```

This might seem like a good idea, since it runs in constant time and takes
advantage of the type level information, but the trade off is that `n`

has to
be available at run time, so at run time we always need the length of the
vector to be available if we ever call `vlen`

. Idris 1 can infer whether the
length is needed, but there’s no easy way for a programmer to be sure.

In Idris 2, we need to state explicitly that `n`

is needed at run time

```
vlen : {n : Nat} -> Vect n a -> Nat
vlen xs = n
```

(Incidentally, also note that in Idris 2, names bound in types are also available in the definition without explicitly rebinding them.)

This also means that when you call `vlen`

, you need the length available. For
example, this will give an error

```
sumLengths : Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen ys
```

Idris 2 reports:

```
vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:
m is not accessible in this context
```

This means that it needs to use `m`

as an argument to pass to `vlen xs`

,
where it needs to be available at run time, but `m`

is not available in
`sumLengths`

because it has multiplicity `0`

.

We can see this more clearly by replacing the right hand side of
`sumLengths`

with a hole…

```
sumLengths : Vect m a -> Vect n a -> Nat
sumLengths xs ys = ?sumLengths_rhs
```

…then checking the hole’s type at the REPL:

```
Main> :t sumLengths_rhs
0 n : Nat
0 a : Type
0 m : Nat
ys : Vect n a
xs : Vect m a
-------------------------------------
sumLengths_rhs : Nat
```

Instead, we need to give bindings for `m`

and `n`

with
unrestricted multiplicity

```
sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen xs
```

Remember that giving no multiplicity on a binder, as with `m`

and `n`

here,
means that the variable has unrestricted usage.

If you’re converting Idris 1 programs to work with Idris 2, this is probably the biggest thing you need to think about. It is important to note, though, that if you have bound implicits, such as…

```
excitingFn : {t : _} -> Coffee t -> Moonbase t
```

…then it’s a good idea to make sure `t`

really is needed, or performance
might suffer due to the run time building the instance of `t`

unnecessarily!

One final note on erasure: it is an error to try to pattern match on an
argument with multiplicity `0`

, unless its value is inferrable from
elsewhere. So, the following definition is rejected

```
badNot : (0 x : Bool) -> Bool
badNot False = True
badNot True = False
```

This is rejected with the error:

```
badnot.idr:2:1--3:1:Attempt to match on erased argument False in
Main.badNot
```

The following, however, is fine, because in `sNot`

, even though we appear
to match on the erased argument `x`

, its value is uniquely inferrable from
the type of the second argument

```
data SBool : Bool -> Type where
SFalse : SBool False
STrue : SBool True
sNot : (0 x : Bool) -> SBool x -> Bool
sNot False SFalse = True
sNot True STrue = False
```

Experience with Idris 2 so far suggests that, most of the time, as long as you’re using unbound implicits in your Idris 1 programs, they will work without much modification in Idris 2. The Idris 2 type checker will point out where you require an unbound implicit argument at run time - sometimes this is both surprising and enlightening!

#### Linearity¶

Full details on linear arguments with multiplicity `1`

are given in Section
Multiplicities. In brief, the intuition behind multiplicity `1`

is
that if we have a function with a type of the following form…

```
f : (1 x : a) -> b
```

…then the guarantee given by the type system is that *if* `f x`

*is used
exactly once, then* `x`

*is used exactly once* in the process.

### Prelude and `base`

libraries¶

The Prelude in Idris 1 contained a lot of definitions, many of them rarely necessary. The philosophy in Idris 2 is different. The (rather vaguely specified) rule of thumb is that it should contain the basic functions required by almost any non-trivial program.

This is a vague specification since different programmers will consider different things absolutely necessary, but the result is that it contains:

- Anything the elaborator can desugar to (e.g. tuples,
`()`

,`=`

) - Basic types
`Bool`

,`Nat`

,`List`

,`Stream`

,`Dec`

,`Maybe`

,`Either`

- The most important utility functions:
`id`

,`the`

, composition, etc - Interfaces for arithmetic and implementations for the primitives and basic types
- Basic
`Char`

and`String`

manipulation `Show`

,`Eq`

,`Ord`

, and implementations for all types in the prelude- Interfaces and functions for basic proof (
`cong`

,`Uninhabited`

, etc) `Semigroup`

,`Monoid`

`Functor`

,`Applicative`

,`Monad`

and related functions`Foldable`

,`Alternative`

and`Traversable`

`Range`

, for list range syntax- Console
`IO`

Anything which doesn’t fit in here has been moved to the `base`

libraries.
Among other places, you can find some of the functions which used to be
in the prelude in:

`Data.List`

and`Data.Nat`

`Data.Maybe`

and`Data.Either`

`System.File`

and`System.Directory`

, (file management was previously part of the prelude)`Decidable.Equality`

### Smaller Changes¶

#### Ambiguous Name Resolution¶

Idris 1 worked very hard to resolve ambiguous names, by type, even if this involved some complicated interaction with interface resolution. This could sometimes be the cause of long type checking times. Idris 2 simplifies this, at the cost of sometimes requiring more programmer annotations on ambiguous names.

As a general rule, Idris 2 will be able to disambiguate between names which have different concrete return types (such as data constructors), or which have different concrete argument types (such as record projections). It may struggle to resolve ambiguities if one name requires an interface to be resolved. It will postpone resolution if a name can’t be resolved immediately, but unlike Idris 1, it won’t attempt significant backtracking. If you have deeply nested ambiguous names (beyond a small threshold, default 3) Idris 2 will report an error. You can change this threshold with a directive, for example:

```
%ambiguity_depth 10
```

However, in such circumstances it is almost certainly a better idea to disambiguate explicitly.

Indeed in general, if you get an ambiguous name error, the best approach is to give the namespace explicitly. You can also rebind names locally:

```
Main> let (::) = Prelude.(::) in [1,2,3]
[1, 2, 3]
```

One difficulty which remains is resolving ambiguous names where one possibility is an interface method, and another is a concrete top level function. For example, we may have:

```
Prelude.(>>=) : Monad m => m a -> (a -> m b) -> m b
LinearIO.(>>=) : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
```

As a pragmatic choice, if type checking in a context where the more concrete
name is valid (`LinearIO.(>>=)`

here, so if type checking an expression known
to have type `IO t`

for some `t`

), the more concrete name will be chosen.

This is somehow unsatisfying, so we may revisit this in future!

#### Modules, namespaces and export¶

The visibility rules, as controlled by the `private`

, `export`

and
`public export`

modifiers, now refer to the visibility of names from
other *namespaces*, rather than other *files*.

So if you have the following, all in the same file…

```
namespace A
private
aHidden : Int -> Int
aHidden x = x * 2
export
aVisible : Int -> Int
aVisibile x = aHidden x
namespace B
export
bVisible : Int -> Int
bVisible x = aVisible (x * 2)
```

…then `bVisible`

can access `aVisible`

, but not `aHidden`

.

Records are, as before, defined in their own namespace, but fields are always visible from the parent namespace.

Also, module names must now match the filename in which they’re defined, with
the exception of the module `Main`

, which can be defined in a file with
any name.

`%language`

pragmas¶

There are several `%language`

pragmas in Idris 1, which define various
experimental extensions. None of these are available in Idris 2, although
extensions may be defined in the future.

Also removed was the `%access`

pragma for default visibility, use visibility
modifiers on each declaration instead.

`let`

bindings¶

`let`

bindings, i.e. expressions of the form `let x = val in e`

have
slightly different behaviour. Previously, you could rely on the computational
behaviour of `x`

in the scope of `e`

, so type checking could take into
account that `x`

reduces to `val`

. Unfortunately, this leads to complications
with `case`

and `with`

clauses: if we want to preserve the computational
behaviour, we would need to make significant changes to the way `case`

and
`with`

are elaborated.

So, for simplicity and consistency (and, realistically, because I don’t have
enough time to resolve the problem for `case`

and `with`

) the above
expression `let x = val in e`

is equivalent to `(\x => e) val`

.

So, `let`

now effectively generalises a complex subexpression.
If you do need the computational behaviour of a definition, it is now possible
using local function definitions instead - see Section Local function definitions
below.

`auto`

-implicits and Interfaces¶

Interfaces and `auto`

-implicit arguments are similar, in that they invoke an
expression search mechanism to find the value of an argument. In Idris 1,
they were implemented separately, but in Idris 2, they use the same mechanism.
Consider the following *total* definition of `fromMaybe`

:

```
data IsJust : Maybe a -> Type where
ItIsJust : IsJust (Just val)
fromMaybe : (x : Maybe a) -> {auto p : IsJust x} -> a
fromMaybe (Just x) {p = ItIsJust} = x
```

Since interface resolution and `auto`

-implicits are now the same thing,
the type of `fromMaybe`

can be written as:

```
fromMaybe : (x : Maybe a) -> IsJust x => a
```

So now, the constraint arrow `=>`

means that the argument will be found
by `auto`

-implicit search.

When defining a `data`

type, there are ways to control how `auto`

-implicit
search will proceed, by giving options to the data type. For example:

```
data Elem : (x : a) -> (xs : List a) -> Type where
[search x]
Here : Elem x (x :: xs)
There : Elem x xs -> Elem x (y :: xs)
```

The `search x`

option means that `auto`

-implicit search for a value of
type `Elem t ts`

will start as soon as the type checker has resolved the
value `t`

, even if `ts`

is still unknown.

By default, `auto`

-implicit search uses the constructors of a data type
as search hints. The `noHints`

option on a data type turns this behaviour
off.

You can add your own search hints with the `%hint`

option on a function.
For example:

```
data MyShow : Type -> Type where
[noHints]
MkMyShow : (myshow : a -> String) -> MyShow a
%hint
showBool : MyShow Bool
showBool = MkMyShow (\x => if x then "True" else "False")
myShow : MyShow a => a -> String
myShow @{MkMyShow myshow} = myshow
```

In this case, searching for `MyShow Bool`

will find `showBool`

, as we
can see if we try evaluating `myShow True`

at the REPL:

```
Main> myShow True
"True"
```

In fact, this is how interfaces are elaborated. However, `%hint`

should be
used with care. Too many hints can lead to a large search space!

#### Record fields¶

Record fields can now be accessed via a `.`

. For example, if you have:

```
record Person where
constructor MkPerson
firstName, middleName, lastName : String
age : Int
```

and you have a record `fred : Person`

, then you can use `fred.firstName`

to access the `firstName`

field.

#### Totality and Coverage¶

`%default covering`

is now the default status, so all functions must cover
all their inputs unless stated otherwise with a `partial`

annotation, or
switching to `%default partial`

(which is not recommended - use a `partial`

annotation instead to have the smallest possible place where functions are
partial).

#### Build artefacts¶

This is not really a language change, but a change in the way Idris saves
checked files, and still useful to know. All checked modules are now saved in a
directory `build/ttc`

, in the root of the source tree, with the directory
structure following the directory structure of the source. Executables are
placed in `build/exec`

.

#### Packages¶

Dependencies on other packages are now indicated with the `depends`

field,
the `pkgs`

field is no longer recognized. Also, fields with URLS or other
string data (other than module or package names), must be enclosed in double
quotes.
For example:

```
package lightyear
sourceloc = "git://git@github.com:ziman/lightyear.git"
bugtracker = "http://www.github.com/ziman/lightyear/issues"
depends = effects
modules = Lightyear
, Lightyear.Position
, Lightyear.Core
, Lightyear.Combinators
, Lightyear.StringFile
, Lightyear.Strings
, Lightyear.Char
, Lightyear.Testing
```

### New features¶

As well as the change to the core language to use quantitative type theory, described above, there are several other new features.

#### Local function definitions¶

Functions can now be defined locally, using a `let`

block. For example,
`greet`

in the following example, which is defined in the scope of a local
variable `x`

:

```
chat : IO ()
chat
= do putStr "Name: "
x <- getLine
let greet : String -> String
greet msg = msg ++ " " ++ x
putStrLn (greet "Hello")
putStrLn (greet "Bye")
```

These `let`

blocks can be used anywhere (in the middle of `do`

blocks
as above, but also in any function, or in type declarations).
`where`

blocks are now elaborated by translation into a local `let`

.

However, Idris no longer attempts to infer types for functions defined in
`where`

blocks, because this was fragile. This may be reinstated, if we can
come up with a good, predictable approach.

#### Scope of implicit arguments¶

Implicit arguments in a type are now in scope in the body of a definition.
We’ve already seen this above, where `n`

is in scope automatically in the
body of `vlen`

:

```
vlen : {n : Nat} -> Vect n a -> Nat
vlen xs = n
```

This is important to remember when using `where`

blocks, or local definitions,
since the names in scope will also be in scope when declaring the *type* of
the local definition. For example, the following definition, where we attempt
to define our own version of `Show`

for `Vect`

, will fail to type check:

```
showVect : Show a => Vect n a -> String
showVect xs = "[" ++ showBody xs ++ "]"
where
showBody : Vect n a -> String
showBody [] = ""
showBody [x] = show x
showBody (x :: xs) = show x ++ ", " ++ showBody xs
```

This fails because `n`

is in scope already, from the type of `showVect`

,
in the type declaration for `showBody`

, and so the first clause ```
showBody
[]
```

will fail to type check because `[]`

has length `Z`

, not `n`

. We can
fix this by locally binding `n`

:

```
showVect : Show a => Vect n a -> String
showVect xs = "[" ++ showBody xs ++ "]"
where
showBody : forall n . Vect n a -> String
...
```

Or, alternatively, using a new name:

```
showVect : Show a => Vect n a -> String
showVect xs = "[" ++ showBody xs ++ "]"
where
showBody : Vect n' a -> String
...
```

Idris 1 took a different approach here: names which were parameters to data types were in scope, other names were not. The Idris 2 approach is, we hope, more consistent and easier to understand.

#### Function application syntax additions¶

From now on you can utilise the new syntax of function applications:

```
f {x1 [= e1], x2 [= e2], ...}
```

There are three additions here:

- More than one argument can be written in braces, separated with commas:

```
record Dog where
constructor MkDog
name : String
age : Nat
-- Notice that `name` and `age` are explicit arguments.
-- See paragraph (2)
haveADog : Dog
haveADog = MkDog {name = "Max", age = 3}
pairOfStringAndNat : (String, Nat)
pairOfStringAndNat = MkPair {x = "year", y = 2020}
myPlus : (n : Nat) -> (k : Nat) -> Nat
myPlus {n = Z , k} = k
myPlus {n = S n', k} = S (myPlus n' k)
twoPlusTwoIsFour : myPlus {n = 2, k = 2} === 4
twoPlusTwoIsFour = Refl
```

- Arguments in braces can now correspond to explicit, implicit and auto implicit
dependent function types (
`Pi`

types), provided the domain type is named:

```
myPointlessFunction : (exp : String) -> {imp : String} -> {auto aut : String} -> String
myPointlessFunction exp = exp ++ imp ++ aut
callIt : String
callIt = myPointlessFunction {imp = "a ", exp = "Just ", aut = "test"}
```

Order of the arguments doesn’t matter as long as they are in braces and the names are distinct. It is better to stick named arguments in braces at the end of your argument list, because regular unnamed explicit arguments are processed first and take priority:

```
myPointlessFunction' : (a : String) -> String -> (c : String) -> String
myPointlessFunction' a b c = a ++ b ++ c
badCall : String
badCall = myPointlessFunction' {a = "a", c = "c"} "b"
```

This snippet won’t type check, because “b” in `badCall`

is passed first,
although logically we want it to be second.
Idris will tell you that it couldn’t find a spot for `a = "a"`

(because “b” took its place),
so the application is ill-formed.

Thus if you want to use the new syntax, it is worth naming your `Pi`

types.

- Multiple explicit arguments can be “skipped” more easily with the following syntax:

```
f {x1 [= e1], x2 [= e2], ..., xn [= en], _}
```

or

```
f {}
```

in case none of the named arguments are wanted.

Examples:

```
import Data.Nat
record Four a b c d where
constructor MkFour
x : a
y : b
z : c
w : d
firstTwo : Four a b c d -> (a, b)
firstTwo $ MkFour {x, y, _} = (x, y)
-- firstTwo $ MkFour {x, y, z = _, w = _} = (x, y)
dontCare : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
dontCare {} = plusCommutative {}
--dontCare _ _ _ _ _ = plusCommutative _ _
```

Last rule worth noting is the case of named applications with repeated argument names, e.g:

```
data WeirdPair : Type -> Type -> Type where
MkWeirdPair : (x : a) -> (x : b) -> WeirdPair a b
weirdSnd : WeirdPair a b -> b
--weirdSnd $ MkWeirdPair {x, x} = x
-- ^
-- Error: "Non linear pattern variable"
-- But that one is okay:
weirdSnd $ MkWeirdPair {x = _, x} = x
```

In this example the name `x`

is given repeatedly to the `Pi`

types of the data constructor `MkWeirdPair`

.
In order to deconstruct the `WeirdPair a b`

in `weirdSnd`

, while writing the left-hand side of the pattern-matching clause
in a named manner (via the new syntax), we have to rename the first occurrence of `x`

to any fresh name or the `_`

as we did.
Then the definition type checks normally.

In general, duplicate names are bound sequentially on the left-hand side and must be renamed for the pattern expression to be valid.

The situation is similar on the right-hand side of pattern-matching clauses:

```
0 TypeOf : a -> Type
TypeOf _ = a
weirdId : {0 a : Type} -> (1 a : a) -> TypeOf a
weirdId a = a
zero : Nat
-- zero = weirdId { a = Z }
-- ^
-- Error: "Mismatch between: Nat and Type"
-- But this works:
zero = weirdId { a = Nat, a = Z }
```

Named arguments should be passed sequentially in the order they were defined in the `Pi`

types,
regardless of their (imp)explicitness.

#### Better inference¶

In Idris 1, holes (that is, unification variables arising from implicit arguments) were local to an expression, and if they were not resolved while checking the expression, they would not be resolved at all. In Idris 2, they are global, so inference works better. For example, we can now say:

```
test : Vect ? Int
test = [1,2,3,4]
Main> :t test
Main.test : Vect (S (S (S (S Z)))) Int
```

The `?`

, incidentally, differs from `_`

in that `_`

will be bound as
an implicit argument if unresolved after checking the type of `test`

, but
`?`

will be left as a hole to be resolved later. Otherwise, they can be
used interchangeably.

#### Dependent case¶

`case`

blocks were available in Idris 1, but with some restrictions. Having
better inference means that `case`

blocks work more effectively in Idris 2,
and dependent case analysis is supported.

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

The implicit arguments and original values are still available in the body of
the `case`

. Somewhat contrived, but the following is valid:

```
info : {n : _} -> Vect n a -> (Vect n a, Nat)
info xs
= case xs of
[] => (xs, n)
(y :: ys) => (xs, n)
```

#### Record updates¶

Dependent record updates work, provided that all relevant fields are updated
at the same time. Dependent record update is implemented via dependent `case`

blocks rather than by generating a specific update function for each field as
in Idris 1, so you will no longer get mystifying errors when trying to update
dependent records!

For example, we can wrap a vector in a record, with an explicit length field:

```
record WrapVect a where
constructor MkVect
purpose : String
length : Nat
content : Vect length a
```

Then, we can safely update the `content`

, provided we update the `length`

correspondingly:

```
addEntry : String -> WrapVect String -> WrapVect String
addEntry val = record { length $= S,
content $= (val :: ) }
```

Another novelty - new update syntax (previous one still functional):

```
record Three a b c where
constructor MkThree
x : a
y : b
z : c
-- Yet another contrived example
mapSetMap : Three a b c -> (a -> a') -> b' -> (c -> c') -> Three a' b' c'
mapSetMap three@(MkThree x y z) f y' g = {x $= f, y := y', z $= g} three
```

The `record`

keyword has been discarded for brevity, symbol `:=`

replaces `=`

in order to not introduce any ambiguity.

#### Generate definition¶

A new feature of the IDE protocol supports generating complete definitions from a type signature. You can try this at the REPL, for example, given our favourite introductory example…

```
append : Vect n a -> Vect m a -> Vect (n + m) a
```

…assuming this is defined on line 3, you can use the `:gd`

command as
follows:

```
Main> :gd 3 append
append [] ys = ys
append (x :: xs) ys = x :: append xs ys
```

This works by a fairly simple brute force search, which tries searching for a valid right hand side, and case splitting on the left if that fails, but is remarkably effective in a lot of situations. Some other examples which work:

```
my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
my_curry : ((a, b) -> c) -> a -> b -> c
my_uncurry : (a -> b -> c) -> (a, b) -> c
append : Vect n a -> Vect m a -> Vect (n + m) a
lappend : (1 xs : List a) -> (1 ys : List a) -> List a
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
```

This is available in the IDE protocol via the `generate-def`

command.

#### Chez Scheme target¶

The default code generator is, for the moment, Chez Scheme. Racket and Gambit code generators are also
available. There is not yet a way to plug in code generators as in Idris 1,
but this is coming.
To change the code generator, you can use the `:set cg`

command:

```
Main> :set cg racket
```

Early experience shows that both are much faster than the Idris 1 C code generator, in both compile time and execution time (but we haven’t done any formal study on this yet, so it’s just anecdotal evidence).

## Type Driven Development with Idris: Updates Required¶

The code in the book Type-Driven Development with Idris by Edwin Brady, available from Manning, will mostly work in Idris 2, with some small changes as detailed in this document. The updated code is also [going to be] part of the test suite (see tests/typedd-book in the Idris 2 source).

If you are new to Idris, and learning from the book, we recommend working through the first 3-4 chapters with Idris 1, to avoid the need to worry about the changes described here. After that, refer to this document for any necessary changes.

### Chapter 1¶

No changes necessary

### Chapter 2¶

The Prelude is smaller than Idris 1, and many functions have been moved to the base libraries instead. So:

In `Average.idr`

, add:

```
import Data.Strings -- for `words`
import Data.List -- for `length` on lists
```

In `AveMain.idr`

and `Reverse.idr`

add:

```
import System.REPL -- for 'repl'
```

### Chapter 3¶

Unbound implicits have multiplicity 0, so we can’t match on them at run-time.
Therefore, in `Matrix.idr`

, we need to change the type of `createEmpties`

and `transposeMat`

so that the length of the inner vector is available to
match on:

```
createEmpties : {n : _} -> Vect n (Vect 0 elem)
transposeMat : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
```

### Chapter 4¶

For the reasons described above:

- In
`DataStore.idr`

, add`import System.REPL`

and`import Data.Strings`

- In
`SumInputs.idr`

, add`import System.REPL`

- In
`TryIndex.idr`

, add an implicit argument:

```
tryIndex : {n : _} -> Integer -> Vect n a -> Maybe a
```

- In exercise 5 of 4.2, add an implicit argument:

```
sumEntries : Num a => {n : _} -> (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
```

### Chapter 5¶

There is no longer a `Cast`

instance from `String`

to `Nat`

, because its
behaviour of returing Z if the `String`

wasn’t numeric was thought to be
confusing and potentially error prone. Instead, there is `stringToNatOrZ`

in
`Data.Strings`

which at least has a clearer name. So:

In `Loops.idr`

and `ReadNum.idr`

add `import Data.Strings`

and change `cast`

to
`stringToNatOrZ`

In `ReadNum.idr`

, since functions must now be `covering`

by default, add
a `partial`

annotation to `readNumber_v2`

.

### Chapter 6¶

In `DataStore.idr`

and `DataStoreHoles.idr`

, add `import Data.Strings`

and
`import System.REPL`

. Also in `DataStore.idr`

, the `schema`

argument to
`display`

is required for matching, so change the type to:

```
display : {schema : _} -> SchemaType schema -> String
```

In `TypeFuns.idr`

add `import Data.Strings`

### Chapter 7¶

`Abs`

is now a separate interface from `Neg`

. So, change the type of `eval`

to include `Abs`

specifically:

```
eval : (Abs num, Neg num, Integral num) => Expr num -> num
```

Also, take `abs`

out of the `Neg`

implementation for `Expr`

and add an
implementation of `Abs`

as follows:

```
Abs ty => Abs (Expr ty) where
abs = Abs
```

### Chapter 8¶

In `AppendVec.idr`

, add `import Data.Nat`

for the `Nat`

proofs

`cong`

now takes an explicit argument for the function to apply. So, in
`CheckEqMaybe.idr`

change the last case to:

```
checkEqNat (S k) (S j) = case checkEqNat k j of
Nothing => Nothing
Just prf => Just (cong S prf)
```

A similar change is necessary in `CheckEqDec.idr`

.

In `ExactLength.idr`

, the `m`

argument to `exactLength`

is needed at run time,
so change its type to:

```
exactLength : {m : _} ->
(len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
```

A similar change is necessary in `ExactLengthDec.idr`

. Also, `DecEq`

is no
longer part of the prelude, so add `import Decidable.Equality`

.

In `ReverseVec.idr`

, add `import Data.Nat`

for the `Nat`

proofs.

In `Void.idr`

, since functions must now be `covering`

by default, add
a `partial`

annotation to `nohead`

and its helper function `getHead`

.

### Chapter 9¶

- In
`ElemType.idr`

, add`import Decidable.Equality`

- In
`Elem.idr`

, add`import Data.Vect.Elem`

In `Hangman.idr`

:

- Add
`import Data.Strings`

,`import Data.Vect.Elem`

and`import Decidable.Equality`

`removeElem`

pattern matches on`n`

, so it needs to be written in its type:

```
removeElem : {n : _} ->
(value : a) -> (xs : Vect (S n) a) ->
{auto prf : Elem value xs} ->
Vect n a
```

`letters`

is used by`processGuess`

, because it’s passed to`removeElem`

:

```
processGuess : {letters : _} ->
(letter : Char) -> WordState (S guesses) (S letters) ->
Either (WordState guesses (S letters))
(WordState (S guesses) letters)
```

`guesses`

and`letters`

are implicit arguments to`game`

, but are used by the definition, so add them to its type:

```
game : {guesses : _} -> {letters : _} ->
WordState (S guesses) (S letters) -> IO Finished
```

In `RemoveElem.idr`

- Add
`import Data.Vect.Elem`

`removeElem`

needs to be updated as above.

### Chapter 10¶

Lots of changes necessary here, at least when constructing views, due to Idris
2 having a better (that is, more precise and correct!) implementation of
unification, and the rules for recursive `with`

application being tightened up.

In `MergeSort.idr`

, add `import Data.List`

In `MergeSortView.idr`

, add `import Data.List`

, and make the arguments to the
views explicit:

```
mergeSort : Ord a => List a -> List a
mergeSort input with (splitRec input)
mergeSort [] | SplitRecNil = []
mergeSort [x] | SplitRecOne x = [x]
mergeSort (lefts ++ rights) | (SplitRecPair lefts rights lrec rrec)
= merge (mergeSort lefts | lrec)
(mergeSort rights | rrec)
```

In the problem 1 of exercise 10-1, the `rest`

argument of the data
constructor `Exact`

of `TakeN`

must be made explicit.

```
data TakeN : List a -> Type where
Fewer : TakeN xs
Exact : (n_xs : List a) -> {rest : _} -> TakeN (n_xs ++ rest)
```

In `SnocList.idr`

, in `my_reverse`

, the link between `Snoc rec`

and `xs ++ [x]`

needs to be made explicit. Idris 1 would happily decide that `xs`

and `x`

were
the relevant implicit arguments to `Snoc`

but this was little more than a guess
based on what would make it type check, whereas Idris 2 is more precise in
what it allows to unify. So, `x`

and `xs`

need to be explicit arguments to
`Snoc`

:

```
data SnocList : List a -> Type where
Empty : SnocList []
Snoc : (x, xs : _) -> (rec : SnocList xs) -> SnocList (xs ++ [x])
```

Correspondingly, they need to be explicit when matching. For example:

```
my_reverse : List a -> List a
my_reverse input with (snocList input)
my_reverse [] | Empty = []
my_reverse (xs ++ [x]) | (Snoc x xs rec) = x :: my_reverse xs | rec
```

Similar changes are necessary in `snocListHelp`

and `my_reverse_help`

. See
tests/typedd-book/chapter10/SnocList.idr for the full details.

Also, in `snocListHelp`

, `input`

is used at run time so needs to be bound
in the type:

```
snocListHelp : {input : _} ->
(snoc : SnocList input) -> (rest : List a) -> SnocList (input +
```

It’s no longer necessary to give `{input}`

explicitly in the patterns for
`snocListHelp`

, although it’s harmless to do so.

In `IsSuffix.idr`

, the matching has to be written slightly differently. The
recursive with application in Idris 1 probably shouldn’t have allowed this!
Note that the `Snoc`

- `Snoc`

case has to be written first otherwise Idris
generates a case tree splitting on `input1`

and `input2`

instead of the
`SnocList`

objects and this leads to a lot of cases being detected as missing.

```
isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1, snocList input2)
isSuffix _ _ | (Snoc x xs xsrec, Snoc y ys ysrec)
= (x == y) && (isSuffix _ _ | (xsrec, ysrec))
isSuffix _ _ | (Empty, s) = True
isSuffix _ _ | (s, Empty) = False
```

This doesn’t yet get past the totality checker, however, because it doesn’t know about looking inside pairs.

In `DataStore.idr`

: Well this is embarrassing - I’ve no idea how Idris 1 lets
this through! I think perhaps it’s too “helpful” when solving unification
problems. To fix it, add an extra parameter `schema`

to `StoreView`

, and change
the type of `SNil`

to be explicit that the `empty`

is the function defined in
`DataStore`

. Also add `entry`

and `store`

as explicit arguments to `SAdd`

:

```
data StoreView : (schema : _) -> DataStore schema -> Type where
SNil : StoreView schema DataStore.empty
SAdd : (entry, store : _) -> (rec : StoreView schema store) ->
StoreView schema (addToStore entry store)
```

Since `size`

is as explicit argument in the `DataStore`

record, it also needs
to be relevant in the type of `storeViewHelp`

:

```
storeViewHelp : {size : _} ->
(items : Vect size (SchemaType schema)) ->
StoreView schema (MkData size items)
```

In `TestStore.idr`

:

- In
`listItems`

,`empty`

needs to be`DataStore.empty`

to be explicit that you mean the function - In
`filterKeys`

, there is an error in the`SNil`

case, which wasn’t caught because of the type of`SNil`

above. It should be:

```
filterKeys test DataStore.empty | SNil = []
```

### Chapter 11¶

In `Streams.idr`

add `import Data.Stream`

for `iterate`

.

In `Arith.idr`

and `ArithTotal.idr`

, the `Divides`

view now has explicit
arguments for the dividend and remainder, so they need to be explicit in
`bound`

:

```
bound : Int -> Int
bound x with (divides x 12)
bound ((12 * div) + rem) | (DivBy div rem prf) = rem + 1
```

In `ArithCmd.idr`

, update `DivBy`

as above. Also add `import Data.Strings`

for
`Strings.toLower`

.

In `ArithCmd.idr`

, update `DivBy`

and `import Data.Strings`

as above. Also,
since export rules are per-namespace now, rather than per-file, you need to
export `(>>=)`

from the namespaces `CommandDo`

and `ConsoleDo`

.

In `ArithCmdDo.idr`

, since `(>>=)`

is `export`

, `Command`

and `ConsoleIO`

also have to be `export`

.

In `StreamFail.idr`

, add a `partial`

annotation to `labelWith`

.

### Chapter 12¶

For reasons described above: In `ArithState.idr`

, add `import Data.Strings`

.
Also the `(>>=)`

operators need to be set as `export`

since they are in their
own namespaces, and in `getRandom`

, `DivBy`

needs to take additional
arguments `div`

and `rem`

.

In `ArithState.idr`

, since `(>>=)`

is `export`

, `Command`

and `ConsoleIO`

also have to be `export`

.

evalState from Control.Monad.State now takes the `stateType`

argument first.

### Chapter 13¶

In `StackIO.idr`

:

`tryAdd`

pattern matches on`height`

, so it needs to be written in its type:

```
tryAdd : {height : _} -> StackIO height
```

`height`

is also an implicit argument to`stackCalc`

, but is used by the definition, so add it to its type:

```
stackCalc : {height : _} -> StackIO height
```

- In
`StackDo`

namespace, export`(>>=)`

:

```
namespace StackDo
export
(>>=) : StackCmd a height1 height2 ->
(a -> Inf (StackIO height2)) -> StackIO height1
(>>=) = Do
```

In `Vending.idr`

:

- Add
`import Data.Strings`

and change`cast`

to`stringToNatOrZ`

in`strToInput`

- In
`MachineCmd`

type, add an implicit argument to`(>>=)`

data constructor:

```
(>>=) : {state2 : _} ->
MachineCmd a state1 state2 ->
(a -> MachineCmd b state2 state3) ->
MachineCmd b state1 state3
```

- In
`MachineIO`

type, add an implicit argument to`Do`

data constructor:

```
data MachineIO : VendState -> Type where
Do : {state1 : _} ->
MachineCmd a state1 state2 ->
(a -> Inf (MachineIO state2)) -> MachineIO state1
```

`runMachine`

pattern matches on`inState`

, so it needs to be written in its type:

```
runMachine : {inState : _} -> MachineCmd ty inState outState -> IO ty
```

- In
`MachineDo`

namespace, add an implicit argument to`(>>=)`

and export it:

```
namespace MachineDo
export
(>>=) : {state1 : _} ->
MachineCmd a state1 state2 ->
(a -> Inf (MachineIO state2)) -> MachineIO state1
(>>=) = Do
```

`vend`

and`refill`

pattern match on`pounds`

and`chocs`

, so they need to be written in their type:

```
vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs)
```

`pounds`

and`chocs`

are implicit arguments to`machineLoop`

, but are used by the definition, so add them to its type:

```
machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
```

### Chapter 14¶

In `ATM.idr`

:

- Add
`import Data.Strings`

and change`cast`

to`stringToNatOrZ`

in`runATM`

In `Hangman.idr`

, add:

```
import Data.Vect.Elem -- `Elem` now has its own submodule
import Data.Strings -- for `toUpper`
import Data.List -- for `nub`
```

- In
`Loop`

namespace, export`GameLoop`

type and its data constructors:

```
namespace Loop
public export
data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
(>>=) : GameCmd a state1 state2_fn ->
((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) ->
GameLoop b state1 state3_fn
Exit : GameLoop () NotRunning (const NotRunning)
```

`letters`

and`guesses`

are used by`gameLoop`

, so they need to be written in its type:

```
gameLoop : {letters : _} -> {guesses : _} ->
GameLoop () (Running (S guesses) (S letters)) (const NotRunning)
```

- In
`Game`

type, add an implicit argument`letters`

to`InProgress`

data constructor:

```
data Game : GameState -> Type where
GameStart : Game NotRunning
GameWon : (word : String) -> Game NotRunning
GameLost : (word : String) -> Game NotRunning
InProgress : {letters : _} -> (word : String) -> (guesses : Nat) ->
(missing : Vect letters Char) -> Game (Running guesses letters)
```

`removeElem`

pattern matches on`n`

, so it needs to be written in its type:

```
removeElem : {n : _} ->
(value : a) -> (xs : Vect (S n) a) ->
{auto prf : Elem value xs} ->
Vect n a
```

### Chapter 15¶

## Packages¶

Idris includes a system for building packages from a package description file. These files can be used with the Idris compiler to manage the development process of your Idris programs and packages.

### Package Descriptions¶

A package description includes the following:

- A header, consisting of the keyword
`package`

followed by the package name. Package names can be any valid Idris identifier. The iPKG format also takes a quoted version that accepts any valid filename. - Fields describing package contents,
`<field> = <value>`

Packages can describe libraries, executables, or both, and should include
a version number. For library packages,
one field must be the modules field, where the value is a comma separated list
of modules to be installed. For example, a library `test`

which has two modules
`Foo.idr`

and `Bar.idr`

as source files would be written as follows:

```
package test
version = 0.1
modules = Foo, Bar
```

When installed, this will be in a directory `test-0.1`

. If the version
number is missing, it will default to `0`

.

Other examples of package files can be found in the `libs`

directory
of the main Idris repository, and in third-party libraries.

#### Metadata¶

The iPKG format supports additional metadata associated with the package. The added fields are:

`brief = "<text>"`

, a string literal containing a brief description of the package.`version = <version number>`

, a version number, which must be in the form of integers separated by dots (e.g.`1.0`

,`0.3.0`

,`3.1.4.1.5`

etc)`readme = "<file>"`

, location of the README file.`license = "<text>"`

, a string description of the licensing information.`authors = "<text>"`

, the author information.`maintainers = "<text>"`

, Maintainer information.`homepage = "<url>"`

, the website associated with the package.`sourceloc = "<url>"`

, the location of the DVCS where the source can be found.`bugtracker = "<url>"`

, the location of the project’s bug tracker.

#### Directories¶

`sourcedir = "<dir>"`

, the directory to look for Idris source files.`builddir = "<dir>"`

, the directory to put the checked modules and the artefacts from the code generator.`outputdir = "<dir>"`

, the directory where the code generator should output the executable.

#### Common Fields¶

Other common fields which may be present in an `ipkg`

file are:

`executable = <output>`

, which takes the name of the executable file to generate. Executable names can be any valid Idris identifier. the iPKG format also takes a quoted version that accepts any valid filename.Executables are placed in

`build/exec`

by default. The location can be changed by specifying the`outputdir`

field.`main = <module>`

, which takes the name of the main module, and must be present if the`executable`

field is present.`opts = "<idris options>"`

, which allows options to be passed to Idris.`depends = <pkg description> (',' <pkg description>)+`

, a comma separated list of package names that the Idris package requires. The`pkg_description`

is the package name, followed by an optional list of version constraints. Version constraints are separated by`&&`

and can use operators`<`

,`<=`

,`>`

,`>=`

,`==`

. For example, the following are valid package descriptions:`contrib`

(no constraints)`contrib == 0.3.0`

(an exact version constraint)`contrib >= 0.3.0`

(an inclusive lower bound)`contrib >= 0.3.0 && < 0.4`

(an inclusive lower bound, and exclusive upper bound)

#### Comments¶

Package files support comments using the standard Idris singleline `--`

and multiline `{- -}`

format.

### Using Package files¶

Given an Idris package file `test.ipkg`

it can be used with the Idris compiler as follows:

`idris2 --build test.ipkg`

will build all modules in the package`idris2 --install test.ipkg`

will install the package to the global Idris library directory (that is`$PREFIX/idris-<version>/`

), making the modules in its`modules`

field accessible by other Idris libraries and programs. Note that this doesn’t install any executables, just library modules.`idris2 --clean test.ipkg`

will clean the intermediate build files.

Once the test package has been installed, the command line option
`--package test`

makes it accessible (abbreviated to `-p test`

).
For example:

```
idris -p test Main.idr
```

### Where does Idris look for packages?¶

Packages can be installed globally (under `$PREFIX/idris-<version>/`

as
described above) or locally (under a `depends`

subdirectory in the top level
working directory of a project).
Packages specified using `-p pkgname`

or with the `depends`

field of a
package will then be located as follows:

- First, Idris looks in
`depends/pkgname-version`

, for a package which satsifies the version constraint. - If no package is found locally, Idris looks in
`$PREFIX/idris-<version>/pkgname-version`

.

In each case, if more than one version satisfies the constraint, it will choose the one with the highest version number.

## Structuring Idris 2 Applications¶

A tutorial on structuring Idris 2 applications using `Control.App`

.

Note

*The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.

Idris applications have `main : IO ()`

as an entry point. A type `IO a`

is
a description of interactive actions which produce a value of type `a`

. This
is fine for primitives, but `IO`

does not support exceptions so we have to be
explicit about how an operation handles failure. Also, if we do
want to support exceptions, we also want to explain how exceptions and linearity
(see Section Multiplicities) interact.

In this tutorial, we describe a parameterised type `App`

and a related
parameterised type `App1`

, which together allow us to structure larger
applications, taking into account both exceptions and linearity. The aims of
`App`

and `App1`

are that they should:

- make it possible to express what interactions a function does, in its type, without too much notational overhead.
- have little or no performance overhead compared to writing in
*IO*. - be compatible with other libraries and techniques for describing effects, such as algebraic effects or monad transformers.
- be sufficiently easy to use and performant that it can be the basis of
*all*libraries that make foreign function calls, much as*IO*is in Idris 1 and Haskell - be compatible with linear types, meaning that they should express whether a section of code is linear (guaranteed to execute exactly once without throwing an exception) or whether it might throw an exception.

We begin by introducing `App`

, with some small example
programs, then show how to extend it with exceptions, state, and other
interfaces.

### Introducing App¶

`App`

is declared as below, in a module `Control.App`

, which is part of
the `base`

libraries.
It is parameterised by an implicit
`Path`

(which states whether the program’s execution path
is linear or might throw
exceptions), which has a `default`

value that the program
might throw, and a `List Error`

(which gives a list of exception types which can be thrown, `Error`

is
a synonym for `Type`

):

```
data App : {default MayThrow l : Path} ->
(es : List Error) -> Type -> Type
```

It serves the same purpose as `IO`

, but supports throwing and catching
exceptions, and allows us to define more constrained interfaces parameterised
by the list of errors `es`

.
e.g. a program which supports console IO:

```
hello : Console es => App es ()
hello = putStrLn "Hello, App world!"
```

We can use this in a complete program as follows:

```
module Main
import Control.App
import Control.App.Console
hello : Console es => App es ()
hello = putStrLn "Hello, App world!"
main : IO ()
main = run hello
```

Or, a program which supports console IO and carries an `Int`

state,
labelled `Counter`

:

```
data Counter : Type where
helloCount : (Console es, State Counter Int es) => App es ()
helloCount = do c <- get Counter
put Counter (c + 1)
putStrLn "Hello, counting world"
c <- get Counter
putStrLn ("Counter " ++ show c)
```

To run this as part of a complete program, we need to initialise the state.

```
main : IO ()
main = run (new 93 helloCount)
```

For convenience, we can list multiple interfaces in one go, using a function
`Has`

, defined in `Control.App`

, to compute the interface constraints:

```
helloCount : Has [Console, State Counter Int] es => App es ()
0 Has : List (a -> Type) -> a -> Type
Has [] es = ()
Has (e :: es') es = (e es, Has es' es)
```

The purpose of `Path`

is to state whether a program can throw
exceptions, so that we can know where it is safe to reference linear
resources. It is declared as follows:

```
data Path = MayThrow | NoThrow
```

The type of `App`

states that `MayThrow`

is the default.
We expect this to be the most
common case. After all, realistically, most operations have possible failure
modes, especially those which interact with the outside world.

The `0`

on the declaration of `Has`

indicates that it can only
be run in an erased context, so it will never be run at run-time.
To run an `App`

inside `IO`

, we use an initial
list of errors `Init`

(recall that an `Error`

is a
synonym for `Type`

):

```
Init : List Error
Init = [Void]
run : App {l} Init a -> IO a
```

Generalising the `Path`

parameter with `l`

means that we can invoke `run`

for any application, whether the `Path`

is `NoThrow`

or `MayThrow`

. But, in practice, all applications
given to `run`

will not throw at the top level, because the only
exception type available is the empty type `Void`

. Any exceptions
will have been introduced and handled inside the `App`

.

### Exceptions and State¶

`Control.App`

is primarily intended to make it easier to manage the common
cases of applications with exceptions and state. We can throw and catch
exceptions listed in the list of errors (the `es`

parameter to `App`

) and
introduce new global state.

#### Exceptions¶

The `List Error`

is a list of error types, usable via the
`Exception`

interface defined in `Control.App`

:

```
interface Exception err e where
throw : err -> App e a
catch : App e a -> (err -> App e a) -> App e a
```

We can use `throw`

and `catch`

for some exception type
`err`

as long as the exception type exists in the list of errors. This is
checked with the `HasErr`

predicate, also defined in `Control.App`

:

```
data HasErr : Error -> List Error -> Type where
Here : HasErr e (e :: es)
There : HasErr e es -> HasErr e (e' :: es)
HasErr err es => Exception err es where ...
```

Note the `HasErr`

constraint on `Exception`

: this is one place
where it is notationally convenient that the `auto`

implicit mechanism
and the interface resolution mechanism are identical in Idris 2.
Finally, we can introduce new exception types via `handle`

, which runs a
block of code which might throw, handling any exceptions:

```
handle : App (err :: e) a ->
(onok : a -> App e b) ->
(onerr : err -> App e b) -> App e b
```

#### Adding State¶

Applications will typically need to keep track of state, and we support
this primitively in `App`

using a `State`

type, defined in
`Control.App`

:

```
data State : (tag : a) -> Type -> List Error -> Type
```

The `tag`

is used purely to distinguish between different states,
and is not required at run-time, as explicitly stated in the types of
`get`

and `put`

, which are used to access and update a state:

```
get : (0 tag : _) -> State tag t e => App {l} e t
put : (0 tag : _) -> State tag t e => (1 val : t) -> App {l} e ()
```

These use an `auto`

-implicit to pass around
a `State`

with the relevant `tag`

implicitly, so we refer
to states by tag alone. In `helloCount`

earlier, we used an empty type
`Counter`

as the tag:

```
data Counter : Type where -- complete definition
```

The list of errors `e`

is used to ensure that
states are only usable in the list of errors in which they are introduced.
States are introduced using `new`

:

```
new : t -> (1 p : State tag t e => App {l} e a) -> App {l} e a
```

Note that the type tells us `new`

runs the program with the state
exactly once.
Rather than using `State`

and `Exception`

directly, however,
we typically use interfaces to constrain the operations which are allowed
in a list of errors. Internally, `State`

is implemented via an
`IORef`

, primarily for performance reasons.

### Defining Interfaces¶

The only way provided by `Control.App`

to run an `App`

is
via the `run`

function, which takes a concrete list of errors
`Init`

.
All concrete extensions to this list of errors are via either `handle`

,
to introduce a new exception, or `new`

, to introduce a new state.
In order to compose `App`

programs effectively, rather than
introducing concrete exceptions and state in general, we define interfaces for
collections of operations which work in a specific list of errors.

#### Example: Console I/O¶

We have seen an initial example using the `Console`

interface,
which is declared as follows, in `Control.App.Console`

:

```
interface Console e where
putStr : String -> App {l} e ()
getStr : App {l} e String
```

It provides primitives for writing to and reading from the console, and
generalising the path parameter to `l`

means that neither can
throw an exception, because they have to work in both the `NoThrow`

and `MayThrow`

contexts.

To implement this for use in a top level `IO`

program, we need access to primitive `IO`

operations.
The `Control.App`

library defines a primitive interface for this:

```
interface PrimIO e where
primIO : IO a -> App {l} e a
fork : (forall e' . PrimIO e' => App {l} e' ()) -> App e ()
```

We use `primIO`

to invoke an `IO`

function. We also have a `fork`

primitive, which starts a new thread in a new list of errors supporting
`PrimIO`

. Note that `fork`

starts a new list of errors `e'`

so that states
are only available in a single thread.

There is an implementation of `PrimIO`

for a list of errors which can
throw the empty type as an exception. This means that if `PrimIO`

is the only interface available, we cannot throw an exception, which is
consistent with the definition of `IO`

. This also allows us to
use `PrimIO`

in the initial list of errors `Init`

.

```
HasErr Void e => PrimIO e where ...
```

Given this, we can implement `Console`

and run our `hello`

program in `IO`

. It is implemented as follows in `Control.App.Console`

:

```
PrimIO e => Console e where
putStr str = primIO $ putStr str
getStr = primIO $ getLine
```

#### Example: File I/O¶

Console I/O can be implemented directly, but most I/O operations can fail.
For example, opening a file can fail for several reasons: the file does not
exist; the user has the wrong permissions, etc. In Idris, the `IO`

primitive reflects this in its type:

```
openFile : String -> Mode -> IO (Either FileError File)
```

While precise, this becomes unwieldy when there are long sequences of
`IO`

operations. Using `App`

, we can provide an interface
which throws an exception when an operation fails, and guarantee that any
exceptions are handled at the top level using `handle`

.
We begin by defining the `FileIO`

interface, in `Control.App.FileIO`

:

```
interface Has [Exception IOError] e => FileIO e where
withFile : String -> Mode -> (onError : IOError -> App e a) ->
(onOpen : File -> App e a) -> App e a
fGetStr : File -> App e String
fPutStr : File -> String -> App e ()
fEOF : File -> App e Bool
```

We use resource bracketing - passing a function to `withFile`

for working
with the opened file - rather than an explicit `open`

operation,
to open a file, to ensure that the file handle is cleaned up on
completion.

One could also imagine an interface using a linear resource for the file, which
might be appropriate in some safety critical contexts, but for most programming
tasks, exceptions should suffice.
All of the operations can fail, and the interface makes this explicit by
saying we can only implement `FileIO`

if the list of errors supports
throwing and catching the `IOError`

exception. `IOError`

is defined
in `Control.App`

.

For example, we can use this interface to implement `readFile`

, throwing
an exception if opening the file fails in `withFile`

:

```
readFile : FileIO e => String -> App e String
readFile f = withFile f Read throw $ \h =>
do content <- read [] h
pure (concat content)
where
read : List String -> File -> App e (List String)
read acc h = do eof <- fEOF h
if eof then pure (reverse acc)
else do str <- fGetStr h
read (str :: acc) h
```

Again, this is defined in `Control.App.FileIO`

.

To implement `FileIO`

, we need access to the primitive operations
via `PrimIO`

, and the ability to throw exceptions if any of the
operations fail. With this, we can implement `withFile`

as follows,
for example:

```
Has [PrimIO, Exception IOError] e => FileIO e where
withFile fname m onError proc
= do Right h <- primIO $ openFile fname m
| Left err => onError (FileErr (toFileEx err))
res <- catch (proc h) onError
pure res
...
```

Given this implementation of `FileIO`

, we can run `readFile`

,
provided that we wrap it in a top level `handle`

function to deal
with any errors thrown by `readFile`

:

```
readMain : String -> App Init ()
readMain fname = handle (readFile fname)
(\str => putStrLn $ "Success:\n" ++ show str)
(\err : IOError => putStrLn $ "Error: " ++ show err)
```

### Linear Resources¶

We have introduced `App`

for writing
interactive programs, using interfaces to constrain which operations are
permitted, but have not yet seen the `Path`

parameter in action.
Its purpose is to constrain when programs can throw exceptions,
to know where linear resource usage is allowed. The bind operator
for `App`

is defined as follows (not via `Monad`

):

```
data SafeBind : Path -> (l' : Path) -> Type where
SafeSame : SafeBind l l
SafeToThrow : SafeBind NoThrow MayThrow
(>>=) : SafeBind l l' =>
App {l} e a -> (a -> App {l=l'} e b) -> App {l=l'} e b
```

The intuition behind this type is that, when sequencing two `App`

programs:

- if the first action might throw an exception, then the whole program might throw.
- if the first action cannot throw an exception, the second action can still throw, and the program as a whole can throw.
- if neither action can throw an exception, the program as a whole cannot throw.

The reason for the detail in the type is that it is useful to be able to
sequence programs with a different `Path`

, but in doing so, we must
calculate the resulting `Path`

accurately.
Then, if we want to sequence subprograms with linear variables,
we can use an alternative bind operator which guarantees to run the
continuation exactly once:

```
bindL : App {l=NoThrow} e a ->
(1 k : a -> App {l} e b) -> App {l} e b
```

To illustrate the need for `bindL`

, we can try writing a program which
tracks the state of a secure data store, which requires logging in before
reading the data.

#### Example: a data store requiring a login¶

Many software components rely on some form of state, and there may be operations which are only valid in specific states. For example, consider a secure data store in which a user must log in before getting access to some secret data. This system can be in one of two states:

`LoggedIn`

, in which the user is allowed to read the secret`LoggedOut`

, in which the user has no access to the secret

We can provide commands to log in, log out, and read the data, as illustrated in the following diagram:

The `login`

command, if it succeeds, moves the overall system state from
`LoggedOut`

to `LoggedIn`

. The `logout`

command moves the state from
`LoggedIn`

to `LoggedOut`

. Most importantly, the `readSecret`

command
is only valid when the system is in the `LoggedIn`

state.

We can represent the state transitions using functions with linear types. To begin, we define an interface for connecting to and disconnecting from a store:

```
interface StoreI e where
connect : (1 prog : (1 d : Store LoggedOut) ->
App {l} e ()) -> App {l} e ()
disconnect : (1 d : Store LoggedOut) -> App {l} e ()
```

Neither `connect`

nor `disconnect`

throw, as shown by
generalising over `l`

. Once we
have a connection, we can use the following functions to
access the resource directly:

```
data Res : (a : Type) -> (a -> Type) -> Type where
(#) : (val : a) -> (1 resource : r val) -> Res a r
login : (1 s : Store LoggedOut) -> (password : String) ->
Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
logout : (1 s : Store LoggedIn) -> Store LoggedOut
readSecret : (1 s : Store LoggedIn) ->
Res String (const (Store LoggedIn))
```

`Res`

is defined in the Prelude, since it is commonly useful. It is a
dependent pair type, which associates a value with a linear resource.
We’ll leave the other definitions abstract, for the purposes of this
introductory example.

The following listing shows a complete program accessing the store, which
reads a password, accesses the store if the password is correct and prints the
secret data. It uses `let (>>=) = bindL`

to redefine
`do`

-notation locally.

```
storeProg : Has [Console, StoreI] e => App e ()
storeProg = let (>>=) = bindL in
do putStr "Password: "
password <- getStr
connect $ \s =>
do let True # s = login s password
| False # s => do putStrLn "Wrong password"
disconnect s
let str # s = readSecret s
putStrLn $ "Secret: " ++ show str
let s = logout s
disconnect s
```

If we omit the `let (>>=) = bindL`

, it will use the default
`(>>=)`

operator, which allows the continuation to be run multiple
times, which would mean that `s`

is not guaranteed to be accessed
linearly, and `storeProg`

would not type check.
We can safely use `getStr`

and `putStr`

because they
are guaranteed not to throw by the `Path`

parameter in their types.

#### App1: Linear Interfaces¶

Adding the `bindL`

function to allow locally rebinding the
`(>>=)`

operator allows us to combine existing linear resource
programs with operations in `App`

- at least, those that don’t throw.
It would nevertheless be nice to interoperate more directly with `App`

.
One advantage of defining interfaces is that we can provide multiple
implementations for different contexts, but our implementation of the
data store uses primitive functions (which we left undefined in any case)
to access the store.

To allow control over linear resources, `Control.App`

provides an alternative
parameterised type `App1`

:

```
data App1 : {default One u : Usage} ->
(es : List Error) -> Type -> Type
```

There is no need for a `Path`

argument, since linear programs can
never throw. The `Usage`

argument states whether the value
returned is to be used once, or has unrestricted usage, with
the default in `App1`

being to use once:

```
data Usage = One | Any
```

The main difference from `App`

is the `(>>=)`

operator, which
has a different multiplicity for the variable bound by the continuation
depending on the usage of the first action:

```
Cont1Type : Usage -> Type -> Usage -> List Error -> Type -> Type
Cont1Type One a u e b = (1 x : a) -> App1 {u} e b
Cont1Type Any a u e b = (x : a) -> App1 {u} e b
(>>=) : {u : _} -> (1 act : App1 {u} e a) ->
(1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b
```

`Cont1Type`

returns a continuation which uses the argument linearly,
if the first `App1`

program has usage `One`

, otherwise it
returns a continuation where argument usage is unrestricted. Either way,
because there may be linear resources in scope, the continuation is
run exactly once and there can be no exceptions thrown.

Using `App1`

, we can define all of the data store operations in a
single interface, as shown in the following listing.
Each operation other than `disconnect`

returns a linear resource.

```
interface StoreI e where
connect : App1 e (Store LoggedOut)
login : (1 d : Store LoggedOut) -> (password : String) ->
App1 e (Res Bool (\ok => Store (if ok then LoggedIn
else LoggedOut))
logout : (1 d : Store LoggedIn) -> App1 e (Store LoggedOut)
readSecret : (1 d : Store LoggedIn) ->
App1 e (Res String (const (Store LoggedIn)))
disconnect : (1 d : Store LoggedOut) -> App {l} e ()
```

We can explicitly move between `App`

and `App1`

:

```
app : (1 p : App {l=NoThrow} e a) -> App1 {u=Any} e a
app1 : (1 p : App1 {u=Any} e a) -> App {l} e a
```

We can run an `App`

program using `app`

, inside `App1`

,
provided that it is guaranteed not to throw. Similarly, we can run an
`App1`

program using `app1`

, inside `App`

, provided that
the value it returns has unrestricted usage. So, for example, we can
write:

```
storeProg : Has [Console, StoreI] e => App e ()
storeProg = app1 $ do
store <- connect
app $ putStr "Password: "
?what_next
```

This uses `app1`

to state that the body of the program is linear,
then `app`

to state that the `putStr`

operation is in
`App`

. We can see that `connect`

returns a linear resource
by inspecting the hole `what_next`

, which also shows that we are
running inside `App1`

:

```
0 e : List Type
1 store : Store LoggedOut
-------------------------------------
what_next : App1 e ()
```

For completeness, one way to implement the interface is as follows, with hard coded password and internal data:

```
Has [Console] e => StoreI e where
connect
= do app $ putStrLn "Connect"
pure1 (MkStore "xyzzy")
login (MkStore str) pwd
= if pwd == "Mornington Crescent"
then pure1 (True # MkStore str)
else pure1 (False # MkStore str)
logout (MkStore str) = pure1 (MkStore str)
readSecret (MkStore str) = pure1 (str # MkStore str)
disconnect (MkStore _)
= putStrLn "Disconnect"
```

Then we can run it in `main`

:

```
main : IO ()
main = run storeProg
```

## Foreign Function Interface¶

Note

*The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.

Idris 2 is designed to support multiple code generators. The default target is Chez Scheme, with Racket and Gambit code generators also supported. However, the intention is, as with Idris 1, to support multiple targets on multiple platforms, including e.g. JavaScript, JVM, .NET, and others yet to be invented. This makes the design of a foreign function interface (FFI), which calls functions in other languages, a little challenging, since ideally it will support all possible targets!

To this end, the Idris 2 FFI aims to be flexible and adaptable, while still supporting most common requirements without too much need for “glue” code in the foreign language.

### FFI Overview¶

Foreign functions are declared with the `%foreign`

directive, which takes the
following general form:

```
%foreign [specifiers]
name : t
```

The specifier is an Idris `String`

which says in which language the foreign
function is written, what it’s called, and where to find it. There may be more
than one specifier, and a code generator is free to choose any specifier it
understands - or even ignore the specifiers completely and use their own
approach. In general, a specifier has the form “Language:name,library”. For
example, in C:

```
%foreign "C:puts,libc"
puts : String -> PrimIO Int
```

It is up to specific code generators to decide how to locate the function and the library. In this document, we will assume the default Chez Scheme code generator (the examples also work with the Racket or Gambit code generator) and that the foreign language is C.

#### Scheme Sidenote¶

Scheme foreign specifiers can be written to target particular flavors.

The following example shows a foreign declaration that allocates memory in a
way specific to the choice of code generator. In this example there is no
general scheme specifier present that matches every flavor, e.g.
`scheme:foo`

, so it will only match the specific flavors listed:

```
%foreign "scheme,chez:foreign-alloc"
"scheme,racket:malloc"
"C:malloc,libc"
allocMem : (bytes : Int) -> PrimIO AnyPtr
```

Note

If your backend (code generator) is not specified but defines a C FFI
it will be able to make use of the `C:malloc,libc`

specifier.

#### FFI Example¶

As a running example, we are going to work with a small C file. Save the
following content to a file `smallc.c`

```
#include <stdio.h>
int add(int x, int y) {
return x+y;
}
int addWithMessage(char* msg, int x, int y) {
printf("%s: %d + %d = %d\n", msg, x, y, x+y);
return x+y;
}
```

Then, compile it to a shared library with:

```
cc -shared smallc.c -o libsmall.so
```

We can now write an Idris program which calls each of these. First, we’ll
write a small program which uses `add`

to add two integers:

```
%foreign "C:add,libsmall"
add : Int -> Int -> Int
main : IO ()
main = printLn (add 70 24)
```

The `%foreign`

declaration states that `add`

is written in C, with the
name `add`

in the library `libsmall`

. As long as the run time is able
to locate `libsmall.so`

(in practice it looks in the current directory and
the system library paths) we can run this at the REPL:

```
Main> :exec main
94
```

Note that it is the programmer’s responsibility to make sure that the Idris function and C function have corresponding types. There is no way for the machine to check this! If you get it wrong, you will get unpredictable behaviour.

Since `add`

has no side effects, we’ve given it a return type of `Int`

.
But what if the function has some effect on the outside world, like
`addWithMessage`

? In this case, we use `PrimIO Int`

to say that it
returns a primitive IO action:

```
%foreign "C:addWithMessage,libsmall"
prim__addWithMessage : String -> Int -> Int -> PrimIO Int
```

Internally, `PrimIO Int`

is a function which takes the current (linear)
state of the world, and returns an `Int`

with an updated state of the world.
In general, `IO`

operations in an Idris program are defined as instances
of the `HasIO`

interface. We can convert a primitive operation to one usable
in `HasIO`

using `primIO`

:

```
primIO : HasIO io => PrimIO a -> io a
```

So, we can extend our program as follows:

```
addWithMessage : HasIO io => String -> Int -> Int -> io Int
addWithMessage s x y = primIO $ prim__addWithMessage s x y
main : IO ()
main
= do printLn (add 70 24)
addWithMessage "Sum" 70 24
pure ()
```

It is up to the programmer to declare which functions are pure, and which have
side effects, via `PrimIO`

. Executing this gives:

```
Main> :exec main
94
Sum: 70 + 24 = 94
```

We have seen two specifiers for foreign functions:

```
%foreign "C:add,libsmall"
%foreign "C:addWithMessage,libsmall"
```

These both have the same form: `"C:[name],libsmall"`

so instead of writing
the concrete `String`

, we write a function to compute the specifier, and
use that instead:

```
libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmall"
%foreign (libsmall "add")
add : Int -> Int -> Int
%foreign (libsmall "addWithMessage")
prim__addWithMessage : String -> Int -> Int -> PrimIO Int
```

#### Primitive FFI Types¶

The types which can be passed to and returned from foreign functions are restricted to those which it is reasonable to assume any back end can handle. In practice, this means most primitive types, and a limited selection of others. Argument types can be any of the following primitives:

`Int`

`Char`

`Double`

(as`double`

in C)`Bits8`

`Bits16`

`Bits32`

`Bits64`

`String`

(as`char*`

in C)`Ptr t`

and`AnyPtr`

(both as`void*`

in C)

Return types can be any of the above, plus:

`()`

`PrimIO t`

, where`t`

is a valid return type other than a`PrimIO`

.

Handling `String`

leads to some complications, for a number of reasons:

- Strings can have multiple encodings. In the Idris run time, Strings are encoded as UTF-8, but C makes no assumptions.
- It is not always clear who is responsible for freeing a
`String`

allocated by a C function. - In C, strings can be
`NULL`

, but Idris strings always have a value.

So, when passing `String`

to and from C, remember the following:

- A
`char*`

returned by a C function will be copied to the Idris heap, and the Idris run time immediately calls`free`

with the returned`char*`

. - If a
`char*`

might be`NULL`

in`C`

, use`Ptr String`

rather than`String`

.

When using `Ptr String`

, the value will be passed as a `void*`

, and
therefore not accessible directly by Idris code. This is to protect against
accidentally trying to use `NULL`

as a `String`

. You can nevertheless
work with them and convert to `String`

via foreign functions of the following
form:

```
char* getString(void *p) {
return (char*)p;
}
void* mkString(char* str) {
return (void*)str;
}
int isNullString(void* str) {
return str == NULL;
}
```

For an example, see the sample Example: Minimal Readline Bindings bindings.

Additionally, foreign functions can take *callbacks*, and take and return
C `struct`

pointers.

#### Callbacks¶

It is often useful in C for a function to take a *callback*, that is a function
which is called after doing some work. For example, we can write a function
which takes a callback that takes a `char*`

and an `int`

and returns a
`char*`

, in C, as follows (added to `smallc.c`

above):

```
typedef char*(*StringFn)(char*, int);
char* applyFn(char* x, int y, StringFn f) {
printf("Applying callback to %s %d\n", x, y);
return f(x, y);
}
```

Then, we can access this from Idris by declaring it as a `%foreign`

function
and wrapping it in the `HasIO`

interface, with the C function calling the
Idris function as the callback:

```
%foreign (libsmall "applyFn")
prim__applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String
applyFn : HasIO io =>
String -> Int -> (String -> Int -> String) -> io String
applyFn c i f = primIO $ prim__applyFn c i f
```

For example, we can try this as follows:

```
pluralise : String -> Int -> String
pluralise str x
= show x ++ " " ++
if x == 1
then str
else str ++ "s"
main : IO ()
main
= do str1 <- applyFn "Biscuit" 10 pluralise
putStrLn str1
str2 <- applyFn "Tree" 1 pluralise
putStrLn str2
```

As a variant, the callback could have a side effect:

```
%foreign (libsmall "applyFn")
prim__applyFnIO : String -> Int -> (String -> Int -> PrimIO String) ->
PrimIO String
```

This is a little more fiddly to lift to a `HasIO`

function,
due to the callback, but we can do so using `toPrim : IO a -> PrimIO a`

:

```
applyFnIO : HasIO io =>
String -> Int -> (String -> Int -> IO String) -> io String
applyFnIO c i f = primIO $ prim__applyFnIO c i (\s, i => toPrim $ f s i)
```

Note that the callback is explicitly in `IO`

here, since `HasIO`

doesn’t
have a general method for extracting the primitive `IO`

operation.

For example, we can extend the above `pluralise`

example to print a message
in the callback:

```
pluralise : String -> Int -> IO String
pluralise str x
= do putStrLn "Pluralising"
pure $ show x ++ " " ++
if x == 1
then str
else str ++ "s"
main : IO ()
main
= do str1 <- applyFnIO "Biscuit" 10 pluralise
putStrLn str1
str2 <- applyFnIO "Tree" 1 pluralise
putStrLn str2
```

#### Structs¶

Many C APIs pass around more complex data structures, as a `struct`

.
We do not aim to be completely general in the C types we support, because
this will make it harder to write code which is portable across multiple
back ends. However, it is still often useful to be able to access a `struct`

directly. For example, add the following to the top of `smallc.c`

, and
rebuild `libsmall.so`

:

```
#include <stdlib.h>
typedef struct {
int x;
int y;
} point;
point* mkPoint(int x, int y) {
point* pt = malloc(sizeof(point));
pt->x = x;
pt->y = y;
return pt;
}
void freePoint(point* pt) {
free(pt);
}
```

We can define a type for accessing `point`

in Idris by importing
`System.FFI`

and using the `Struct`

type, as follows:

```
Point : Type
Point = Struct "point" [("x", Int), ("y", Int)]
%foreign (libsmall "mkPoint")
mkPoint : Int -> Int -> Point
%foreign (libsmall "freePoint")
prim__freePoint : Point -> PrimIO ()
freePoint : Point -> IO ()
freePoint p = primIO $ prim__freePoint p
```

The `Point`

type in Idris now corresponds to `point*`

in C. Fields can
be read and written using the following, also from `System.FFI`

:

```
getField : Struct s fs -> (n : String) ->
FieldType n ty fs => ty
setField : Struct s fs -> (n : String) ->
FieldType n ty fs => ty -> IO ()
```

Notice that fields are accessed by name, and must be available in the
struct, given the constraint `FieldType n ty fs`

, which states that the
field named `n`

has type `ty`

in the structure fields `fs`

.
So, we can display a `Point`

as follows by accessing the fields directly:

```
showPoint : Point -> String
showPoint pt
= let x : Int = getField pt "x"
y : Int = getField pt "y" in
show (x, y)
```

And, as a complete example, we can initialise, update, display and
delete a `Point`

as follows:

```
main : IO ()
main = do let pt = mkPoint 20 30
setField pt "x" (the Int 40)
putStrLn $ showPoint pt
freePoint pt
```

The field types of a `Struct`

can be any of the following:

`Int`

`Char`

`Double`

(`double`

in C)`Bits8`

`Bits16`

`Bits32`

`Bits64`

`Ptr a`

or`AnyPtr`

(`void*`

in C)- Another
`Struct`

, which is a pointer to a`struct`

in C

Note that this doesn’t include `String`

or function types! This is primarily
because these aren’t directly supported by the Chez back end. However, you can
use another pointer type and convert. For example, assuming you have, in C:

```
typedef struct {
char* name;
point* pt;
} namedpoint;
```

You can represent this in Idris as:

```
NamedPoint : Type
NamedPoint
= Struct "namedpoint"
[("name", Ptr String),
("pt", Point)]
```

That is, using a `Ptr String`

instead of a `String`

directly. Then you
can convert between a `void*`

and a `char*`

in C:

```
char* getString(void *p) {
return (char*)p;
}
```

…and use this to convert to a `String`

in Idris:

```
%foreign (pfn "getString")
getString : Ptr String -> String
```

#### Finalisers¶

In some libraries, a foreign function creates a pointer and the caller is
responsible for freeing it. In this case, you can make an explicit foreign
call to `free`

. However, this is not always convenient, or even possible.
Instead, you can ask the Idris run-time to be responsible for freeing the
pointer when it is no longer accessible, using `onCollect`

(or its
typeless variant `onCollectAny`

) defined in the Prelude:

```
onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t)
onCollectAny : AnyPtr -> (AnyPtr -> IO ()) -> IO GCAnyPtr
```

A `GCPtr t`

behaves exactly like `Ptr t`

when passed to a foreign
function (and, similarly, `GCAnyPtr`

behaves like `AnyPtr`

). A foreign
function cannot return a `GCPtr`

however, because then we can no longer
assume the pointer is completely managed by the Idris run-time.

The finaliser is called either when the garbage collector determines that the pointer is no longer accessible, or at the end of execution.

Note that finalisers might not be supported by all back ends, since they depend on the facilities offered by a specific back end’s run time system. They are certainly supported in the Chez Scheme and Racket back ends.

### Example: Minimal Readline Bindings¶

In this section, we’ll see how to create bindings for a C library (the GNU
Readline library) in
Idris, and make them available in a package. We’ll only create the most minimal
bindings, but nevertheless they demonstrate some of the trickier problems in
creating bindings to a C library, in that they need to handle memory allocation
of `String`

.

You can find the example in full in the Idris 2 source repository, in samples/FFI-readline. As a minimal example, this can be used as a starting point for other C library bindings.

We are going to provide bindings to the following functions in the Readline
API, available via `#include <readline/readline.h>`

:

```
char* readline (const char *prompt);
void add_history(const char *string);
```

Additionally, we are going to support tab completion, which in the Readline API is achieved by setting a global variable to a callback function (see Section Callbacks) which explains how to handle the completion:

```
typedef char *rl_compentry_func_t (const char *, int);
rl_compentry_func_t * rl_completion_entry_function;
```

A completion function takes a `String`

, which is the text to complete, and
an `Int`

, which is the number of times it has asked for a completion so far.
In Idris, this could be a function `complete : String -> Int -> IO String`

.
So, for example, if the text so far is `"id"`

, and the possible completions
are `idiomatic`

and `idris`

, then `complete "id" 0`

would produce the
string `"idiomatic"`

and `complete "id" 1`

would produce `"idris"`

.

We will define *glue* functions in a C file `idris_readline.c`

, which compiles
to a shared object `libidrisreadline`

, so we write a function for locating
the C functions:

```
rlib : String -> String
rlib fn = "C:" ++ fn ++ ",libidrisreadline"
```

Each of the foreign bindings will have a `%foreign`

specifier which locates
functions via `rlib`

.

#### Basic behaviour: Reading input, and history¶

We can start by writing a binding for `readline`

directly. It’s interactive,
so needs to return a `PrimIO`

:

```
%foreign (rlib "readline")
prim__readline : String -> PrimIO String
```

Then, we can write an `IO`

wrapper:

```
readline : String -> IO String
readline prompt = primIO $ readline prompt
```

Unfortunately, this isn’t quite good enough! The C `readline`

function
returns a `NULL`

string if there is no input due to encountering an
end of file. So, we need to handle that - if we don’t, we’ll get a crash
on encountering end of file (remember: it’s the Idris programmer’s responsibility
to give an appropriate type to the C binding!)

Instead, we need to use a `Ptr`

to say that it might be a `NULL`

pointer (see Section Primitive FFI Types):

```
%foreign (rlib "readline")
prim__readline : String -> PrimIO (Ptr String)
```

We also need to provide a way to check whether the returned `Ptr String`

is
`NULL`

. To do so, we’ll write some glue code to convert back and forth
between `Ptr String`

and `String`

, in a file `idris_readline.c`

and a
corresponding header `idris_readline.h`

. In `idris_readline.h`

we have:

```
int isNullString(void* str); // return 0 if a string in NULL, non zero otherwise
char* getString(void* str); // turn a non-NULL Ptr String into a String (assuming not NULL)
void* mkString(char* str); // turn a String into a Ptr String
void* nullString(); // create a new NULL String
```

Correspondingly, in `idris_readline.c`

:

```
int isNullString(void* str) {
return str == NULL;
}
char* getString(void* str) {
return (char*)str;
}
void* mkString(char* str) {
return (void*)str;
}
void* nullString() {
return NULL;
}
```

Now, we can use `prim__readline`

as follows, with a safe API, checking
whether the result it returns is `NULL`

or a concrete `String`

:

```
%foreign (rlib "isNullString")
prim__isNullString : Ptr String -> Int
export
isNullString : Ptr String -> Bool
isNullString str = if prim__isNullString str == 0 then False else True
export
readline : String -> IO (Maybe String)
readline s
= do mstr <- primIO $ prim__readline s
if isNullString mstr
then pure $ Nothing
else pure $ Just (getString mstr)
```

We’ll need `nullString`

and `mkString`

later, for dealing with completions.

Once we’ve read a string, we’ll want to add it to the input history. We can
provide a binding to `add_history`

as follows:

```
%foreign (rlib "add_history")
prim__add_history : String -> PrimIO ()
export
addHistory : String -> IO ()
addHistory s = primIO $ prim__add_history s
```

In this case, since Idris is in control of the `String`

, we know it’s not
going to be `NULL`

, so we can add it directly.

A small `readline`

program that reads input, and echoes it, recording input
history for non-empty inputs, can be written as follows:

```
echoLoop : IO ()
echoLoop
= do Just x <- readline "> "
| Nothing => putStrLn "EOF"
putStrLn ("Read: " ++ x)
when (x /= "") $ addHistory x
if x /= "quit"
then echoLoop
else putStrLn "Done"
```

This gives us command history, and command line editing, but Readline becomes much more useful when we add tab completion. The default tab completion, which is available even in the small example above, is to tab complete file names in the current working directory. But for any realistic application, we probably want to tab complete other commands, such as function names, references to local data, or anything that is appropriate for the application.

#### Completions¶

Readline has a large API, with several ways of supporting tab completion, typically involving setting a global variable to an appropriate completion function. We’ll use the following:

```
typedef char *rl_compentry_func_t (const char *, int);
rl_compentry_func_t * rl_completion_entry_function;
```

The completion function takes the prefix of the completion, and the number
of times it has been called so far on this prefix, and returns the next
completion, or `NULL`

if there are no more completions. An Idris equivalent
would therefore have the following type:

```
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
```

The function returns `Nothing`

if there are no more completions, or
`Just str`

for some `str`

if there is another one for the current
input.

We might hope that it’s a matter of defining a function to assign the completion function…

```
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
rl_completion_entry_function = fn;
}
```

…then defining the Idris binding, which needs to take into account that
the Readline library expects `NULL`

when there are no more completions:

```
%foreign (rlib "idrisrl_setCompletion")
prim__setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO ()
export
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
setCompletionFn fn
= primIO $ prim__setCompletion $ \s, i => toPrim $
do mstr <- fn s i
case mstr of
Nothing => pure nullString // need to return a Ptr String to readline!
Just str => pure (mkString str)
```

So, we turn `Nothing`

into `nullString`

and `Just str`

into ```
mkString
str
```

. Unfortunately, this doesn’t quite work. To see what goes wrong, let’s
try it for the most basic completion function that returns one completion no
matter what the input:

```
testComplete : String -> Int -> IO (Maybe String)
testComplete text 0 = pure $ Just "hamster"
testComplete text st = pure Nothing
```

We’ll try this in a small modification of `echoLoop`

above, setting a
completion function first:

```
main : IO ()
main = do setCompletionFn testComplete
echoLoop
```

We see that there is a problem when we try running it, and hitting TAB before entering anything:

```
Main> :exec main
> free(): invalid pointer
```

The Idris code which sets up the completion is fine, but there is a problem with the memory allocation in the C glue code.

This problem arises because we haven’t thought carefully enough about which
parts of our program are responsible for allocating and freeing strings.
When Idris calls a foreign function that returns a string, it copies the
string to the Idris heap and frees it immediately. But, if the foreign
library also frees the string, it ends up being freed twice. This is what’s
happening here: the callback passed to `prim__setCompletion`

frees the string
and puts it onto the Idris heap, but Readline also frees the string returned
by `prim__setCompletion`

once it has processed it. We can solve this
problem by writing a wrapper for the completion function which reallocates
the string, and using that in `idrisrl_setCompletion`

instead.

```
rl_compentry_func_t* my_compentry;
char* compentry_wrapper(const char* text, int i) {
char* res = my_compentry(text, i); // my_compentry is an Idris function, so res is on the Idris heap,
// and freed on return
if (res != NULL) {
char* comp = malloc(strlen(res)+1); // comp is passed back to readline, which frees it when
// it is finished with it
strcpy(comp, res);
return comp;
}
else {
return NULL;
}
}
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
rl_completion_entry_function = compentry_wrapper;
my_compentry = fn; // fn is an Idris function, called by compentry_wrapper
}
```

So, we define the completion function in C, which calls the Idris completion function then makes sure the string returned by the Idris function is copied to the C heap.

We now have a primitive API that covers the most fundamental features of the readline API:

```
readline : String -> IO (Maybe String)
addHistory : String -> IO ()
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
```

## Theorem Proving¶

A tutorial on theorem proving in Idris 2.

Note

*The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.

Before we discuss the details of theorem proving in Idris, we will describe some fundamental concepts:

- Propositions and judgments
- Boolean and constructive logic
- Curry-Howard correspondence
- Definitional and propositional equalities
- Axiomatic and constructive approaches

### Propositions and Judgments¶

Propositions are the subject of our proofs. Before the proof, we can’t
formally say if they are true or not. If the proof is successful then the
result is a ‘judgment’. For instance, if the `proposition`

is,

1+1=2 |

When we prove it, the `judgment`

is,

1+1=2 true |

Or if the `proposition`

is,

1+1=3 |

we can’t prove it is true, but it is still a valid proposition and perhaps we
can prove it is false so the `judgment`

is,

1+1=3 false |

This may seem a bit pedantic but it is important to be careful: in mathematics not every proposition is true or false. For instance, a proposition may be unproven or even unprovable.

So the logic here is different from the logic that comes from boolean algebra. In that case what is not true is false and what is not false is true. The logic we are using here does not have this law, the “Law of Excluded Middle”, so we cannot use it.

A false proposition is taken to be a contradiction and if we have a contradiction then we can prove anything, so we need to avoid this. Some languages, used in proof assistants, prevent contradictions.

The logic we are using is called constructive (or sometimes intuitional) because we are constructing a ‘database’ of judgments.

#### Curry-Howard correspondence¶

So how do we relate these proofs to Idris programs? It turns out that there is a correspondence between constructive logic and type theory. They have the same structure and we can switch back and forth between the two notations.

The way that this works is that a proposition is a type so…

```
Main> 1 + 1 = 2
2 = 2
Main> :t 1 + 1 = 2
(fromInteger 1 + fromInteger 1) === fromInteger 2 : Type
```

…is a proposition and it is also a type. The following will also produce an equality type:

```
Main> 1 + 1 = 3
2 = 3
```

Both of these are valid propositions so both are valid equality types. But how do we represent a true judgment? That is, how do we denote 1+1=2 is true but not 1+1=3? A type that is true is inhabited, that is, it can be constructed. An equality type has only one constructor ‘Refl’ so a proof of 1+1=2 is

```
onePlusOne : 1+1=2
onePlusOne = Refl
```

Now that we can represent propositions as types other aspects of propositional logic can also be translated to types as follows:

propositions | example of possible type | |

A | x=y | |

B | y=z | |

and | A /B | Pair(x=y,y=z) |

or | A / B | Either(x=y,y=z) |

implies | A -> B | (x=y) -> (y=x) |

for all | y=z | |

exists | y=z |

#### And (conjunction)¶

We can have a type which corresponds to conjunction:

```
AndIntro : a -> b -> A a b
```

There is a built in type called ‘Pair’.

#### Or (disjunction)¶

We can have a type which corresponds to disjunction:

```
data Or : Type -> Type -> Type where
OrIntroLeft : a -> A a b
OrIntroRight : b -> A a b
```

There is a built in type called ‘Either’.

#### Definitional and Propositional Equalities¶

We have seen that we can ‘prove’ a type by finding a way to construct a term.
In the case of equality types there is only one constructor which is `Refl`

.
We have also seen that each side of the equation does not have to be identical
like ‘2=2’. It is enough that both sides are *definitionally equal* like this:

```
onePlusOne : 1+1=2
onePlusOne = Refl
```

Both sides of this equation normalise to 2 and so Refl matches and the proposition is proved.

We don’t have to stick to terms; we can also use symbolic parameters so the following type checks:

```
varIdentity : m = m
varIdentity = Refl
```

If a proposition/equality type is not definitionally equal but is still true
then it is *propositionally equal*. In this case we may still be able to prove
it but some steps in the proof may require us to add something into the terms
or at least to take some sideways steps to get to a proof.

Especially when working with equalities containing variable terms (inside
functions) it can be hard to know which equality types are definitionally equal,
in this example `plusReducesL`

is *definitionally equal* but `plusReducesR`

is
not (although it is *propositionally equal*). The only difference between
them is the order of the operands.

```
plusReducesL : (n:Nat) -> plus Z n = n
plusReducesL n = Refl
plusReducesR : (n:Nat) -> plus n Z = n
plusReducesR n = Refl
```

Checking `plusReducesR`

gives the following error:

```
Proofs.idr:21:18--23:1:While processing right hand side of Main.plusReducesR at Proofs.idr:21:1--23:1:
Can't solve constraint between:
plus n Z
and
n
```

So why is `Refl`

able to prove some equality types but not others?

The first answer is that `plus`

is defined by recursion on its first
argument. So, when the first argument is `Z`

, it reduces, but not when the
second argument is `Z`

.

If an equality type can be proved/constructed by using `Refl`

alone it is known
as a *definitional equality*. In order to be definitionally equal both sides
of the equation must normalise to the same value.

So when we type `1+1`

in Idris it is immediately reduced to 2 because
definitional equality is built in

```
Main> 1+1
2
```

In the following pages we discuss how to resolve propositional equalities.

### Running example: Addition of Natural Numbers¶

Throughout this tutorial, we will be working with the following function, defined in the Idris prelude, which defines addition on natural numbers:

```
plus : Nat -> Nat -> Nat
plus Z m = m
plus (S k) m = S (plus k m)
```

It is defined by the above equations, meaning that we have for free the
properties that adding `m`

to zero always results in `m`

, and that
adding `m`

to any non-zero number `S k`

always results in
`S (plus k m)`

. We can see this by evaluation at the Idris REPL (i.e.
the prompt, the read-eval-print loop):

```
Main> \m => plus Z m
\m => m
Idris> \k,m => plus (S k) m
\k => \m => S (plus k m)
```

Note that unlike many other language REPLs, the Idris REPL performs
evaluation on *open* terms, meaning that it can reduce terms which
appear inside lambda bindings, like those above. Therefore, we can
introduce unknowns `k`

and `m`

as lambda bindings and see how
`plus`

reduces.

The `plus`

function has a number of other useful properties, for
example:

- It is
*commutative*, that is for all`Nat`

inputs`n`

and`m`

, we know that`plus n m = plus m n`

. - It is
*associative*, that is for all`Nat`

inputs`n`

,`m`

and`p`

, we know that`plus n (plus m p) = plus (plus m n) p`

.

We can use these properties in an Idris program, but in order to do so
we must *prove* them.

#### Equality Proofs¶

Idris defines a propositional equality type as follows:

```
data Equal : a -> b -> Type where
Refl : Equal x x
```

As syntactic sugar, `Equal x y`

can be written as `x = y`

.

It is *propositional* equality, where the type states that any two
values in different types `a`

and `b`

may be proposed to be equal.
There is only one way to *prove* equality, however, which is by
reflexivity (`Refl`

).

We have a *type* for propositional equality here, and correspondingly a
*program* inhabiting an instance of this type can be seen as a proof of
the corresponding proposition [1]. So, trivially, we can prove that
`4`

equals `4`

:

```
four_eq : 4 = 4
four_eq = Refl
```

However, trying to prove that `4 = 5`

results in failure:

```
four_eq_five : 4 = 5
four_eq_five = Refl
```

The type `4 = 5`

is a perfectly valid type, but is uninhabited, so
when trying to type check this definition, Idris gives the following
error:

```
When unifying 4 = 4 and (fromInteger 4) = (fromInteger 5)
Mismatch between:
4
and
5
```

##### Type checking equality proofs¶

An important step in type checking Idris programs is *unification*,
which attempts to resolve implicit arguments such as the implicit
argument `x`

in `Refl`

. As far as our understanding of type checking
proofs is concerned, it suffices to know that unifying two terms
involves reducing both to normal form then trying to find an assignment
to implicit arguments which will make those normal forms equal.

When type checking `Refl`

, Idris requires that the type is of the form
`x = x`

, as we see from the type of `Refl`

. In the case of
`four_eq_five`

, Idris will try to unify the expected type `4 = 5`

with the type of `Refl`

, `x = x`

, notice that a solution requires
that `x`

be both `4`

and `5`

, and therefore fail.

Since type checking involves reduction to normal form, we can write the following equalities directly:

```
twoplustwo_eq_four : 2 + 2 = 4
twoplustwo_eq_four = Refl
plus_reduces_Z : (m : Nat) -> plus Z m = m
plus_reduces_Z m = Refl
plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)
plus_reduces_Sk k m = Refl
```

#### Heterogeneous Equality¶

Equality in Idris is *heterogeneous*, meaning that we can even propose
equalities between values in different types:

```
idris_not_php : Z = "Z"
```

The type `Z = "Z"`

is uninhabited, and one might wonder why it is useful to
be able to propose equalities between values in different types. However, with
dependent types, such equalities can arise naturally. For example, if two
vectors are equal, their lengths must be equal:

```
vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) ->
(xs = ys) -> n = m
```

In the above declaration, `xs`

and `ys`

have different types because
their lengths are different, but we would still like to draw a
conclusion about the lengths if they happen to be equal. We can define
`vect_eq_length`

as follows:

```
vect_eq_length xs xs Refl = Refl
```

By matching on `Refl`

for the third argument, we know that the only
valid value for `ys`

is `xs`

, because they must be equal, and
therefore their types must be equal, so the lengths must be equal.

Alternatively, we can put an underscore for the second `xs`

, since
there is only one value which will type check:

```
vect_eq_length xs _ Refl = Refl
```

#### Properties of `plus`

¶

Using the `(=)`

type, we can now state the properties of `plus`

given above as Idris type declarations:

```
plus_commutes : (n, m : Nat) -> plus n m = plus m n
plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p
```

Both of these properties (and many others) are proved for natural number
addition in the Idris standard library, using `(+)`

from the `Num`

interface rather than using `plus`

directly. They have the names
`plusCommutative`

and `plusAssociative`

respectively.

In the remainder of this tutorial, we will explore several different
ways of proving `plus_commutes`

(or, to put it another way, writing
the function.) We will also discuss how to use such equality proofs, and
see where the need for them arises in practice.

[1] | This is known as the Curry-Howard correspondence. |

### Inductive Proofs¶

Before embarking on proving `plus_commutes`

in Idris itself, let us
consider the overall structure of a proof of some property of natural
numbers. Recall that they are defined recursively, as follows:

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

A *total* function over natural numbers must both terminate, and cover
all possible inputs. Idris checks functions for totality by checking that
all inputs are covered, and that all recursive calls are on
*structurally smaller* values (so recursion will always reach a base
case). Recalling `plus`

:

```
plus : Nat -> Nat -> Nat
plus Z m = m
plus (S k) m = S (plus k m)
```

This is total because it covers all possible inputs (the first argument
can only be `Z`

or `S k`

for some `k`

, and the second argument
`m`

covers all possible `Nat`

) and in the recursive call, `k`

is structurally smaller than `S k`

so the first argument will always
reach the base case `Z`

in any sequence of recursive calls.

In some sense, this resembles a mathematical proof by induction (and
this is no coincidence!). For some property `P`

of a natural number
`x`

, we can show that `P`

holds for all `x`

if:

`P`

holds for zero (the base case).- Assuming that
`P`

holds for`k`

, we can show`P`

also holds for`S k`

(the inductive step).

In `plus`

, the property we are trying to show is somewhat trivial (for
all natural numbers `x`

, there is a `Nat`

which need not have any
relation to `x`

). However, it still takes the form of a base case and
an inductive step. In the base case, we show that there is a `Nat`

arising from `plus n m`

when `n = Z`

, and in the inductive step we
show that there is a `Nat`

arising when `n = S k`

and we know we can
get a `Nat`

inductively from `plus k m`

. We could even write a
function capturing all such inductive definitions:

```
nat_induction :
(prop : Nat -> Type) -> -- Property to show
(prop Z) -> -- Base case
((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step
(x : Nat) -> -- Show for all x
prop x
nat_induction prop p_Z p_S Z = p_Z
nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k)
```

Using `nat_induction`

, we can implement an equivalent inductive
version of `plus`

:

```
plus_ind : Nat -> Nat -> Nat
plus_ind n m
= nat_induction (\x => Nat)
m -- Base case, plus_ind Z m
(\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
-- where k_rec = plus_ind k m
n
```

To prove that `plus n m = plus m n`

for all natural numbers `n`

and
`m`

, we can also use induction. Either we can fix `m`

and perform
induction on `n`

, or vice versa. We can sketch an outline of a proof;
performing induction on `n`

, we have:

Property

`prop`

is`\x => plus x m = plus m x`

.Show that

`prop`

holds in the base case and inductive step:- Base case:
`prop Z`

, i.e.`plus Z m = plus m Z`

, which reduces to`m = plus m Z`

due to the definition of`plus`

. - Inductive step: Inductively, we know that
`prop k`

holds for a specific, fixed`k`

, i.e.`plus k m = plus m k`

(the induction hypothesis). Given this, show`prop (S k)`

, i.e.`plus (S k) m = plus m (S k)`

, which reduces to`S (plus k m) = plus m (S k)`

. From the induction hypothesis, we can rewrite this to`S (plus m k) = plus m (S k)`

.

To complete the proof we therefore need to show that `m = plus m Z`

for all natural numbers `m`

, and that `S (plus m k) = plus m (S k)`

for all natural numbers `m`

and `k`

. Each of these can also be
proved by induction, this time on `m`

.

We are now ready to embark on a proof of commutativity of `plus`

formally in Idris.

### Pattern Matching Proofs¶

In this section, we will provide a proof of `plus_commutes`

directly,
by writing a pattern matching definition. We will use interactive
editing features extensively, since it is significantly easier to
produce a proof when the machine can give the types of intermediate
values and construct components of the proof itself. The commands we
will use are summarised below. Where we refer to commands
directly, we will use the Vim version, but these commands have a direct
mapping to Emacs commands.

Command | Vim binding | Emacs binding | Explanation |

Check type | `\t` |
`C-c C-t` |
Show type of identifier or hole under the cursor. |

Proof search | `\s` |
`C-c C-a` |
Attempt to solve hole under the cursor by applying simple proof search. |

Make new definition | `\a` |
`C-c C-s` |
Add a template definition for the type defined under the cursor. |

Make lemma | `\l` |
`C-c C-e` |
Add a top level function with a type which solves the hole under the cursor. |

Split cases | `\c` |
`C-c C-c` |
Create new constructor patterns for each possible case of the variable under the cursor. |

#### Creating a Definition¶

To begin, create a file `pluscomm.idr`

containing the following type
declaration:

```
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
```

To create a template definition for the proof, press `\a`

(or the
equivalent in your editor of choice) on the line with the type
declaration. You should see:

```
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes n m = ?plus_commutes_rhs
```

To prove this by induction on `n`

, as we sketched in Section
Inductive Proofs, we begin with a case split on `n`

(press
`\c`

with the cursor over the `n`

in the definition.) You
should see:

```
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = ?plus_commutes_rhs_1
plus_commutes (S k) m = ?plus_commutes_rhs_2
```

If we inspect the types of the newly created holes,
`plus_commutes_rhs_1`

and `plus_commutes_rhs_2`

, we see that the
type of each reflects that `n`

has been refined to `Z`

and `S k`

in each respective case. Pressing `\t`

over
`plus_commutes_rhs_1`

shows:

```
m : Nat
-------------------------------------
plus_commutes_rhs_1 : m = plus m Z
```

Similarly, for `plus_commutes_rhs_2`

:

```
k : Nat
m : Nat
--------------------------------------
plus_commutes_rhs_2 : (S (plus k m)) = (plus m (S k))
```

It is a good idea to give these slightly more meaningful names:

```
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = ?plus_commutes_Z
plus_commutes (S k) m = ?plus_commutes_S
```

#### Base Case¶

We can create a separate lemma for the base case interactively, by
pressing `\l`

with the cursor over `plus_commutes_Z`

. This
yields:

```
plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = plus_commutes_Z m
plus_commutes (S k) m = ?plus_commutes_S
```

That is, the hole has been filled with a call to a top level
function `plus_commutes_Z`

, applied to the variable in scope `m`

.

Unfortunately, we cannot prove this lemma directly, since `plus`

is
defined by matching on its *first* argument, and here `plus m Z`

has a
concrete value for its *second argument* (in fact, the left hand side of
the equality has been reduced from `plus Z m`

.) Again, we can prove
this by induction, this time on `m`

.

First, create a template definition with `\d`

:

```
plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z m = ?plus_commutes_Z_rhs
```

Now, case split on `m`

with `\c`

:

```
plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = ?plus_commutes_Z_rhs_1
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
```

Checking the type of `plus_commutes_Z_rhs_1`

shows the following,
which is provable by `Refl`

:

```
--------------------------------------
plus_commutes_Z_rhs_1 : Z = Z
```

For such immediate proofs, we can let write the proof automatically by
pressing `\s`

with the cursor over `plus_commutes_Z_rhs_1`

.
This yields:

```
plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
```

For `plus_commutes_Z_rhs_2`

, we are not so lucky:

```
k : Nat
-------------------------------------
plus_commutes_Z_rhs_2 : S k = S (plus k Z)
```

Inductively, we should know that `k = plus k Z`

, and we can get access
to this inductive hypothesis by making a recursive call on k, as
follows:

```
plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k)
= let rec = plus_commutes_Z k in
?plus_commutes_Z_rhs_2
```

For `plus_commutes_Z_rhs_2`

, we now see:

```
k : Nat
rec : k = plus k Z
-------------------------------------
plus_commutes_Z_rhs_2 : S k = S (plus k Z)
```

So we know that `k = plus k Z`

, but how do we use this to update the goal to
`S k = S k`

?

To achieve this, Idris provides a `replace`

function as part of the
prelude:

```
Main> :t replace
Builtin.replace : (0 rule : x = y) -> p x -> p y
```

Given a proof that `x = y`

, and a property `p`

which holds for
`x`

, we can get a proof of the same property for `y`

, because we
know `x`

and `y`

must be the same. Note the multiplicity on `rule`

means that it’s guaranteed to be erased at run time.
In practice, this function can be
a little tricky to use because in general the implicit argument `p`

can be hard to infer by unification, so Idris provides a high level
syntax which calculates the property and applies `replace`

:

```
rewrite prf in expr
```

If we have `prf : x = y`

, and the required type for `expr`

is some
property of `x`

, the `rewrite ... in`

syntax will search for all
occurrences of `x`

in the required type of `expr`

and replace them with `y`

. We want
to replace `plus k Z`

with `k`

, so we need to apply our rule
`rec`

in reverse, which we can do using `sym`

from the Prelude

```
Main> :t sym
Builtin.sym : (0 rule : x = y) -> y = x
```

Concretely, in our example, we can say:

```
plus_commutes_Z (S k)
= let rec = plus_commutes_Z k in
rewrite sym rec in ?plus_commutes_Z_rhs_2
```

Checking the type of `plus_commutes_Z_rhs_2`

now gives:

```
k : Nat
rec : k = plus k Z
-------------------------------------
plus_commutes_Z_rhs_2 : S k = S k
```

Using the rewrite rule `rec`

, the goal type has been updated with `plus k Z`

replaced by `k`

.

We can use proof search (`\s`

) to complete the proof, giving:

```
plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k)
= let rec = plus_commutes_Z k in
rewrite sym rec in Refl
```

The base case of `plus_commutes`

is now complete.

#### Inductive Step¶

Our main theorem, `plus_commutes`

should currently be in the following
state:

```
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = plus_commutes_Z m
plus_commutes (S k) m = ?plus_commutes_S
```

Looking again at the type of `plus_commutes_S`

, we have:

```
k : Nat
m : Nat
-------------------------------------
plus_commutes_S : S (plus k m) = plus m (S k)
```

Conveniently, by induction we can immediately tell that
`plus k m = plus m k`

, so let us rewrite directly by making a
recursive call to `plus_commutes`

. We add this directly, by hand, as
follows:

```
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = plus_commutes_Z
plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S
```

Checking the type of `plus_commutes_S`

now gives:

```
k : Nat
m : Nat
-------------------------------------
plus_commutes_S : S (plus m k) = plus m (S k)
```

The good news is that `m`

and `k`

now appear in the correct order.
However, we still have to show that the successor symbol `S`

can be
moved to the front in the right hand side of this equality. This
remaining lemma takes a similar form to the `plus_commutes_Z`

; we
begin by making a new top level lemma with `\l`

. This gives:

```
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
```

Again, we make a template definition with `\a`

:

```
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
plus_commutes_S k m = ?plus_commutes_S_rhs
```

Like `plus_commutes_Z`

, we can define this by induction over `m`

, since
`plus`

is defined by matching on its first argument. The complete definition
is:

```
total
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
plus_commutes_S k Z = Refl
plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
```

All holes have now been solved.

The `total`

annotation means that we require the final function to
pass the totality checker; i.e. it will terminate on all possible
well-typed inputs. This is important for proofs, since it provides a
guarantee that the proof is valid in *all* cases, not just those for
which it happens to be well-defined.

Now that `plus_commutes`

has a `total`

annotation, we have completed the
proof of commutativity of addition on natural numbers.

This page attempts to explain some of the techniques used in Idris to prove propositional equalities.

### Proving Propositional Equality¶

We have seen that definitional equalities can be proved using `Refl`

since they
always normalise to values that can be compared directly.

However with propositional equalities we are using symbolic variables, which do not always normalse.

So to take the previous example:

```
plusReducesR : (n : Nat) -> plus n Z = n
```

In this case `plus n Z`

does not normalise to n. Even though both sides of
the equality are provably equal we cannot claim `Refl`

as a proof.

If the pattern match cannot match for all `n`

then we need to
match all possible values of `n`

. In this case

```
plusReducesR : (n : Nat) -> plus n Z = n
plusReducesR Z = Refl
plusReducesR (S k)
= let rec = plusReducesR k in
rewrite sym rec in Refl
```

we can’t use `Refl`

to prove `n = plus n 0`

for all `n`

. Instead, we call
it for each case separately. So, in the second line for example, the type checker
substitutes `Z`

for `n`

in the type being matched, and reduces the type
accordingly.

### Replace¶

This implements the ‘indiscernability of identicals’ principle, if two terms
are equal then they have the same properties. In other words, if `x=y`

, then we
can substitute y for x in any expression. In our proofs we can express this as:

if x=y then prop x = prop y

where prop is a pure function representing the property. In the examples below
prop is an expression in some variable with a type like this: `prop: n -> Type`

So if `n`

is a natural number variable then `prop`

could be something
like `\n => 2*n + 3`

.

To use this in our proofs there is the following function in the prelude:

```
||| Perform substitution in a term according to some equality.
replace : forall x, y, prop . (0 rule : x = y) -> prop x -> prop y
replace Refl prf = prf
```

If we supply an equality (x=y) and a proof of a property of x (`prop x`

) then we get
a proof of a property of y (`prop y`

).
So, in the following example, if we supply `p1 x`

which is a proof that `x=2`

and
the equality `x=y`

then we get a proof that `y=2`

.

```
p1: Nat -> Type
p1 n = (n=2)
testReplace: (x=y) -> (p1 x) -> (p1 y)
testReplace a b = replace a b
```

### Rewrite¶

In practice, `replace`

can be
a little tricky to use because in general the implicit argument `prop`

can be hard to infer for the machine, so Idris provides a high level
syntax which calculates the property and applies `replace`

.

Example: again we supply `p1`

which is a proof that `x=2`

and the equality
`x=y`

then we get a proof that `y=2`

.

```
p1: Nat -> Type
p1 x = (x=2)
testRewrite2: (x=y) -> (p1 y) -> (p1 x)
testRewrite2 a b = rewrite a in b
```

We can think of `rewrite`

as working in this way:

- Start with a equation
`x=y`

and a property`prop : x -> Type`

- Search for
`x`

in`prop`

- Replaces all occurrences of
`x`

with`y`

in`prop`

.

That is, we are doing a substitution.

### Symmetry and Transitivity¶

In addition to ‘reflexivity’ equality also obeys ‘symmetry’ and ‘transitivity’ and these are also included in the prelude:

```
||| Symmetry of propositional equality
sym : forall x, y . (0 rule : x = y) -> y = x
sym Refl = Refl
||| Transitivity of propositional equality
trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c
trans Refl Refl = Refl
```

### Heterogeneous Equality¶

Also included in the prelude:

```
||| Explicit heterogeneous ("John Major") equality. Use this when Idris
||| incorrectly chooses homogeneous equality for `(=)`.
||| @ a the type of the left side
||| @ b the type of the right side
||| @ x the left side
||| @ y the right side
(~=~) : (x : a) -> (y : b) -> Type
(~=~) x y = (x = y)
```

## Frequently Asked Questions¶

### Can Idris 2 compile itself?¶

Yes, Idris 2 is implemented in Idris 2. By default, it targets Chez Scheme, so you can bootstrap from the generated Scheme code, as described in Section Getting Started.

### Why does Idris 2 target Scheme? Surely a dynamically typed target language is going to be slow?¶

You may be surprised at how fast Chez Scheme is :). Racket, as an alternative target, also performs well. Both perform better than the Idris 1 back end, which is written in C but has not had the decades of engineering effort by run time system specialists that Chez and Racket have. Chez Scheme also allows us to turn off run time checks, which we do.

As anecdotal evidence of the performance improvement, as of 23rd May 2020, on a Dell XPS 13 running Ubuntu, the performance is:

- Idris 2 (with the Chez Scheme runtime) checks its own source in 93 seconds.
- The bootstrapping Idris 2 (compiled with Idris 1) checks the same source in 125s.
- Idris 1 checks the bootstrapping Idris 2’s source (the same as the above, but with minor variations due to the syntax changes) in 768 seconds.

This is, nevertheless, not intended to be a long term solution, even if it is a very convenient way to bootstrap.

### Can Idris 2 generate Javascript? What about plug-in code generators?¶

Yes! A JavaScript code generator is built in, and can target either the browser or NodeJS.

Like Idris 1, Idris 2 supports plug-in code generation to allow you to write a back end for the platform of your choice.

### What are the main differences between Idris 1 and Idris 2?¶

The most important difference is that Idris 2 explicitly represents *erasure*
in types, so that you can see at compile time which function and data type
arguments are erased, and which will be present at run time. You can see more
details in Multiplicities.

Idris 2 has significantly better type checking performance (perhaps even an order of magnitude!) and generates significantly better code.

Also, being implemented in Idris, we’ve been able to take advantage of the type system to remove some significant sources of bugs!

You can find more details in Section Changes since Idris 1.

### Why aren’t there more linearity annotations in the library?¶

In theory, now that Idris 2 is based on Quantitative Type Theory (see Section Multiplicities, we can write more precise types in the Prelude and Base libraries which give more precise usage information. We have chosen not to do that (yet) however. Consider, for example, what would happen if we did:

```
id : (1 _ : a) -> a
id x = x
```

This is definitely correct, because `x`

is used exactly once. However, we
also have:

```
map : (a -> b) -> List a -> List b
```

We can’t guarantee that the function passed to `map`

is linear in its
argument in general, and so we can no longer say `map id xs`

since the
multiplicity of `id`

doesn’t match the multiplicity of the function passed
to `map`

.

Eventually, we hope to extend the core language with multiplicity polymorphism which will help resolve these problems. Until then, we consider linearity an experimental new feature in the type system, and therefore we follow the general philosophy that if you don’t want to use linearity, its presence mustn’t impact the way you write programs.

### How do I get command history in the Idris2 REPL?¶

The Idris2 repl does not support readline in the interest of
keeping dependencies minimal. A useful work around is to
install rlwrap, this
utility provides command history simply by invoking the Idris2
repl as an argument to the utility `rlwrap idris2`

.

The goal, eventually, is to use the IDE mode as the basis of an implementation of a sophisticated REPL, developed independently from the Idris 2 core.

### Where can I find more answers?¶

The Idris 1 FAQ is mostly still relevant.

## Implementation Notes¶

Note

*The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.

This section contains (or will contain, hopefully) a variety of notes on aspects of the implementation of Idris 2, in the hope that they help with debugging and future contributions.

### Implementation Overview¶

These are some unsorted notes on aspects of the implementation. Sketchy, and not always completely up to date, but hopefully give some hints as to what’s going on and some ideas where to look in the code to see how certain features work.

#### Introduction¶

Core language TT (defined in `Core.TT`

), based on quantitative type theory
(see https://bentnib.org/quantitative-type-theory.html). Binders have
“multiplicities” which are either *0*, *1* or *unlimited*.

Terms are indexed over the names in scope so that we know terms are always well
scoped. Values (i.e. normal forms) are defined in `Core.Value`

as `NF`

;
constructors do not evaluate their arguments until explicitly requested.

Elaborate to *TT* from a higher level language *TTImp* (defined in `TTImp.TTImp`

),
which is TT with implicit arguments, local function definitions, case blocks,
as patterns, qualified names with automatic type-directed disambiguation, and
proof search.

Elaboration relies on unification (in `Core.Unify`

), which allows postponing
of unification problems. Essentially works the same way as Agda as described
in Ulf Norell’s thesis.

General idea is that high level languages will provide a translation to TT.
In the `Idris/`

namespace we define the high level syntax for Idris, which
translates to TTImp by desugaring operators, do notation, etc.

There is a separate linearity check after elaboration, which updates types of
holes (and is aware of case blocks). This is implemented in
`Core.LinearCheck`

. During this check, we also recalculate the multiplicities
in hole applications so that they are displayed appropriately (e.g. if a
linear variable is unused elsewhere, it will always appear with multiplicity
1 in holes).

Where to find things:

`Core/`

– anything related to the core TT, typechecking and unification`TTImp/`

– anything related to the implicit TT and its elaboration`TTImp/Elab/`

– Elaboration state and elaboration of terms`TTImp/Interactive/`

– Interactive editing infrastructure

`Parser/`

– various utilities for parsing and lexing TT and TTImp (and other things)`Utils/`

– some generally useful utilities`Idris/`

– anything relating to the high level language, translating to TTImp`Idris/Elab/`

– High level construct elaboration machinery (e.g. interfaces)

`Compiler/`

– back ends

#### The Core Type, and Ref¶

`Core`

is a “monad” (not really, for efficiency reasons, at the moment…)
supporting `Error`

’s and `IO`

(I did originally plan to allow restricting this to
some specific IO operations, but haven’t yet). The raw syntax is defined by a
type `RawImp`

which has a source location at each node, and any errors in
elaboration note the location at the point where the error occurred, as
a file context `FC`

.

`Ref`

is essentially an `IORef`

. Typically we pass them implicitly and use
labels to disambiguate which one we mean. See `Core.Core`

for their
definition. Again, `IORef`

is for efficiency - even if it would be neater to
use a state monad this turned out to be about 2-3 times faster, so I’m
going with the “ugly” choice…

#### Term representation¶

Terms in the core language are indexed by a list of the names in scope, most recently defined first:

```
data Term : List Name -> Type
```

This means that terms are always well scoped, and we can use the type system to keep us right when manipulating names. For example, we have:

```
Local : FC -> (isLet : Maybe Bool) ->
(idx : Nat) -> (0 p : IsVar name idx vars) -> Term vars
```

So local variables are represented by an index into the local context (a de
Bruijn index, `idx`

), and a proof, erased at run time, that the index
is valid. So everything is de Bruijn indexed, but the type checker still
keeps track of the indices so that we don’t have to think too hard!

`Core.TT`

contains various handy tools for manipulating terms with their
indices, such as:

```
weaken : Term vars -> Term (n :: vars) -- actually in an interface, Weaken
embed : Term vars -> Term (ns ++ vars)
refToLocal : (x : Name) -> -- explicit name of a reference
(new : Name) -> -- name to bind as
Term vars -> Term (new :: vars)
```

Note that the types are explicit about when the `vars`

needs to be passed at
run time, and when it isn’t. Mostly where it’s needed it’s to help with
displaying names, or name generation, rather than any fundamental reason in
the core. In general, this isn’t expensive at run time.

Environments, defined in `Core.Env`

, map local variables to binders:

```
data Env : (tm : List Name -> Type) -> List Name -> Type
```

A binders is typically a *lambda*, a *pi*, or a *let* (with a value), but can
also be a *pattern variable*. See the definition of `TT`

for more details.
Where we have a term, we usually also need an `Env`

.

We also have values, which are in head normal form, and defined in
`Core.Value`

:

```
data NF : List Name -> Type
```

We can convert a term to a value by normalising…

```
nf : {vars : _} ->
Defs -> Env Term vars -> Term vars -> Core (NF vars)
```

…and back again, by quoting:

```
quote : {vars : _} ->
Defs -> Env Term vars -> tm vars -> Core (Term vars)
```

Both `nf`

and `quote`

are defined in `Core.Normalise`

. We don’t
always know whether we’ll need to work with `NF`

or `Term`

, so
we also have a “glued” representation, `Glued vars`

, again defined in
`Core.Normalise`

, which lazily computes either a `NF`

or `Term`

as
required. Elaborating a term returns the type as a `Glued vars`

.

`Term`

separates `Ref`

(global user defined names) from `Meta`

, which
are globally defined metavariables. For efficiency, metavariables are only
substituted into terms if they have non-0 multiplicity, to preserve sharing as
much as possible.

#### Unification¶

Unification is probably the most important part of the elaboration process,
and infers values for implicit arguments. That is, it finds values for the
things which are referred to by `Meta`

in `Term`

. It is defined in
`Core.Unify`

, as the top level unification function has the following
type:

```
unify : Unify tm =>
{vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
UnifyInfo ->
FC -> Env Term vars ->
tm vars -> tm vars ->
Core UnifyResult
```

The `Unify`

interface is there because it is convenient to be able to
define unification on `Term`

and `NF`

, as well as `Closure`

(which
is part of `NF`

to represent unevaluated arguments to constructors).

This is one place where indexing over `vars`

is extremely valuable: we
have to keep the environment consistent, so unification won’t accidentally
introduce any scoping bugs!

Idris 2 implements pattern unification - see Adam Gundry’s thesis for an accessible introduction.

#### Context¶

`Core.Context`

defines all the things needed for TT. Most importantly: `Def`

gives definitions of names (case trees, builtins, constructors and
holes, mostly); `GlobalDef`

is a definition with all the other information
about it (type, visibility, totality, etc); `Context`

is a context mapping names
to `GlobalDef`

, and `Defs`

is the core data structure with everything needed to
typecheck more definitions.

The main Context type stores definitions in an array, indexed by a “resolved
name id”, an integer, for fast look up. This means that it also needs to be
able to convert between resolved names and full names. The `HasNames`

interface defines methods for going back and forth between structures with
human readable names, and structures with resolved integer names.

Since we store names in an array, all the lookup functions need to be in the
`Core`

monad. This also turns out to help with loading checked files (see
below).

#### Elaboration Overview¶

Elaboration of `RawImp`

to `TT`

is driven by `TTImp.Elab`

, with the
top level function for elaborating terms defined in `TTImp.Elab.Term`

,
support functions defined in `TTImp.Elab.Check`

, and elaborators for the
various TTImp constructs defined in separate files under `TTImp.Elab.*`

.

#### Laziness¶

Like Idris 1, laziness is marked in types using `Lazy`

, `Delay`

and `Force`

, or
`Inf`

(instead of `Lazy`

) for codata. Unlike Idris 1, these are language primitives
rather than special purpose names.

Implicit laziness resolution is handled during unification (in `Core.Unify`

).
When unification is invoked (by `convert`

in `TTImp.Elab.Check`

) with
the `withLazy`

flag set, it checks whether it is converting a lazy type
with a non-lazy type. If so, it continues with unification, but returning
that either a `Force`

or `Delay`

needs inserting as appropriate.

#### TTC format¶

We can save things to binary if we have an implementation of the TTC interface
for it. See `Utils.Binary`

to see how this is done. It uses a global reference
`Ref Bin Binary`

which uses `Data.Buffer`

underneath.

When we load checked TTC files, we don’t process the definitions immediately,
but rather store them as a `ContextEntry`

, which is either a `Binary`

blob, or
a processed definition. We only process the definitions the first time they
are looked up, since converting Binary to the definition is fairly costly
(due to having to construct a lot of AST nodes), and often definitions in an
imported file are never used.

#### Bound Implicits¶

The `RawImp`

type has a constructor `IBindVar`

. The first time we encounter an
`IBindVar`

, we record the name as one which will be implicitly bound. At the
end of elaboration, we decide which holes should turn into bound variables
(Pi bound in types, Pattern bound on a LHS, still holes on the RHS) by
looking at the list of names bound as `IBindVar`

, the things they depend on,
and sorting them so that they are bound in dependency order. This happens
in `TTImp.Implicit.getToBind`

.

Once we know what the bound implicits need to be, we bind them in
`bindImplicits`

. Any application of a hole which stands for a bound implicit
gets turned into a local binding (either Pi or Pat as appropriate, or PLet for
@-patterns).

#### Unbound Implicits¶

Any name beginning with a lower case letter is considered an unbound implicit. They are elaborated as holes, which may depend on the initial environment of the elaboration, and after elaboration they are converted to an implicit pi binding, with multiplicity 0. So, for example:

```
map : {f : _} -> (a -> b) -> f a -> f b
```

becomes:

```
map : {f : _} -> {0 a : _} -> {0 b : _} -> (a -> b) -> f a -> f b
```

Bindings are ordered according to dependency. It’ll infer any additional names, e.g. in:

```
lookup : HasType i xs t -> Env xs -> t
```

… where `xs`

is a `Vect n a`

, it infers bindings for `n`

and `a`

.

The `%unbound_implicits`

directive means that it will no longer automatically
bind names (that is, `a`

and `b`

in `map`

above) but it will still
infer the types for any additional names, e.g. if you write:

```
lookup : forall i, x, t . HasType i xs t -> Env xs -> t
```

… it will still infer a type for `xs`

and infer bindings for `n`

and
`a`

.

#### Implicit arguments¶

When we encounter an implicit argument (`_`

in the raw syntax, or added when
we elaborate an application and see that there is an implicit needed) we
make a new hole which is a fresh name applied to the current environment,
and return that as the elaborated term. This happens in `TTImp.Elab.Check`

,
with the function `metaVar`

. If there’s enough information elsewhere we’ll
find the definition of the hole by unification.

We never substitute holes in a term during elaboration and rely on normalisation if we need to look inside it. If there are holes remaining after elaboration of a definition, report an error (it’s okay for a hole in a type as long as it’s resolved by the time the definition is done).

See `Elab.App.makeImplicit`

, `Elab.App.makeAutoImplicit`

to see where we
add holes for the implicit arguments in applications.

`Elab.App`

does quite a lot of tricky stuff! In an attempt to help with
resolving ambiguous names and record updates, it will sometimes delay
elaboration of an argument (see `App.checkRestApp`

) so that it can get more
information about its type first.

`Core.Unify.solveConstraints`

revisits all of the currently unsolved holes
and constrained definitions, and tries again to unify any constraints which
they require. It also tries to resolve anything defined by proof search.
The current state of unification is defined in `Core.UnifyState`

, and
unification constraints record which metavariables are blocking them. This
improves performance, since we’ll only retry a constraint if one of the
blocking metavariables has been resolved.

#### Additional type inference¶

A `?`

in a type means “infer this part of the type”. This is distinct from
`_`

in types, which means “I don’t care what this is”. The distinction is in
what happens when inference fails. If inference fails for `_`

, we implicitly
bind a new name (just like pattern matching on the lhs - i.e. it means match
anything). If inference fails for `?`

, we leave it as a hole and try to fill
it in later. As a result, we can say:

```
foo : Vect ? Int
foo = [1,2,3,4]
```

… and the `?`

will be inferred to be 4. But if we say:

```
foo : Vect _ Int
foo = [1,2,3,4]
```

… we’ll get an error, because the `_`

has been bound as a new name.
Both `?`

and `_`

are represented in `RawImp`

by the `Implicit`

constructor, which has a boolean flag meaning “bind if unresolved”.

So the meaning of `_`

is now consistent on the lhs and in types (i.e. it
means infer a value and bind a variable on failure to infer anything). In
practice, using `_`

will get you the old Idris behaviour, but `?`

might
get you a bit more type inference.

#### Auto Implicits¶

Auto implicits are resolved by proof search, and can be given explicit
arguments in the same way as ordinary implicits: i.e. `{x = exp}`

to give
`exp`

as the value for auto implicit `x`

. Interfaces are syntactic sugar for
auto implicits (it is the same resolution mechanism - interfaces translate into
records, and implementations translate into hints for the search).

The argument syntax `@{exp}`

means that the value of the next auto implicit
in the application should be `exp`

- this is the same as the syntax for
invoking named implementations in Idris 1, but interfaces and auto implicits
have been combined now.

Implicit search is defined in `Core.AutoSearch`

. It will only begin a
search if all the *determining arguments* of the goal are defined, meaning
that they don’t contain *any* holes. This avoids committing too early to
the solution of a hole by resolving it by search, rather than unification,
unless a programmer has explicitly said (via a `search`

option on a data
type) that that’s what they want.

#### Dot Patterns¶

`IMustUnify`

is a constructor of `RawImp`

. When we elaborate this, we generate a
hole, then elaborate the term, and add a constraint that the generated hole
must unify with the term which was explicitly given (in `UnifyState.addDot`

),
without resolving any holes. This is finally checked in `UnifyState.checkDots`

.

#### Proof Search¶

A definition constructed with `Core.Context.BySearch`

is a hole which will
be resolved by searching for something which fits the type. This happens in
`Core.AutoSearch`

. It checks all possible hints for a term, to ensure that
only one is possible.

#### @-Patterns¶

Names which are bound in types are also bound as @-patterns, meaning that functions have access to them. For example, we can say:

```
vlength : {n : Nat} -> Vect n a -> Nat
vlength [] = n
vlength (x :: xs) = n
```

As patterns are implemented as a constructor of `TT`

, which makes a lot
of things more convenient (especially case tree compilation).

#### Linear Types¶

Following Conor McBride and Bob Atkey’s work, all binders have a multiplicity
annotation (`RigCount`

). After elaboration in `TTImp.Elab`

, we do a
separate linearity check which: a) makes sure that linear variables are used
exactly once; b) updates hole types to properly reflect usage information.

#### Local definitions¶

We elaborate relative to an environment, meaning that we can elaborate local function definitions. We keep track of the names being defined in a nested block of declarations, and ensure that they are lifted to top level definitions in TT by applying them to every name in scope.

Since we don’t know how many times a local definition will be applied, in general, anything bound with multiplicity 1 is passed to the local definition with multiplicity 0, so if you want to use it in a local definition, you need to pass it explicitly.

#### Case blocks¶

Similar to local definitions, these are lifted to top level definitions which represent the case block, which is immediately applied to the scrutinee of the case. We don’t attempt to calculate the multiplicities of arguments when elaborating the case block, since we’ll probably get it wrong - instead, these are checked during linearity checking, which knows about case functions.

Case blocks in the scope of local definitions are tricky, because the names
need to match up, and the types might be refined, but we also still need to
apply the local names to the scope in which they were defined. This is a bit
fiddly, and dealt with by the `ICaseLocal`

constructor of `RawImp`

.

Various parts of the system treat case blocks specially, even though they aren’t strictly part of the core. In particular, these are linearity checking and totality checking.

#### Parameters¶

The parameters to a data type are taken to be the arguments which appear, unchanged, in the same position, everywhere across a data definition.

#### Erasure¶

Unbound implicits are given `0`

multiplicity, so the rule is now that if you
don’t explicitly write it in the type of a function or constructor, the
argument is erased at run time.

Elaboration and the case tree compiler check ensure that 0-multiplicity arguments are not inspected in case trees. In the compiler, 0-multiplicity arguments to constructors are erased completely, whereas 0-multiplicity arguments to functions are replaced with a placeholder erased value.

#### Namespaces and name visibility¶

Same rules mostly apply as in Idris 1. The difference is that visibility is
*per namespace* not *per file* (that is, files have no relevance other except
in that they introduce their own namespace, and in that they allow separate
typechecking).

One effect of this is that when a file defines nested namespaces, the inner
namespace can see what’s in the outer namespace, but not vice versa unless
names defined in the inner namespace are explicitly exported. The visibility
modifiers `export`

, `public export`

, and `private`

control whether the name
can be seen in any other namespace, and it’s nothing to do with the file
they’re defined in at all.

Unlike Idris 1, there is no restriction on whether public definitions can
refer to private names. The only restriction on `private`

names is that
they can’t be referred to directly (i.e. in code) outside the namespace.

#### Records¶

Records are part of TTImp (rather than the surface language). Elaborating a
record declaration creates a data type and associated projection functions.
Record setters are generated on demand while elaborating TTImp (in
`TTImp.Elab.Record`

). Setters are translated directly to `case`

blocks,
which means that update of dependent fields works as one might expect (i.e.
it’s safe as long as all of the fields are updated at the same time
consistently).

### The IDE Protocol¶

The Idris REPL has two modes of interaction: a human-readable syntax designed for direct use in a terminal, and a machine-readable syntax designed for using Idris as a backend for external tools.

The IDE-Protocol is versioned separately from the Idris compiler. The first version of Idris (written in Haskell and is at v1.3.3) implements version one of the IDE Protocol, and Idris2 (self-hosting and is at v.0.3.0) implements version two of the IDE Protocol.

#### Protocol Overview¶

The communication protocol is of asynchronous request-reply style: a single request from the client is handled by Idris at a time. Idris waits for a request on its standard input stream, and outputs the answer or answers to standard output. The result of a request can be either success, failure, or intermediate output; and furthermore, before the result is delivered, there might be additional meta-messages.

A reply can consist of multiple messages: any number of messages to inform the user about the progress of the request or other informational output, and finally a result, either `ok`

or `error`

.

The wire format is the length of the message in characters, encoded in 6 characters hexadecimal, followed by the message encoded as S-expression (sexp). Additionally, each request includes a unique integer (counting upwards), which is repeated in all messages corresponding to that request.

An example interaction from loading the file `/home/hannes/empty.idr`

looks as follows on the wire::

```
00002a((:load-file "/home/hannes/empty.idr") 1)
000039(:write-string "Type checking /home/hannes/empty.idr" 1)
000025(:set-prompt "/home/hannes/empty" 1)
000032(:return (:ok "Loaded /home/hannes/empty.idr") 1)
```

The first message is the request from idris-mode to load the specific file, which length is hex 2a, decimal 42 (including the newline at the end).
The request identifier is set to 1.
The first message from Idris is to write the string `Type checking /home/hannes/empty.idr`

, another is to set the prompt to `*/home/hannes/empty`

.
The answer, starting with `:return`

is `ok`

, and additional information is that the file was loaded.

There are three atoms in the wire language: numbers, strings, and symbols. The only compound object is a list, which is surrounded by parenthesis. The syntax is:

```
A ::= NUM | '"' STR '"' | ':' ALPHA+
S ::= A | '(' S* ')' | nil
```

where `NUM`

is either 0 or a positive integer, `ALPHA`

is an alphabetical character, and `STR`

is the contents of a string, with `"`

escaped by a backslash.
The atom `nil`

is accepted instead of `()`

for compatibility with some regexp pretty-printing routines.

The state of the Idris process is mainly the active file, which needs to be kept synchronised between the editor and Idris.
This is achieved by the already seen `:load-file`

command.

#### Protocol Versioning¶

When interacting with Idris through the IDE Protocol the initial message sent by the running Idris Process is the version (major and minor) of the IDE Protocol being used.

The expected message has the following format:

`(:protocol-version MAJOR MINOR)`

IDE Clients can use this to help support multiple Idris versions.

#### Commands¶

The available commands are listed below. They are compatible with Version 1 and 2.0 of the protocol unless otherwise stated.

`(:load-file FILENAME [LINE])`

- Load the named file. If a
`LINE`

number is provided, the file is only loaded up to that line. Otherwise, the entire file is loaded. Version 2 of the IDE Protocol Requires that the file name is quoted.`(:cd FILEPATH)`

- Change the working direction to the given
`FILEPATH`

Version 2 of the IDE Protocol Requires that the path is quoted.`(:interpret STRING)`

- Interpret
`STRING`

at the Idris REPL, returning a highlighted result.`(:type-of STRING)`

- Return the type of the name, written with Idris syntax in the
`STRING`

. The reply may contain highlighting information.`(:case-split LINE NAME)`

- Generate a case-split for the pattern variable
`NAME`

on program line`LINE`

. The pattern-match cases to be substituted are returned as a string with no highlighting.`(:add-clause LINE NAME)`

- Generate an initial pattern-match clause for the function declared as
`NAME`

on program line`LINE`

. The initial clause is returned as a string with no highlighting.`(:add-proof-clause LINE NAME)`

- Add a clause driven by the
`<==`

syntax.`(:add-missing LINE NAME)`

- Add the missing cases discovered by totality checking the function declared as
`NAME`

on program line`LINE`

. The missing clauses are returned as a string with no highlighting.`(:make-with LINE NAME)`

- Create a with-rule pattern match template for the clause of function
`NAME`

on line`LINE`

. The new code is returned with no highlighting.`(:make-case LINE NAME)`

- Create a case pattern match template for the clause of function
`NAME`

on line`LINE`

. The new code is returned with no highlighting.`(:make-lemma LINE NAME)`

- Create a top level function with a type which solves the hole named
`NAME`

on line`LINE`

.`(:proof-search LINE NAME HINTS)`

- Attempt to fill out the holes on
`LINE`

named`NAME`

by proof search.`HINTS`

is a possibly-empty list of additional things to try while searching.`(:docs-for NAME [MODE])`

- Look up the documentation for
`NAME`

, and return it as a highlighted string. If`MODE`

is`:overview`

, only the first paragraph of documentation is provided for`NAME`

. If`MODE`

is`:full`

, or omitted, the full documentation is returned for`NAME`

.`(:apropos STRING)`

- Search the documentation for mentions of
`STRING`

, and return any found as a list of highlighted strings.`(:metavariables WIDTH)`

- List the currently-active holes, with their types pretty-printed with
`WIDTH`

columns.`(:who-calls NAME)`

- Get a list of callers of
`NAME`

.`(:calls-who NAME)`

- Get a list of callees of
`NAME`

.`(:browse-namespace NAMESPACE)`

- Return the contents of
`NAMESPACE`

, like`:browse`

at the command-line REPL.`(:normalise-term TM)`

- Return a highlighted string consisting of the results of normalising the serialised term
`TM`

(which would previously have been sent as the`tt-term`

property of a string).`(:show-term-implicits TM)`

- Return a highlighted string consisting of the results of making all arguments in serialised term
`TM`

(which would previously have been sent as the`tt-term`

property of a string) explicit.`(:hide-term-implicits TM)`

- Return a highlighted string consisting of the results of making all arguments in serialised term
`TM`

(which would previously have been sent as the`tt-term`

property of a string) follow their usual implicitness setting.`(:elaborate-term TM)`

- Return a highlighted string consisting of the core language term corresponding to serialised term
`TM`

(which would previously have been sent as the`tt-term`

property of a string).`(:print-definition NAME)`

- Return the definition of
`NAME`

as a highlighted string.`(:repl-completions NAME)`

- Search names, types and documentations which contain
`NAME`

. Return the result of tab-completing`NAME`

as a REPL command.`:version`

- Return the version information of the Idris compiler.

#### New For Version 2¶

New in Version 2 of the protocol are:

`(:generate-def LINE NAME)`

- Generate a definition
`(:generate-def-next)`

- Replace the previous generated definition with next definition.
`(:proof-search-next)`

- Replace the previous proof search result with the next one.

#### Possible Replies¶

Possible replies include a normal final reply::

```
(:return (:ok SEXP [HIGHLIGHTING]))
(:return (:error String [HIGHLIGHTING]))
```

A normal intermediate reply::

```
(:output (:ok SEXP [HIGHLIGHTING]))
(:output (:error String [HIGHLIGHTING]))
```

Informational and/or abnormal replies::

```
(:write-string String)
(:set-prompt String)
(:warning (FilePath (LINE COL) (LINE COL) String [HIGHLIGHTING]))
```

#### Output Highlighting¶

Idris mode supports highlighting the output from Idris. In reality, this highlighting is controlled by the Idris compiler. Some of the return forms from Idris support an optional extra parameter: a list mapping spans of text to metadata about that text. Clients can then use this list both to highlight the displayed output and to enable richer interaction by having more metadata present. For example, the Emacs mode allows right-clicking identifiers to get a menu with access to documentation and type signatures.

A particular semantic span is a three element list. The first element of the list is the index at which the span begins, the second element is the number of characters included in the span, and the third is the semantic data itself. The semantic data is a list of lists. The head of each list is a key that denotes what kind of metadata is in the list, and the tail is the metadata itself.

- The following keys are available:
`name`

- gives a reference to the fully-qualified Idris name
`implicit`

- provides a Boolean value that is True if the region is the name of an implicit argument
`decor`

- describes the category of a token, which can be
`type`

,`function`

,`data`

,`keyword`

, or`bound`

. `source-loc`

states that the region refers to a source code location. Its body is a collection of key-value pairs, with the following possibilities:

`filename`

- provides the filename
`start`

- provides the line and column that the source location starts at as a two-element tail
`end`

- provides the line and column that the source location ends at as a two-element tail

`text-formatting`

- provides an attribute of formatted text. This is for use with natural-language text, not code, and is presently emitted only from inline documentation. The potential values are
`bold`

,`italic`

, and`underline`

. `link-href`

- provides a URL that the corresponding text is a link to.
`quasiquotation`

- states that the region is quasiquoted.
`antiquotation`

- states that the region is antiquoted.
`tt-term`

- A serialised representation of the Idris core term corresponding to the region of text.

#### Source Code Highlighting¶

Idris supports instructing editors how to colour their code. When elaborating source code or REPL input, Idris will locate regions of the source code corresponding to names, and emit information about these names using the same metadata as output highlighting.

These messages will arrive as replies to the command that caused elaboration to occur, such as `:load-file`

or `:interpret`

.
They have the format::

```
(:output (:ok (:highlight-source POSNS)))
```

where `POSNS`

is a list of positions to highlight. Each of these is a two-element list whose first element is a position (encoded as for the `source-loc`

property above) and whose second element is highlighting metadata in the same format used for output.

## Idris2 Reference Guide¶

Note

The documentation for Idris 2 has been published under the Creative
Commons CC0 License. As such to the extent possible under law, *The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.

More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/

This is a placeholder, to get set up with readthedocs.

### Environment Variables¶

Idris 2 recognises a number of environment variables, to decide where to look for packages, external libraries, code generators, etc. It currently recognises, in approximately the order you’re likely to need them:

`EDITOR`

- Sets the editor used in REPL :e command`IDRIS2_CG`

- Sets which code generator to use when compiling programs`IDRIS2_PACKAGE_PATH`

- Lists the directories where Idris2 looks for packages, in addition to the defaults (which are under the`IDRIS2_PREFIX`

and in the`depends`

subdirectory of the current working directory). Directories are separated by a`:`

, or a`;`

on Windows`IDRIS2_PATH`

- Places Idris2 looks for import files, in addition to the imports in packages`IDRIS2_DATA`

- Places Idris2 looks for its data files. These are typically support code for code generators.`IDRIS2_LIBS`

- Places Idris2 looks for libraries used by code generators.`IDRIS2_PREFIX`

- Gives the Idris2 installation prefix`CHEZ`

- Sets the location of the`chez`

executable used in Chez codegen`RACKET`

- Sets the location of the`racket`

executable used in Racket codegen`RACKET_RACO`

- Sets the location of the`raco`

executable used in Racket codegen`GAMBIT_GSI`

- Sets the location of the`gsi`

executable used in Gambit codegen`GAMBIT_GSC`

- Sets the location of the`gsc`

executable used in Gambit codegen`GAMBIT_GSC_BACKEND`

- Sets the`gsc`

executable backend argument`IDRIS2_CC`

- Sets the location of the C compiler executable used in RefC codegen`CC`

- Sets the location of the C compiler executable used in RefC codegen`NODE`

- Sets the location of the`node`

executable used in Node codegen`PATH`

- used to search for executables in certain codegens

### Dot syntax for records¶

Long story short, `.field`

is a postfix projection operator that binds
tighter than function application.

#### Lexical structure¶

`.foo`

is a valid name, which stands for record fields (new`Name`

constructor`RF "foo"`

)`Foo.bar.baz`

starting with uppercase`F`

is one lexeme, a namespaced identifier:`DotSepIdent ["baz", "bar", "Foo"]`

`foo.bar.baz`

starting with lowercase`f`

is three lexemes:`foo`

,`.bar`

,`.baz`

`.foo.bar.baz`

is three lexemes:`.foo`

,`.bar`

,`.baz`

- If you want
`Constructor.field`

, you have to write`(Constructor).field`

. - All module names must start with an uppercase letter.

#### New syntax of `simpleExpr`

¶

Expressions binding tighter than application (`simpleExpr`

), such as variables or parenthesised expressions, have been renamed to `simplerExpr`

, and an extra layer of syntax has been inserted.

```
simpleExpr ::= (.field)+ -- parses as PPostfixAppPartial
| simplerExpr (.field)+ -- parses as PPostfixApp
| simplerExpr -- (parses as whatever it used to)
```

`(.foo)`

is a name, so you can use it to e.g. define a function called`.foo`

(see`.squared`

below)`(.foo.bar)`

is a parenthesised expression

#### Desugaring rules¶

`(.field1 .field2 .field3)`

desugars to`(\x => .field3 (.field2 (.field1 x)))`

`(simpleExpr .field1 .field2 .field3)`

desugars to`((.field .field2 .field3) simpleExpr)`

#### Record elaboration¶

- there is a new pragma
`%prefix_record_projections`

, which is`on`

by default - for every field
`f`

of a record`R`

, we get:- projection
`f`

in namespace`R`

(exactly like now), unless`%prefix_record_projections`

is`off`

- projection
`.f`

in namespace`R`

with the same definition

- projection

#### Example code¶

```
record Point where
constructor MkPoint
x : Double
y : Double
```

This record creates two projections:
* `.x : Point -> Double`

* `.y : Point -> Double`

Because `%prefix_record_projections`

are `on`

by default, we also get:
* `x : Point -> Double`

* `y : Point -> Double`

To prevent cluttering the ordinary global name space with short identifiers, we can do this:

```
%prefix_record_projections off
record Rect where
constructor MkRect
topLeft : Point
bottomRight : Point
```

For `Rect`

, we don’t get the prefix projections:

```
Main> :t topLeft
(interactive):1:4--1:11:Undefined name topLeft
Main> :t .topLeft
\{rec:0} => .topLeft rec : ?_ -> Point
```

Let’s define some constants:

```
pt : Point
pt = MkPoint 4.2 6.6
rect : Rect
rect =
MkRect
(MkPoint 1.1 2.5)
(MkPoint 4.3 6.3)
```

User-defined projections work, too. (Should they?)

```
(.squared) : Double -> Double
(.squared) x = x * x
```

Finally, the examples:

```
main : IO ()
main = do
-- desugars to (.x pt)
-- prints 4.2
printLn $ pt.x
-- prints 4.2, too
-- maybe we want to make this a parse error?
printLn $ pt .x
-- prints 10.8
printLn $ pt.x + pt.y
-- works fine with namespacing
-- prints 4.2
printLn $ (Main.pt).x
-- the LHS can be an arbitrary expression
-- prints 4.2
printLn $ (MkPoint pt.y pt.x).y
-- user-defined projection
-- prints 17.64
printLn $ pt.x.squared
-- prints [1.0, 3.0]
printLn $ map (.x) [MkPoint 1 2, MkPoint 3 4]
-- .topLeft.y desugars to (\x => .y (.topLeft x))
-- prints [2.5, 2.5]
printLn $ map (.topLeft.y) [rect, rect]
-- desugars to (.topLeft.x rect + .bottomRight.y rect)
-- prints 7.4
printLn $ rect.topLeft.x + rect.bottomRight.y
-- qualified names work, too
-- all these print 4.2
printLn $ Main.Point.(.x) pt
printLn $ Point.(.x) pt
printLn $ (.x) pt
printLn $ .x pt
-- haskell-style projections work, too
printLn $ Main.Point.x pt
printLn $ Point.x pt
printLn $ (x) pt
printLn $ x pt
-- record update syntax uses dots now
-- prints 3.0
printLn $ (record { topLeft.x = 3 } rect).topLeft.x
-- but for compatibility, we support the old syntax, too
printLn $ (record { topLeft->x = 3 } rect).topLeft.x
-- prints 2.1
printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x
printLn $ (record { topLeft->x $= (+1) } rect).topLeft.x
```

Parses but does not typecheck:

```
-- parses as: map.x [MkPoint 1 2, MkPoint 3 4]
-- maybe we should disallow spaces before dots?
--
printLn $ map .x [MkPoint 1 2, MkPoint 3 4]
```

### Literate Programming¶

Idris2 supports several types of literate mode styles.

The unlit’n has been designed based such that we assume that we are parsing markdown-like languages The unlit’n is performed by a Lexer that uses a provided literate style to recognise code blocks and code lines. Anything else is ignored. Idris2 also provides support for recognising both ‘visible’ and ‘invisible’ code blocks using ‘native features’ of each literate style.

A literate style consists of:

- a list of String encoded code block deliminators;
- a list of line indicators; and
- a list of valid file extensions.

Lexing is simple and greedy in that when consuming anything that is a code blocks we treat everything as code until we reach the closing deliminator. This means that use of verbatim modes in a literate file will also be treated as active code.

In future we should add support for literate `LaTeX`

files, and potentially other common document formats.
But more importantly, a more intelligent processing of literate documents using a pandoc like library in Idris such as: Edda <https://github.com/jfdm/edda> would also be welcome.

#### Bird Style Literate Files¶

We treat files with an extension of `.lidr`

as bird style literate files.

Bird notation is a classic literate mode found in Haskell, (and Orwell) in which visible code lines begin with `>`

and hidden lines with `<`

.
Other lines are treated as documentation.

Note

We have diverged from `lhs2tex`

in which `<`

is traditionally used to display inactive code.
Bird-style is presented as is, and we recommended use of the other styles for much more comprehensive literate mode.

#### Embedding in Markdown-like documents¶

While Bird Style literate mode is useful, it does not lend itself well to more modern markdown-like notations such as Org-Mode and CommonMark. Idris2 also provides support for recognising both ‘visible’ and ‘invisible’ code blocks and lines in both CommonMark and OrgMode documents using native code blocks and lines..

The idea being is that:

**Visible**content will be kept in the pretty printer’s output;**Invisible**content will be removed; and**Specifications**will be displayed*as is*and not touched by the compiler.

##### OrgMode¶

We treat files with an extension of `.org`

as org-style literate files.
Each of the following markup is recognised regardless of case:

Org mode source blocks for idris sans options are recognised as visible code blocks:

#+begin_src idris data Nat = Z | S Nat #+end_src

Comment blocks that begin with

`#+BEGIN_COMMENT idris`

are treated as invisible code blocks:#+begin_comment idris data Nat = Z | S Nat #+end_comment

Visible code lines, and specifications, are not supported. Invisible code lines are denoted with

`#+IDRIS:`

:`#+IDRIS: data Nat = Z | S Nat`

Specifications can be given using OrgModes plain source or example blocks:

#+begin_src map : (f : a -> b) -> List a -> List b map f _ = Nil #+end_src

##### CommonMark¶

We treat files with an extension of `.md`

and `.markdown`

as CommonMark style literate files.

CommonMark source blocks for idris sans options are recognised as visible code blocks:

```idris data Nat = Z | S Nat ``` ~~~idris data Nat = Z | S Nat ~~~

Comment blocks of the form

`<!-- idris\n ... \n -->`

are treated as invisible code blocks:<!-- idris data Nat = Z | S Nat -->

Code lines are not supported.

Specifications can be given using CommonMark’s pre-formatted blocks (indented by four spaces) or unlabelled code blocks.:

Compare ``` map : (f : a -> b) -> List a -> List b map f _ = Nil ``` with map : (f : a -> b) -> List a -> List b map f _ = Nil

##### LaTeX¶

We treat files with an extension of `.tex`

and `.ltx`

as LaTeX style literate files.

We treat environments named

`code`

as visible code blocks:\begin{code} data Nat = Z | S Nat \end{code}

We treat environments named

`hidden`

as invisible code blocks:\begin{hidden} data Nat = Z | S Nat \end{hidden}

Code lines are not supported.

Specifications can be given using user defined environments.

We do not provide definitions for these code blocks and ask the user to define them.
With one such example using `fancyverbatim`

and `comment`

packages as:

```
\usepackage{fancyvrb}
\DefineVerbatimEnvironment
{code}{Verbatim}
{}
\usepackage{comment}
\excludecomment{hidden}
```

### Overloaded literals¶

The compiler provides directives for literals overloading, respectively
`%stringLit <fun>`

and `%integerLit <fun>`

for string and integer literals. During
elaboration, the given function is applied to the corresponding literal.
In the Prelude these functions are set to `fromString`

and `fromInteger`

.

The interface `FromString ty`

provides the `fromString : String -> ty`

function,
while the `Num ty`

interface provides the `fromInteger : Integer -> ty`

function
for all numerical types.

#### Restricted overloads¶

Although the overloading of literals can be achieved by implementing the interfaces
described above, in principle only a function with the correct signature and name
is enough to achieve the desired behaviour. This can be exploited to obtain more
restrictive overloading such as converting literals to `Fin n`

values, where
integer literals greater or equal to n are not constructible values for the type.
Additional implicit arguments can be added to the function signature, in particular
auto implicit arguments for searching proofs. As an example, this is the implementation
of `fromInteger`

for `Fin n`

.

```
public export
fromInteger : (x : Integer) -> {n : Nat} ->
{auto prf : (IsJust (integerToFin x n))} ->
Fin n
fromInteger {n} x {prf} with (integerToFin x n)
fromInteger {n} x {prf = ItIsJust} | Just y = y
```

The `prf`

auto implicit is an automatically constructed proof (if possible) that
the literal is suitable for the `Fin n`

type. The restricted behaviour can be
observed in the REPL, where the failure to construct a valid proof is caught during
the type-checking phase and not at runtime:

```
Main> the (Fin 3) 2
FS (FS FZ)
Main> the (Fin 3) 5
(interactive):1:13--1:14:Can't find an implementation for IsJust (integerToFin 5 3) at:
1 the (Fin 3) 5
```