git.iko.soy/Idris-dev
on e32e899 help sign in
Idris-dev/docs/tutorial/introduction.rst
69 lines 2.9 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<http://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 (e.g. the length of a list) the type of a function can
29begin to describe its own properties. For example, concatenating two
30lists has the property that the resulting list’s length is the sum of
31the lengths of the two input lists. We can therefore give the
32following type to the ``app`` function, which concatenates vectors:
34.. code-block:: idris
36 app : Vect n a -> Vect m a -> Vect (n + m) a
38This tutorial introduces Idris, a general purpose functional
39programming language with dependent types. The goal of the Idris
40project is to build a dependently typed language suitable for
41verifiable *systems* programming. To this end, Idris is a compiled
42language which aims to generate efficient executable code. It also has
43a lightweight foreign function interface which allows easy interaction
44with external ``C`` libraries.
46Intended Audience
47=================
49This tutorial is intended as a brief introduction to the language, and
50is aimed at readers already familiar with a functional language such
51as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.
52In particular, a certain amount of familiarity with Haskell syntax is
53assumed, although most concepts will at least be explained
54briefly. The reader is also assumed to have some interest in using
55dependent types for writing and verifying systems software.
57Example Code
58============
60This tutorial includes some example code, which has been tested with
61Idris version . The files are available in the Idris
62distribution, and provided along side the tutorial source, so that you
63can try them out easily, under ``tutorial/examples``. However, it is
64strongly recommended that you can type them in yourself, rather than
65simply loading and reading them.
67.. [1]
68 Typically, and perhaps confusingly, referred to in the dependently
69 typed programming literature as “vectors”