@@ -246,10 +246,46 @@ So, for example, the following definitions are legal:
246Dependent Types
246Dependent Types
247===============
247===============
252+In Idris, types are a first class language construct, meaning that they
253+can be computed and manipulated (and passed to functions) just like any
254+other language construct. For example, we could write a function which
257+.. code-block:: idris
259+ isSingleton : Bool -> Type
260+ isSingleton True = Nat
261+ isSingleton False = List Nat
263+This function calculates the appropriate type from a ``Bool`` which flags
264+whether the type should be a singleton or not. We can use this function
265+to calculate a type anywhere that a type can be used. For example, it
266+can be used to calculate a return type:
268+.. code-block:: idris
270+ mkSingle : (x : Bool) -> isSingleton x
274+Or it can be used to have varying input types. The following function
275+calculates either the sum of a list of ``Nat``, or returns the given
276+``Nat``, depending on whether the singleton flag is true:
278+.. code-block:: idris
280+ sum : (single : Bool) -> isSingleton single -> Nat
283+ sum True (x :: xs) = x + sum True xs
252−A standard example of a dependent type is the type of “lists with
288+A standard example of a dependent data type is the type of “lists with
253length”, conventionally called vectors in the dependent type
289length”, conventionally called vectors in the dependent type
254literature. They are available as part of the Idris library, by
290literature. They are available as part of the Idris library, by
255importing ``Data.Vect``, or we can declare them as follows:
291importing ``Data.Vect``, or we can declare them as follows: