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.