Testing Number Theoretic Functions in Haskell using a recursor over natural numbers

Question

I'm implementing some number theoretic functions as the exponentiation in Haskell using a recursor. I'm using the QuickCheck library for testing my implementation. For simplify my tests, I'm using the Natural data type from the base library, the Arbitrary instance for Natural defined in the quickcheck-instances library and the following functions converting from Nat to Natural and from Natural to Nat, respectively, considering the data Nat defined by myself:

data Nat = Zero | Succ Nat

natToNatural :: Nat -> Natural
natToNatural Zero = 0
natToNatural (Succ n) = 1 + natToNatural n

naturalToNat :: Natural -> Nat
naturalToNat 0 = Zero
naturalToNat n = Succ (naturalToNat (n - 1))

The implemetation use the following recursor over natural numbers:

recNat :: a -> (Nat -> a -> a) -> Nat -> a
recNat a _ Zero     = a
recNat a h (Succ n) = h n (recNat a h n)

My function of exponentiation is

expR :: Nat -> Nat -> Nat
expR m n = recNat (Succ Zero) (\ _ y -> multR m y) n

I define the prop_Exp property using the exponentiation on Natural

prop_Exp :: Natural -> Natural -> Bool
prop_Exp m n = natToNatural (expR m' n') == m ^ n
  where
    m' :: Nat
    m' = naturalToNat m

    n' :: Nat
    n' = naturalToNat n

for testing my implementation of the expR function via QuickCheck

main :: IO ()
main = quickCheck prop_expR

However, after running this code I get an exception:

*** Exception: stack overflow

I want to know what it is wrong with this code

I guess that such test could generate random numbers which are too large for exponentiation. Keep in mind that your Nat type represents numbers in unary, so it will require a lot of memory even for, say, 10^10. I fear that random Natural numbers can be much larger than 10. I can't remember how to tell quickcheck to limit the range. — chi

Mark Seemann Mark Seemann · Accepted Answer · 2020-06-01T08:07:20

As chi remarks, the Nat type represents numbers as recursive data structure. I think that it's isomorphic to [()], but I could be mistaken...

AFAICT, the conversion functions, as well as recNat, aren't tail recursive, so when working with something like 10^10, they'd be building up thunks for billions of elements. It's not too surprising that you get a stack overflow from larger numbers.

You can tell QuickCheck to limit the range of the values generated. The choose function is the general-purpose solution to this problem, but AFAICT Natural doesn't have a Random instance. Instead, you might be able to use chooseEnum, since Natural does have an Enum instance.

A few years back I was also dabbling with natural numbers (and associated ideas) in a like fashion. Here's a property I wrote of multiplication:

testProperty "Multiplication" $ do
  x <- choose @Integer (0, 25)
  y <- choose (0, 25)
  return $ x * y === toNum (multiplyF (fromNum x) (fromNum y))

I didn't base my QuickCheck properties on Natural since I used choose. This enabled me to tell QuickCheck to only pick numbers greater than 0. For multiplication, I had to constrain my integers to be less than 25, but for other properties, I chose a larger range:

testProperty "Increment" $ do
  i <- choose @Integer (0, 1e4)
  return $ i + 1 === toNum (incF (fromNum i))

It's been a few years, so I don't recall exactly why I chose those particular numbers. I was using an older laptop back then, but I don't recall if higher numbers caused my process to overflow, or if it was simply that the tests ran too slowly.

Testing Number Theoretic Functions in Haskell using a recursor over natural numbers

1 Answers