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

Olaf Klinke olf at aatal-apotheke.de
Wed Mar 3 15:17:02 UTC 2021


Which bugs can be caught at compile-time by having length return
natural numbers? Regarding space, Int instead of Word only wastes the
sign bit, doesn't it?

I like the idea that Johannes Waldmann and Jaro Reinders brought up: 
Why is length :: Foldable a => a -> Int so convenient? Short answer:
Because of "affine" things like `availableSpace - length xs'.

There are indeed two types involved here, as the foundation package
points out: relative offsets (like a tangent space?) and absolute
counts. Think of NominalDiffTime versus UTCTime, or the two
interpretations of vectors as points/movements in space. 

In this light one could regard the current length as 
"the relative offset of the end of the list" which can readily be
subtracted from another relative offset. In mathematical terms: Int the
free group over the monoid of cardinal lengths.   

While we're at it: Can there be a Fractional type permitting only
positive numbers, as the positive real numbers are closed under
division? Can there be a type of rationals between 0 and 1 (which is
closed under multiplication) where (/x) is the right adjoint to (*x)? 

Olaf



More information about the Haskell-Cafe mailing list