Mark partial functions as such

[David Feuer]

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 <wolfgang-it at jeltsch.info>
wrote:

> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180831/3e1e8372/attachment.html>