I think it actually can be made precise, with some more knowledge than I
have. Roughly speaking, a function is total if its result is fully defined
(contains no bottoms) whenever its argument is fully defined.
On Fri, Aug 31, 2018, 7:04 AM Wolfgang Jeltsch
Am Freitag, den 31.08.2018, 08:21 +0200 schrieb Frerich Raabe:
This caught me by surprise - I would have never considered 'length' to be a partial function! Maybe I don't quite understand what it means for some expression to be 'bottom' (I thought that's the same as 'undefined').
My naive understanding was that a partial function is one which has no definition for certain arguments; in particular, it has no definition which could be used while doing equational reasoning by hand, on a piece of paper (i.e. without running the program).
It appears that this is not quite correct -- instead, any function which fails to return anything (at runtime!) for certain arguments is partial? E.g. 'sort' would be partial or even 'elem' (consider 'True `elem` repeat False')?
The word “partial” might not have a precise definition in the context of Haskell. In particular, it might not necessarily be defined in terms of ⊥ (bottom). However, the notion of ⊥ itself does have a precise definition.
⊥ is a special value that every type contains. A consequence of this is that there are also values like ⊥ : ⊥.
A good way to think about ⊥ is that ⊥ marks the absence of any information. So the value of an expression is ⊥ if there is a lack of an appropriate alternative in a case distinction but also if there is a recursion that doesn’t produce any data.
For example, if zeros is defined via the equation zeroes = 0 : zeroes, you know that zeroes must be of the form 0 : _; so it cannot be ⊥. However, if unknown is defined via the equation unknown = unknown, there is nothing you can learn about any information that unknown would contain; so unknown is ⊥.
Mathematically, the values of each type form a domain such that ⊥ is the minimum and each data constructor is an order-preserving function. When defining a value recursively, Haskell will give you the *least* solution of the defining equation. The equation zeros = 0 : zeros has only one solution (0 : 0 : 0 : …). The equation unknown = unknown, on the other hand, has every value as a solution, and thus the least of them, ⊥, is picked as the value for unknown.
All the best, Wolfgang _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries