Mark partial functions as such

[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