git.iko.soy/Idris-dev
on f572cd0 help sign in
Idris-dev/docs/tutorial/introduction.rst
66 lines 2.9 kB history raw
1===========
2Introducton
3===========
5In conventional programming languages, there is a clear distinction
6between *types* and *values*. For example, in `Haskell <http://www.haskell.org>`_, the following
7are types, representing integers, characters, lists of characters, and
8lists of any value respectively:
10- ``Int``, ``Char``, ``[Char]``, ``[a]``
12Correspondingly, the following values are examples of inhabitants of
13those types:
15- ``42``, ``’a’``, ``Hello world!``, ``[2,3,4,5,6]``
17In a language with *dependent types*, however, the distinction is less
18clear. Dependent types allow types to “depend” on values — in other
19words, types are a *first class* language construct and can be
20manipulated like any other value. The standard example is the type of
21lists of a given length [1]_, ``Vect n a``, where ``a`` is the element
22type and ``n`` is the length of the list and can be an arbitrary term.
24When types can contain values, and where those values describe
25properties (e.g. the length of a list) the type of a function can begin
26to describe its own properties. For example, concatenating two lists has
27the property that the resulting list’s length is the sum of the lengths
28of the two input lists. We can therefore give the following type to the
29``app`` function, which concatenates vectors:
31.. code-block:: idris
33 app : Vect n a -> Vect m a -> Vect (n + m) a
35This tutorial introduces ``Idris``, a general purpose functional
36programming language with dependent types. The goal of the ``Idris``
37project is to build a dependently typed language suitable for verifiable
38*systems* programming. To this end, ``Idris`` is a compiled language
39which aims to generate efficient executable code. It also has a
40lightweight foreign function interface which allows easy interaction
41with external ``C`` libraries.
43Intended Audience
44-----------------
46This tutorial is intended as a brief introduction to the language, and
47is aimed at readers already familiar with a functional language such
48as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.
49In particular, a certain amount of familiarity with Haskell syntax is
50assumed, although most concepts will at least be explained
51briefly. The reader is also assumed to have some interest in using
52dependent types for writing and verifying systems software.
54Example Code
55------------
57This tutorial includes some example code, which has been tested with
58``Idris`` version . The files are available in the ``Idris``
59distribution, and provided along side the tutorial source, so that you
60can try them out easily, under ``tutorial/examples``. However, it is
61strongly recommended that you can type them in yourself, rather than
62simply loading and reading them.
64.. [1]
65 Typically, and perhaps confusingly, referred to in the dependently
66 typed programming literature as “vectors”