用自然数上的递归子检验Haskell中的数论函数

Question

我用递归函数在Haskell中实现一些数论函数的幂运算。我正在使用QuickCheck库来测试我的实现。为了简化我的测试，我使用了基库中的Natural数据类型，在quickcheck-instances库中定义的Natural任意实例，以及以下从Nat转换到Natural和从Natural转换到Nat的函数，考虑的是我自己定义的数据Nat：

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))

在自然数上使用以下递归：

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

我的幂函数是

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

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

main :: IO ()
main = quickCheck prop_expR

*** Exception: stack overflow

Answer 1

正如chi所说，NAT类型将数字表示为递归数据结构。我认为它与[()]同构，但我可能错了······

当然，转换函数和recnat都不是尾部递归的，所以当使用10^10这样的东西时，它们将为数十亿个元素建立thunk。从较大的数字中得到堆栈溢出并不奇怪。

您可以告诉QuickCheck限制生成的值的范围。choose函数是该问题的通用解决方案，但是AFAICTnatural没有random实例。相反，您可以使用chooseenum，因为natural确实有enum实例。

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

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