.. _sect-misc: **********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 beomitted when they can be inferred by the type checker [#IdrisType]_, e.g. .. code-block:: idris     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 typechecking but by searching the context for an appropriate value, orconstructing a proof. For example, the following definition of ``head``which requires a proof that the list is non-empty: .. code-block:: idris     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 itsvalue is known or because a proof already exists in the context, theproof can be constructed automatically. Auto implicit arguments allowthis to happen silently. We define ``head`` as follows: .. code-block:: idris     head : (xs : List a) -> {auto p : isCons xs = True} -> a    head (x :: xs) = x The ``auto`` annotation on the implicit argument means that Idriswill attempt to fill in the implicit argument by searching for a valueof the appropriate type. In fact, internally, this is exactly how interfaceresolution 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: .. code-block:: idris     head xs {p = ?headProof} Default implicit arguments--------------------------- Besides having Idris automatically find a value of a given type, sometimes wewant to have an implicit argument with a specific default value. In Idris, we cando this using the ``default`` annotation. While this is primarily intended to assistin 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 fibonaccinumber as 0), we could write: .. code-block:: idris 	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 theintended use of the ``default`` annotation. It is included here for illustrative purposesonly. Usually, ``default`` is used to provide things like a custom proof search script. Literate programming==================== [NOT YET IN IDRIS 2] Like Haskell, Idris supports *literate* programming. If a file hasan extension of ``.lidr`` then it is assumed to be a literate file. Inliterate programs, everything is assumed to be a comment unless the linebegins with a greater than sign ``>``, for example: .. code-block:: literate-idris   :force:     > 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 aprogram line (beginning with ``>``) and a comment line (beginning withany other character). Cumulativity============ [NOT YET IN IDRIS 2] Since values can appear in types and *vice versa*, it is natural thattypes 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 <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,so internally there is a *hierarchy* of types (or *universes*): .. code-block:: idris     Type : Type 1 : Type 2 : Type 3 : ... Universes are *cumulative*, that is, if ``x : Type n`` we can also havethat ``x : Type m``, as long as ``n < m``. The typechecker generatessuch universe constraints and reports an error if any inconsistenciesare found. Ordinarily, a programmer does not need to worry about this,but it does prevent (contrived) programs such as the following: .. code-block:: idris     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 universehierarchy — ``myid``\ ’s first argument is a ``Type``, which cannot beat a lower level than required if it is applied to itself. .. [#IdrisType] https://github.com/david-christiansen/idris-type-providers