Idris2中类型函数isSingleton运行次数与擦除机制的技术问询

核心问题 #

1. 有观点认为依赖类型语言的类型检查速度较慢，因此推测其类型函数的运行速度也较慢。以Idris2官方文档的经典示例为例：

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

执行mkSingle True时，类型函数isSingleton会运行多少次？传统语言可通过控制台打印验证，但Idris在类型检查阶段无法执行IO操作，有没有简便方法证明isSingleton的调用次数？

2. 更新内容后的疑问：
   给isSingleton设置multiplicity为0，并新增以下代码：

f : (x : Bool) -> isSingleton x -> Nat
f True n = 0
f False ls = 1

执行Main> f True []时出现错误：

Error: When unifying:
    List ?a
and:
    isSingleton True
Mismatch between: List ?a and Nat.

(Interactive):1:8--1:10
 1 | f True []
            ^^

既然isSingleton在运行时会被擦除，Idris是如何知道第二个参数应为Nat，进而报错的？

解答 #

1. isSingleton的调用次数 #

• 类型函数isSingleton仅在类型检查阶段运行，运行时完全不会执行。执行mkSingle True的过程分为两个阶段：
  • 类型检查阶段：为了验证mkSingle True的返回值0符合isSingleton True的类型，Idris会调用一次isSingleton True，得到结果Nat，随后确认0属于Nat类型，验证通过。
  • 运行时：mkSingle True直接返回0，不会涉及isSingleton的任何调用——因为类型信息已经在编译阶段完成验证，运行时无需再计算类型函数。
• 验证方法：
  • 编译后查看二进制：使用idris2 --compile -o main yourfile.idr编译代码，再用反汇编工具（如objdump）查看生成的可执行文件，会发现isSingleton没有生成任何运行时代码。
  • 查看核心表达式：在Idris REPL中执行:core mkSingle，可以看到isSingleton仅出现在类型标注中，运行时逻辑里没有它的调用痕迹。

2. 运行时擦除与类型检查的关系 #

• multiplicity 0的作用是标记该函数仅用于类型检查，不会生成运行时代码，但这并不影响类型检查阶段的执行。
• 调用f True []时，Idris在类型检查阶段就会执行isSingleton True得到Nat，然后检查第二个参数[]的类型是List ?a，与Nat不匹配，因此直接报错——这个过程完全发生在编译/REPL检查阶段，和运行时擦除没有关联。
• 本质逻辑：类型检查是前置验证步骤，只有通过类型检查的代码才会进入编译生成运行时代码；运行时擦除的是已经完成验证的类型相关代码，不会影响类型检查阶段的逻辑执行。

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