[Haskell-cafe] naturally, length :: a -> Int

[Ben Franksen]

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