Am 03.03.21 um 16:17 schrieb Olaf Klinke:

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.

Hm, interesting point. If we do embrace that viewpoint, then I'd say we should go all the way and interpret indices modulo (non-negative) structure size! This makes (safe) indexing total (for non-empty structures) and allows things like xs !! (-1) == last xs as in Perl and some other languages. Unsafe indexing (as in the vector package) could remain as is for performance critical code. Cheers Ben

On Wed, 3 Mar 2021, Olaf Klinke wrote:

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)?

Once I defined a wrapper for numbers that (morally) restricts the value range to non-negative values: http://hackage.haskell.org/package/non-negative However, it turned out to be impractical. It is incompatible with its base number type. If you have even more variants for positive numbers, for numbers in the range [0,1] you will do more conversions than computations. I found the LiquidHaskell approach convincing: You have a base type and add constraints on the value range. You could assign a [0,1]-value to a non-negative value without conversion, because LiquidHaskell would ask Z3 and Z3 would confirm that a [0,1]-value is always non-negative.