Mark partial functions as such

[Henrik Nilsson]

Hi,

Frerich Raabe wrote:

 > On 2018-08-31 04:09, David Feuer wrote:
 > > What about functions like length? length (repeat ()) is bottom.
 > > repeat () is not bottom. Ergo, length is partial.
 >
 > 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').

We have to be a bit careful with attributing blame for failure.
By David's argument, e.g. "fst" would also be "partial". Consider:

   (_|_, _|_) /= _|_

But

   fst (_|_, _|_) == _|_

But the bottom here does not originate in the computation of "fst" as
such, but in the computation of the *argument* to "fst".

Similarly for "length" above: "length" is not to blame for the
fact that

   length (repeat ()) == _|_

It's simply that computation of the argument to length takes a very(!)
long time.

In a language with strict semantics, this is of course no surprise
at all, and I suspect no one would suggest that a function
like "length" is partial in a strict setting just because the
overall computation fails to terminate when the computation of
an argument does.

 > 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')?

I'd say neither "sort" nor "elem" is partial for the same reason.

As to the original suggestion of marking functions as partial, I think
that's fine, as long as one is careful to explain exactly what is meant.
(And documenting (different forms of) strictness would be fine too.)

But one should bear in mind that there are functions that are
partial for other reasons that pattern matching failure, in particular
numerical functions like division, square root, ...
(And the full story of floating point arithmetic with infinities
and NaNs etc. is of course quite complicated.)

Students (well, any programmer) should of course be aware that one have
to be extra careful when using partial functions, and certainly also
encouraged to seek alternative formulations, but just saying "Don't use
partial functions" is not the full story.

Best,

/Henrik





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.