Idris中使用clockTime做基准测试始终返回0纳秒是何原因

你的代码有两个核心错误，直接导致耗时统计结果为0：

• 未强制求值纯计算逻辑：Idris采用按需调用的非严格求值策略，let r = factorial a并不会立刻执行阶乘计算，只会生成一个待求值的表达式占位（thunk）。真正的计算会推迟到后续putStrLn里show r需要用到结果时才执行，而此时你已经完成了t2的时间采样，两次clockTime调用之间几乎没有运行任何计算逻辑，自然得到0纳秒的结果。
• 时间差值计算逻辑错误：clockTime返回的时间戳包含seconds（从纪元开始的整秒数）和nanoseconds（当前整秒内的纳秒偏移）两个字段，你仅计算了nanoseconds字段的差值，没有累加整秒部分的时间差，一旦函数运行时间超过1秒，得到的结果会完全错误（甚至出现负数）。

首先需要导入Control.DeepSeq模块提供的deepseq函数，在获取t2之前强制r被完全求值，同时修正时间差的计算逻辑。修正后的核心代码如下：

module Main

import Data.String
import System
import Control.DeepSeq -- 新增导入，用于强制求值

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
                    r `deepseq` pure () -- 强制r完全求值后再执行后续逻辑
                    t2 <- clockTime

                    -- 正确计算总纳秒耗时
                    let elapsed = (seconds t2 - seconds t1) * 1000000000 + (nanoseconds t2 - nanoseconds t1)

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

                Nothing => putStrLn "Not a valid number"

编译时可以加上优化参数获得更贴近真实生产运行的性能结果，例如：
idris main.idr -O2 -o main

clockTime可以用于简单的粗略耗时统计，但并不适合精确的性能基准测试，原因如下：

• 它返回的是墙钟时间（系统真实流逝的时间），会受进程调度切换、系统其他进程资源占用、IO等待等无关因素影响，统计值波动大。
• 它的精度受操作系统时钟分辨率限制，无法捕捉纳秒级的极短耗时。

如果需要做严谨的性能测试，建议遵循以下规则：

• 多次重复运行待测逻辑，剔除异常值后取平均值、中位数作为统计结果
• 正式统计前先做几轮预热运行，消除缓存冷启动、运行时初始化带来的误差
• 优先读取进程的CPU执行时间而非墙钟时间，排除调度干扰
• 确保待测逻辑不会被编译优化判定为无用代码直接消除

内容的提问来源于stack exchange，提问作者Foxy