Lazy List Lengths

This is a summary about Peano number implementations on HackageDB regarding the behaviour of genericLength on incomplete and infinite lists.

Preparation

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¹

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

Test Cases

"Easy" cases

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

Failures caused by not appropriate 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

Failures caused by implementing (<), (>), (>=) 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

Reasonable failures

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]

Evaluation

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