类型构造器中的参数擦除是什么含义？

在Idris这类依赖类型语言里，(0 _ : Nat)里的0是擦除标记，核心作用是告诉编译器：这个参数仅用于编译阶段的类型检查，运行时会被完全移除，不会留下任何数据或性能开销。

两个代码定义的核心区别 #

1. 带擦除标记的定义

data Foo : (0 _ : Nat) -> Type where

• 编译阶段：这个Nat参数会正常参与类型约束，比如Foo 5和Foo 10是完全不同的类型，编译器会严格校验类型匹配。
• 运行阶段：所有Foo类型的实例不会携带这个Nat参数的具体值——编译器会彻底擦除它，不占用任何内存，也无法在运行时代码中读取这个参数。

2. 不带擦除标记的定义

data Foo : Nat -> Type where

• 编译阶段：同样参与类型检查，和擦除版的约束逻辑一致。
• 运行阶段：每个Foo实例都会附带对应的Nat参数值，这个值会占用内存，也可以在运行时的函数中被读取、使用。

纠正你的理解偏差 #

你之前认为“类型构造器中的内容在运行时都不会被使用，所以它实际上始终是0”是错误的。这里的0不是参数的取值，而是擦除标记，和参数的具体数值无关。比如你可以写Foo 7这种类型，编译时它是合法的，但运行时这个7会被完全删掉，不会被保留。

使用擦除参数的意义 #

• 性能优化：去掉运行时无用的参数，减少内存占用和冗余计算
• 语义明确：清晰告知代码阅读者，这个参数仅用于类型层面的约束，不影响运行时逻辑

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