A simple demo of lazy nats in haskell, defined as list of unit

LazyNats.hs

import Data.List (genericLength)
import qualified Data.List.NonEmpty as NE

type Nat = [()]

instance Enum Nat where
  succ = (():)
  pred = tail
  fromEnum = length
  toEnum = flip replicate ()
  enumFrom = iterate succ -- Not necessery, but slightly more efficient

instance Num Nat where
  (+) = (++)
  (*) = (>>)
  fromInteger = toEnum . fromInteger

sumLazy :: (Foldable t, Num b) => t b -> b
sumLazy = foldr (+) 0

-- Not really lazy enough to be useful in this case
productLazy :: (Foldable t, Num b) => t b -> b
productLazy = foldr (*) 1

-- >>> (4 :: Nat) < genericLength [1..]
-- True

-- >>> (6 :: Nat) <= sumLazy [2..]
-- True

-- We can't determine if a product is non-zero without seeing the whole list
-- >>> (3 :: Nat) <= productLazy ([2,3,4] ++ repeat (error "not sufficiently lazy"))
-- *** Exception: not sufficiently lazy

-- We can however multiply infinite numbers
-- >>> (8 :: Nat) <= sumLazy [1..] * genericLength [2..]
-- True

-- If the second number is infinite, we'll only check that the first number is non-zero
-- >>> (10 :: Nat) <= sumLazy [1, undefined] * sumLazy [2..]
-- True

-- * Using non-empty lists to get non-zero natural numbers


type PositiveInteger = NE.NonEmpty ()

instance Enum PositiveInteger where
  toEnum = NE.fromList . toEnum
  fromEnum = length

instance Num PositiveInteger where
  (+) = (<>)
  (*) = flip (>>) -- Flip is necessary to get laziness
  fromInteger = toEnum . fromInteger

-- If we guarantee that the number is non-zero, we can get laziness with products as well
-- >>> (3 :: PositiveInteger) <= productLazy ([2,3,4] ++ (error "not sufficiently lazy"))
-- True

-- >>> (3 :: PositiveInteger) <= productLazy ([2..])
-- True