Idris中参数名前的0或1（RigCount）代表什么含义？

RigCount是Idris 2线性类型系统内置的参数多重性标注，作用是给参数加上编译期强制校验的使用次数约束，不符合约束的代码会直接在类型检查阶段报错，一共有三类合法的标注值：

• 0：擦除参数
  被标记的参数仅在编译期类型检查阶段存在，运行时会被完全擦除，绝对不能出现在需要运行时执行的函数体逻辑中。
  你给出的第一段代码报错的原因就在这：参数x被标为0，属于运行时不存在的擦除内容，你在函数右式直接返回x，相当于要在运行时访问这个根本不存在的值，编译器就会抛出x is not accessible in this context的错误。
  这类标注通常用来传递类型索引、定理证明项这类只服务于编译期校验、运行时不需要保留的内容，可以有效减少运行时内存开销。合法的0参数用法示例：

  // n是向量长度索引，仅做类型约束，运行时擦除
  mapVec : (0 n : Nat) -> (a -> b) -> Vec n a -> Vec n b
  mapVec _ f [] = []
  mapVec n f (x::xs) = f x :: mapVec (pred n) f xs
  

• 1：线性参数
  被标记的参数在函数体中必须恰好被使用1次，既不能完全不引用，也不能重复使用。
  你给出的第二段代码能通过检查，就是因为参数x被标为1，函数体直接返回x刚好满足“使用1次”的要求。如果违反使用次数要求就会报错，比如：

  duplicate : (1 a : b) -> (b, b)
  duplicate x = (x, x) -- 报错：x被重复使用2次，违反线性约束
  

  这类标注主要用来做资源安全建模，比如文件句柄、申请的堆内存这类需要严格管控生命周期的资源，用1标注可以保证资源不会被泄露、不会被重复释放。
• 无标注（隐式值ω）：普通无约束参数
  就是日常写函数默认的参数形式，使用次数没有任何限制，不用、用一次、重复调用都可以，编译器不会做次数校验。

核心使用规则 #

• 多重性约束会沿着函数调用链传递校验：如果把1标注的线性参数传给其他函数，被调用的函数也必须恰好消费该参数1次，否则整个调用链都会检查失败。
• 0标注的擦除参数只能参与编译期的类型层面计算，不能出现在任何会被编译为运行时执行的表达式中。
• 多重性标注可以同时用在显式参数、隐式参数上，约束规则完全一致。

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