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
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!
+1 from me too. The partiality of a function seems to me like something that should be documented.
Best,
Daniel
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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
Libraries@haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
--------------------------------------------------------------------
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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/--------------------------------------------------------------------