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