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

[Viktor Dukhovni]

On Mon, Mar 01, 2021 at 05:45:07PM +0100, Johannes Waldmann wrote:

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

If you're willing to tolerate the small overhead of Natural:

    $ ghci
    λ> import Data.Foldable (Foldable, foldl')
    λ> import GHC.Natural 
    λ> len :: Foldable t => t a -> Natural; len = foldl' (\a _ -> a + 1) 0
    λ> let x = len [1,2,3]
    λ> :t x    
    x :: Natural
    λ> x       
    3

otherwise, note that `succ`, unlike (+), does bounds checks:

    λ> let x = maxBound :: Int
    λ> succ x
    *** Exception: Prelude.Enum.succ{Int}: tried to take `succ' of maxBound

and so:

    λ> import Data.Foldable (Foldable, foldl')
    λ> len :: Foldable t => t a -> Int; len = foldl' (\a _ -> succ a) 0
    λ> let x = len [1,2,3]
    λ> :t x    
    x :: Int
    λ> x       
    3

on a 64-bit machine, testing to make sure the bounds check actually
works would take too long, but we can cheat:

    λ> len :: Foldable t => t a -> Int; len = foldl' (\a _ -> succ a) (maxBound :: Int)
    λ> len []
    9223372036854775807
    λ> len [1]
    *** Exception: Prelude.Enum.succ{Int}: tried to take `succ' of maxBound

-- 
    Viktor.