一个类型函数运行多少次，你能证明吗？

Question

人们说依赖类型语言在类型检查方面很慢，所以我认为它在运行类型函数方面很慢。

使用https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html 上的经典示例

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

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

并运行

mkSingle True

isSingleton 运行了多少次？

使用传统语言，我可以打印到控制台。 But Idris doesn't appear to execute the IO machinery when type checking。我可以增加一个全局计数器或在isSingleton 的开头设置一个断点，并计算断点被击中的次数。

我可以在 idris 2 中做一些事情来轻松地说服人们，“嘿，在此期间 isSingleton 已被称为 x 次”？

更新

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

我将isSingleton的多重性设置为0，将上面的代码添加到我的文件中并运行

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 []
            ^^

idris 知道第二个参数应该是 Nat，它由 isSingleton 提供，对吧？但是isSingleton是在运行时被擦除的，isSingleton是怎么调用的呢？

Answer 1

抹去isSingleton

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

那么你知道它在运行时不存在并且永远不会被调用。我想如果你不擦除它，它也永远不会被调用（在这个例子中），但通过擦除它你可以确定。