Non-totality and turing-completeness

[tonymorris]

Conor McBride rightly points out the inaccuracy of the statement that turing-completeness implies non-totality.

https://twitter.com/pigworker/status/405475048217010176

For example, Agda denotes non-totality as an effect using what is essentially type Partiality = Free (->).

Loose or inaccurate statements alone may be beneficial, however, this particular statement has very little pedagogical value, while continuing the propagation of a common misunderstanding regarding total functional programming.

Although in the verbal presentation this point was loosely covered, this statement requires revision such that it is accurate and encourages further thought about denoting partiality. This can almost certainly be done with no loss of explanatory simplicity and value.