为什么在 Idris 中，`clockTime` 似乎不适用于基准测试？

可能有库可以做到这一点（尽管我还没有找到），我实际上正在寻找测量函数在 Idris 中运行所需的时间。我发现的方法是在函数运行之前和之后使用clockTime和System区分。这是一个示例代码：

module Main

import Data.String
import System

factorial : Integer -> Integer
factorial 0 = 1
factorial 1 = 1
factorial n = n * factorial (n - 1)

main : IO ()
main = do
    args <- getArgs

    case args of
        [self ] => putStrLn "Please enter a value"
        [_, ar] => do
            case parseInteger ar of
                Just a => do

                    t1 <- clockTime
                    let r = factorial a
                    t2 <- clockTime

                    let elapsed = (nanoseconds t2) - (nanoseconds t1)

                    putStrLn $ "fact(" ++ show a ++ ") = "
                                       ++ show r ++ " in "
                                       ++ (show elapsed) ++ " ns"

                Nothing => putStrLn "Not a valid number"

为了避免 Idris 通过评估阶乘来优化程序，我只是要求使用参数调用程序。

但是这段代码不起作用：无论我输入什么数字，例如10000，Idris 总是返回 0 纳秒，这让我很怀疑，即使只是分配一个 bigint 也需要时间。我用idris main.idr -o main.

我在我的代码中做错了什么？clockTime基准测试不是一个好的计划吗？