Mark partial functions as such

[Andrew Butterfield]

Dear David,

given that "data [a] =  [] | (a : [a])" in Haskell is viewed co-inductively and hence admits infinite lists,
then any function f : [a] -> b  is total only if it returns a result.
Does this mean it must terminate?

In a strict world, yes.

In the lazy world, it's a little more complicated than that.

Consider  map id :: [a] -> [a]

is map id partial? It won't terminate if given an infinite list, but it will produce partial results on demand indefinitely - so I say it is total.

However , length applied to [0..] (say) will never return any partial or complete result, and so I would say it's partial.

I too am going to start teaching Haskell newbies, so this is of interest - to what extend to we use "stories for children"

One suggestion: if you don't start with laziness, and they  initially consider lists as finite, then length :: [a] -> Int  is total, where [a] is interpreted as finite lists.
When laziness enters the picture, then points out that having [a] include infinite lists means that some hitherto total function become partial, on that expanded domain.

Perhaps the added documentation should also comment for list and ADT based functions where the infinite forms influence totality/partiality?

Regards, Andrew

> On 31 Aug 2018, at 03:09, David Feuer <david.feuer at gmail.com> wrote:
> 
> Yes, I think so. What about functions like length? length (repeat ()) is bottom. repeat () is not bottom. Ergo, length is partial. But I don't think we want to say that!
> 
> On Thu, Aug 30, 2018, 10:05 PM Daniel Díaz Casanueva <dhelta.diaz at gmail.com <mailto:dhelta.diaz at gmail.com>> wrote:
> +1 from me too. The partiality of a function seems to me like something that should be documented.
> 
> Best,
> Daniel
> 
> Am Fr., 31. Aug. 2018 um 02:10 Uhr schrieb Richard Eisenberg <rae at cs.brynmawr.edu <mailto:rae at cs.brynmawr.edu>>:
> Proposal: Mark partial functions in `base` as partial
> 
> Motivation: I'm about to teach Haskell to a classful of beginners. In my experience, they will soon reach for functions like `head` and `tail`, because pattern-matching is foreign to them. I would love just to be able to say "Don't use partial functions", but many students will not easily be able to tell partial functions from total ones.
> 
> I do expect this problem to work itself out rather quickly, and then students will be able to identify partial functions, but loudly marking partial functions as partial seems like a small service to everyone and a bigger one to newbies. I don't see any downsides.
> 
> Thoughts?
> 
> Thanks,
> Richard
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org <mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org <mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero at TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180831/4fc16e16/attachment.html>