# 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 , 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
```

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.