@@ -537,10 +537,11 @@ Note: Declaration Order and ``mutual`` blocks
537537~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
538538
539539In general, functions and data types must be defined before use, since
540−dependent types allow functions to appear as part of types, and their
541−reduction behaviour to affect type checking. However, this restriction
542−can be relaxed by using a ``mutual`` block, which allows data types
543−and functions to be defined simultaneously:
540+dependent types allow functions to appear as part of types, and type
541+checking can rely on how particular functions are defined (though this
542+is only true of total functions; see Section :ref:`sect-totality`)).
543+However, this restriction can be relaxed by using a ``mutual`` block,
544+which allows data types and functions to be defined simultaneously:
544545
545546.. code-block:: idris
546547
@@ -1182,3 +1183,81 @@ matching ``let`` and lambda bindings. It will *only* work if:
11821183- The type of the result is "known". i.e. the type of the expression
11831184 can be determined *without* type checking the ``case``-expression
11841185 itself.
1186+
1187+Totality
1188+========
1189+
1190+A *total* function is a function that terminates for all possible
1191+inputs, or one that is guaranteed to produce some output before making
1192+a recursive call. For example, Idris' ``head`` function is total for
1193+all lists:
1194+
1195+::
1196+
1197+ Idris> :t Prelude.List.head
1198+ head : (l : List a) -> {auto ok : NonEmpty l} -> a
1199+
1200+The ``{auto ok : NonEmpty l}`` tells us that Idris won't compile if we
1201+try to call ``head`` on an empty list. The implementation is as follows:
1202+
1203+.. code-block:: idris
1204+
1205+ ||| Get the first element of a non-empty list
1206+ ||| @ ok proof that the list is non-empty
1207+ head : (l : List a) -> {auto ok : NonEmpty l} -> a
1208+ head [] {ok=IsNonEmpty} impossible
1209+ head (x::xs) {ok=p} = x
1210+
1211+(Note that this implementation is in contrast to Haskell's ``head``,
1212+which is *not* total and will fail at runtime rather than compile time.)
1213+The following Idris code will compile:
1214+
1215+.. code-block:: idris
1216+
1217+ module Main
1218+
1219+ main : IO ()
1220+ main = do
1221+ let x = head [1, 2, 3]
1222+ print x
1223+
1224+And will print ``1``. However, the same code with ``head []`` won't compile:
1225+
1226+::
1227+
1228+ test.idr:5:6:When checking right hand side of main with expected type
1229+ IO ()
1230+
1231+ Can't infer argument letty to head,
1232+ Can't infer argument letty to [],
1233+ Can't infer argument ok to head,
1234+ Can't infer argument letty to print,
1235+ Can't infer argument constraint to print
1236+
1237+We can't bind and print ``x`` because ``head []`` doesn't type check.
1238+
1239+However, we might imagine a function, ``unsafeHead``, that is identical to
1240+Idris' ``head`` function except that it is *not* total: it will error out
1241+at runtime if called on an empty list. (This is similar to the behavior of
1242+Haskell's ``head`` function.) ``unsafeHead`` might look like this:
1243+
1244+.. code-block:: idris
1245+ -- Unsafe head example!
1246+ unsafeHead : List a -> a
1247+ unsafeHead (x::xs) = x
1248+
1249+And although it typechecks and compiles, it will not reduce (that is, evaluation
1250+of the function will cause its type to change):
1251+
1252+::
1253+
1254+ unsafe> unsafeHead [1, 2, 3]
1255+ 1 : Integer
1256+ unsafe> unsafeHead []
1257+ (input):Can't infer argument iType to unsafeHead,
1258+ Can't infer argument iType to []
1259+
1260+Functions that are not total are known as *partial functions*. As
1261+mentioned in the note about ``mutual`` blocks, non-total definitions
1262+aren't reduced when type checking because they are not well-defined
1263+for all possible inputs.