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