This is a summary about Peano number implementations on HackageDB regarding the behaviour of `genericLength`

on incomplete and infinite lists.

We pick `genericLength`

from `Data.List`

and rename it to `length`

:

`import Data.List hiding (length)`

import Prelude hiding (length)

`length :: [a] -> Nat`

length = genericLength

The following definition of `Nat`

were used one after the other (the declarations were put before the definition of `length`

):

`Number.Peano`

from numeric-prelude-0.0.5

`import qualified Number.Peano`

type Nat = Number.Peano.T

`Numeric.NonNegative.Chunky`

from non-negative-0.0.3

`import qualified Numeric.NonNegative.Chunky as C`

import qualified Numeric.NonNegative.Wrapper as W

type Nat = C.T (W.T Int)

`Data.Number.Natural`

from numbers-2008-4-20

`import qualified Data.Number.Natural`

type Nat = Data.Number.Natural.Natural

`Data.Number.Nat`

from nat-0.2^{1}

`import qualified Data.Number.Nat`

type Nat = Data.Number.Nat.Nat

`Number.Peano.Inf`

from peano-inf-0.1

`import qualfified Number.Peano.Inf`

type Nat = Number.Peano.Inf.Nat

These test cases were completed by all implementations excluding `Data.Number.Nat`

:

`length [1..] > 100`

`length [1..] > length [1..100]`

`length (1:undefined) >= 0 -- it is OK with Data.Number.Nat`

length (1:2:undefined) >= 1

length (1:2:3:undefined) >= 2

length (1:2:3:4:undefined) >= 3

`6 + length undefined >= 5`

`length [1..] `min` length [1..100] == 100`

`length (1:2:undefined) `min` length [1] /= 5`

`length [1..] `max` length [1..100] > 1000`

`min`

and `max`

`Data.Number.Natural`

fails on these test cases:

`1 `min` length (1:undefined) == 1`

2 `min` length (1:2:undefined) == 2

3 `min` length (1:2:3:undefined) == 3

`Numeric.NonNegative.Chunky`

, `Data.Number.Natural`

and `Data.Number.Nat`

fail on these test cases:

`0 `min` length undefined == 0 -- it is OK with Data.Number.Nat`

`10 `max` length (1:undefined) > 0`

`length (1:2:undefined) `min` length [1..100] > 1`

`minimum [length [1..], length (1:2:undefined), length [], length undefined] == 0`

`(<)`

, `(>)`

, `(>=)`

and `(<=)`

with `compare`

`Numeric.Peano`

, `Numeric.NonNegative.Chunky`

, `Data.Number.Natural`

and `Data.Number.Nat`

fail on these test cases:

`length undefined >= 0 -- it is OK with Data.Number.Nat`

length (1:undefined) >= 1

length (1:2:undefined) >= 2

length (1:2:3:undefined) >= 3

length (1:2:3:4:undefined) >= 4

`5 + length undefined >= 5`

All implementations fail on these test cases:

`length (1:undefined) `compare` 1 /= LT ==> bottom`

`length undefined `min` 0 == 0 ==> bottom`

`take`

, `drop`

, `replicate`

The following tests were completed by all implementations (excluding `Numeric.NonNegative.Chunky`

which has no `Integral`

instance and could not take part in these test cases):

`head (genericTake (length (1:undefined)) [1..]) == 1`

`head (genericTake (length (1:2:undefined)) [1..]) == 1`

`head (genericReplicate (length (1:undefined)) 1) == 1`

`null $ genericDrop (length [1..]) [1..10]`

According to this test, the Peano numbers implemented in peano-inf are the laziest, followed by Peano numbers implemented in numeric-prelude, non-negative, numbers and nat.

*Created by Péter Diviánszky, 2008-11-11*

This number representation has completed only 6 test cases, maybe because it is a binary representation (so it is not a Peano number). ↩