.. _sect-intro: ************Introduction************ In conventional programming languages, there is a clear distinctionbetween *types* and *values*. For example, in `Haskell<http://www.haskell.org>`_, the following are types, representingintegers, characters, lists of characters, and lists of any valuerespectively: -  ``Int``, ``Char``, ``[Char]``, ``[a]`` Correspondingly, the following values are examples of inhabitants ofthose types: -  ``42``, ``’a’``, ``"Hello world!"``, ``[2,3,4,5,6]`` In a language with *dependent types*, however, the distinction is lessclear. Dependent types allow types to “depend” on values — in otherwords, types are a *first class* language construct and can bemanipulated like any other value. The standard example is the type oflists of a given length [#fn1]_, ``Vect n a``, where ``a`` is the elementtype and ``n`` is the length of the list and can be an arbitrary term. When types can contain values, and where those values describeproperties, for example the length of a list, the type of a functioncan begin to describe its own properties. Take for example theconcatenation of two lists. This operation has the property that theresulting list's length is the sum of the lengths of the two inputlists. We can therefore give the following type to the ``app``function, which concatenates vectors: .. code-block:: idris     app : Vect n a -> Vect m a -> Vect (n + m) a This tutorial introduces Idris, a general purpose functionalprogramming language with dependent types. The goal of the Idrisproject is to build a dependently typed language suitable forverifiable general purpose programming. To this end, Idris is a compiledlanguage which aims to generate efficient executable code. It also hasa lightweight foreign function interface which allows easy interactionwith external libraries. Intended Audience================= This tutorial is intended as a brief introduction to the language, andis aimed at readers already familiar with a functional language suchas `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.In particular, a certain amount of familiarity with Haskell syntax isassumed, although most concepts will at least be explainedbriefly. The reader is also assumed to have some interest in usingdependent types for writing and verifying software. For a more in-depth introduction to Idris, which proceeds at a much slowerpace, covering interactive program development, with many more examples, see`Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_by Edwin Brady, available from `Manning <https://www.manning.com>`_. Example Code============ This tutorial includes some example code, which has been testedagainst 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 typethem in yourself, rather than simply loading and reading them. .. rubric:: Footnotes .. [#fn1] Typically, and perhaps confusingly, referred to in the dependently   typed programming literature as "vectors".