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

[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

I think we should not be so quick to give up theoretical elegance and 
simplicity for the sake of performance (especially not in a language like 
Haskell). If we would make a change then I would prefer using the lazy and 
possibly infinite natural numbers with pattern synonyms for successor and zero. 
Like the existing Integer but then lazy, so more programs will terminate, for 
example a program that checks if the length of a finite list is smaller than 
the length of an infinite list.

And if we make the change we will probably also need something like 
Linear.Affine from the linear package with an instance for these natural 
numbers where the difference between two naturals is an Integer. That would 
hopefully make it reasonably easy to convert naturals to and from integers.

I hope that some of the performance concerns can be tackled by compiler 
optimizations, for example, detecting when naturals are used in tight loops 
which can be safely replaced by machine words, similar to strictness analysis 
and unboxing. And of course programmers can choose to use the old unsafe 
machine words/ints manually.