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

[Olaf Klinke]

> Date: Thu, 4 Mar 2021 11:36:14 +0100
> From: Ben Franksen <ben.franksen at online.de>
> To: haskell-cafe at haskell.org
> Subject: Re: [Haskell-cafe] naturally, length :: a -> Int
> Message-ID: <s1qd6u$l43$1 at ciao.gmane.io>
> Content-Type: text/plain; charset=utf-8
> 
> 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

I like Haskell particularly for not being like Matlab, where virtually
any well-bracketed indexing syntax does produce a result, but not
necessarily what you intended or expected. Besides, for some structures
length is expensive but index is not so much, so I wonder whether one
can modulo-index into a lazy container without evaluating its entire
spine. 
I just wanted to understand/justify why Int is so convenient, and the
Time-DiffTime analogy sprang to mind. 
Following the free group route, one immediately sees that there is an
embedding from cardinalities to offsets, but no inverse. We could, of
course, bring other categories into the picture such as ordered sets.
Then there is an embedding-projection pair between Int and Natural,
where all Ints < 0 are mapped to 0. The base functions such as take and
drop adhere to this interpretation. 

Olaf