git.iko.soy/Idris-dev
on master help sign in
Idris-dev/docs/tutorial/introduction.rst
74 lines 3.2 kB history raw
1.. _sect-intro:
3************
4Introduction
5************
7In conventional programming languages, there is a clear distinction
8between *types* and *values*. For example, in `Haskell
9<https://www.haskell.org>`_, the following are types, representing
10integers, characters, lists of characters, and lists of any value
11respectively:
13- ``Int``, ``Char``, ``[Char]``, ``[a]``
15Correspondingly, the following values are examples of inhabitants of
16those types:
18- ``42``, ``’a’``, ``"Hello world!"``, ``[2,3,4,5,6]``
20In a language with *dependent types*, however, the distinction is less
21clear. Dependent types allow types to “depend” on values — in other
22words, types are a *first class* language construct and can be
23manipulated like any other value. The standard example is the type of
24lists of a given length [1]_, ``Vect n a``, where ``a`` is the element
25type and ``n`` is the length of the list and can be an arbitrary term.
27When types can contain values, and where those values describe
28properties, for example the length of a list, the type of a function
29can begin to describe its own properties. Take for example the
30concatenation of two lists. This operation has the property that the
31resulting list's length is the sum of the lengths of the two input
32lists. We can therefore give the following type to the ``app``
33function, which concatenates vectors:
35.. code-block:: idris
37 app : Vect n a -> Vect m a -> Vect (n + m) a
39This tutorial introduces Idris, a general purpose functional
40programming language with dependent types. The goal of the Idris
41project is to build a dependently typed language suitable for
42verifiable general purpose programming. To this end, Idris is a compiled
43language which aims to generate efficient executable code. It also has
44a lightweight foreign function interface which allows easy interaction
45with external ``C`` libraries.
47Intended Audience
48=================
50This tutorial is intended as a brief introduction to the language, and
51is aimed at readers already familiar with a functional language such
52as `Haskell <https://www.haskell.org>`_ or `OCaml <https://ocaml.org>`_.
53In particular, a certain amount of familiarity with Haskell syntax is
54assumed, although most concepts will at least be explained
55briefly. The reader is also assumed to have some interest in using
56dependent types for writing and verifying systems software.
58For a more in-depth introduction to Idris, which proceeds at a much slower
59pace, covering interactive program development, with many more examples, see
60`Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
61by Edwin Brady, available from `Manning <https://www.manning.com>`_.
63Example Code
64============
66This tutorial includes some example code, which has been tested with
67against Idris. These files are available with the Idris distribution,
68so that you can try them out easily. They can be found under
69``samples``. It is, however, strongly recommended that you type
70them in yourself, rather than simply loading and reading them.
72.. [1]
73 Typically, and perhaps confusingly, referred to in the dependently
74 typed programming literature as “vectors”