Here's an interesting paper recently mention in another thread: Total Functional Programming
Abstract: The driving idea of functional programming is to make programming more
closely related to mathematics. A program in a functional language such as Haskell or
Miranda consists of equations which are both computation rules and a basis for simple
algebraic reasoning about the functions and data structures they define. The existing
model of functional programming, although elegant and powerful, is compromised to
a greater extent than is commonly recognized by the presence of partial functions.
We consider a simple discipline of total functional programming designed to exclude
the possibility of non-termination. Among other things this requires a type distinction
between data, which is finite, and codata, which is potentially infinite.
I presume that the bogus definiton of "
" is a subtle reminder of the importance of eliminating bottom.