Am 02.03.21 um 17:48 schrieb Jaro Reinders:
There was a great talk about this at PWLConf 2019 by José Manuel Calderón Trilla: "What about the Natural Numbers?" There is a recording on YouTube: https://www.youtube.com/watch?v=jFk1qpr1ytk
Thanks for the link. I read Colin's paper long ago and forgot most about it. IMO the correspondence with take and drop for lists isn't too convincing. Lists are boring, and for data structures with more interesting invariants (like Sets) size/length is no longer a monoid homomorphism. The talk is also missing out on the opportunity to hold an extended discussion about arithmetic laws like cancellation. For instance, we have (a - b) + b == a for unsigned (Data.Word, assuming operations modulo 2^bitsize), but (a .-. b) + b == a does not hold in general. Due to primary school "indoctrination" we all intuitively expect such laws to hold for the standard arithmetic operators, which is why I think they should be either modulo 2^wordsize as in C or raise an exception. And I would really like to be able to chose which of those I get. None of this preclude the addition of non-standard arithmetic operators, of course. These may be useful in certain simple situations like when dealing with lists. Cheers Ben