Let me throw in one key bikeshed to be painted. I don't like the fact that subtraction on naturals is a partial operation as proposed. I would much prefer saturated subtraction where for y > x, x - y = 0. This prior discussion on -cafe tends towards such a definition as being 'universally better' https://www.haskell.org/pipermail/haskell-cafe/2011-March/090265.html Here is my motivation for saturated subtraction: On all non-bottom calculations, it agrees. On calculations that are bottom under partial subtraction, it nonetheless gives a mathematically meaningful and useful result in a coherent way. As a general principle, I think our goal should be to make base more total, not less. The arguments cited in the thread from Runciman's "What About the Natural Numbers" (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.3442) are also fairly compelling in this regard. -g
Herbert Valerio Riedel wrote:
I hereby suggest to add a type for encoding term-level naturals... to `base:Data.Word` module
+1
because Edward, who is the current leading purveyor of term-level nats, is in favor.
Roman Cheplyaka wrote:
Yeah, having Natural in Data.Word feels unnatural to me.
Agreed. I'm not sure what the solution is though. I'd be in favor if someone comes up with something decent. *However* I'd be strongly opposed to letting any kind of bikeshedding getting in the way of Herbert's proposal.
Thanks, Yitz