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

Johannes Waldmann johannes.waldmann at htwk-leipzig.de
Mon Mar 1 16:45:07 UTC 2021


Dear Cafe -


let's fight Int.


In a lot of code I write (for research, teaching, production),
a lot of numbers are in fact natural numbers -
because I am counting (e.g., number of elements in a collection)
or pointing into what I just counted (e.g., Data.Set.elemAt).

But Haskell's "most natural" type is - Int.
At least that's my impression from current usage in libraries
and teaching examples (see functions length, replicate, ... ).

I've developed a horror
of reading and writing "length something :: Int".

As I will be teaching an introductory class on FP soon,
I am looking for ways to handle this.


One option is presented in Bird/Gibbons: Algorithm Design with Haskell,
which has "type Nat = Int" on page 6. Actually, that's the very first
code example that appears in the book! The footnote there
refers to a remark in Data.Word that has since been dropped?


Now there is Numeric.Natural, (cf.
https://mail.haskell.org/pipermail/libraries/2014-November/024203.html )
and numeric literals
are already overloaded, so we can just use that?
Well, yes and no - we still have to write a type conversion
each time we use some library function that insists on Int,
or, write cumbersome "genericLength".


Also (but that is the lesser concern), Numeric.Natural
is for arbitrary-length numbers (corresponding to Integer),
while I might sometimes know that numbers are representable
in a machine word, and I don't want to pay for the implied pattern match
(data Natural = NatS Word | NatJ BigNat).
I am willing to pay for underflow checks (on subtraction),
and for overflow  checks (if there's an upper bound).
If I want to live risky (no checks) I could use Data.Word.


So, what do you do?   (Yes, Peano numerals ...)
Or, how do we convince ourselves (and our students)
of keeping the current status?


NB: here is another practical argument for Natural
(from production code, an auto-grading system for student homework)
We use datatype-generic parsers heavily.
For  data Foo = Foo { ... :: Nat ... },
bad input will be rejected by the parser already,
and I need no extra checks later on. Less code!
I sometimes even use "Pos(itive)".
That's all fine and dandy - until I call some library function...


- J.W.


More information about the Haskell-Cafe mailing list