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

[Henning Thielemann]

On Mon, 1 Mar 2021, Johannes Waldmann wrote:

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

A poor man's definition of peano numbers is:
   type Peano = [()]

'length xs' becomes:
   map (const ()) xs
or
   () <$ xs
or
   void xs

(+) becomes (++)
(*) becomes liftA2 const
(-) becomes \xs ys -> foldl (flip drop) ys (1<$xs)

My experience with Word is that it makes things even worse. It is neither 
compatible with Int nor has it bound checks. It happens pretty easily that 
in an intermediate result is negative although the whole expression of 
type Word is always non-negative.

I would prefer to use Liquid Haskell and restrict Int to non-negative 
numbers. This would solve both problems.