@@ -246,10 +246,46 @@ So, for example, the following definitions are legal:
246246Dependent Types
247247===============
248248
249+First Class Types
250+-----------------
251+
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
255+computes a type:
256+
257+.. code-block:: idris
258+
259+ isSingleton : Bool -> Type
260+ isSingleton True = Nat
261+ isSingleton False = List Nat
262+
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:
267+
268+.. code-block:: idris
269+
270+ mkSingle : (x : Bool) -> isSingleton x
271+ mkSingle False = 0
272+ mkSingle True = []
273+
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:
277+
278+.. code-block:: idris
279+
280+ sum : (single : Bool) -> isSingleton single -> Nat
281+ sum False x = x
282+ sum True [] = 0
283+ sum True (x :: xs) = x + sum True xs
284+
249285Vectors
250286-------
251287
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
253289length”, conventionally called vectors in the dependent type
254290literature. They are available as part of the Idris library, by
255291importing ``Data.Vect``, or we can declare them as follows: