非总函数在类型级别被视为常量？
Non-total functions are treated as constants at the type level?
在使用 Idris 进行类型驱动开发，第 6 章，他说
- Type-level functions exist at compile time only ...
- Only functions that are total will be evaluated at the type level. A function that isn't total may not terminate, or may not cover all possible inputs. Therefore, to ensure that type-checking itself terminates, functions that are not total are treated as constants at the type level, and don't evaluate further.
我很难理解第二个要点的含义。
- 类型检查器如何声称代码类型检查是否存在其签名中不完整的函数？根据定义，是否会有一些未定义类型的输入？
- 当他说常量时，他的意思和the docs中的意思一样吗，比如
one: Nat
one = 1
是常数？如果是这样，那如何使类型检查器完成其工作？
- 如果类型级函数仅在编译时存在，如果它不是完整的，是否会对其求值？如果不是，它有什么作用？
部分类型级函数在 Skolem 意义上被视为常量：部分函数的调用 f 保持 f 没有进一步的意义。
让我们看一个例子。这里 f 是部分前置函数：
f : Nat -> Nat
f (S x) = x
如果我们然后尝试在类型中使用它，它不会减少，即使 f 3 会减少到 2:
bad : f 3 = 2
bad = Refl
When checking right hand side of bad with expected type
f 3 = 2
Type mismatch between
2 = 2 (Type of Refl)
and
f 3 = 2 (Expected type)
所以f在这里是一个原子常数，只代表它自己。当然，因为它 确实 代表它自己，下面仍然是类型检查：
good : f 3 = f 3
good = Refl
在使用 Idris 进行类型驱动开发，第 6 章，他说
- Type-level functions exist at compile time only ...
- Only functions that are total will be evaluated at the type level. A function that isn't total may not terminate, or may not cover all possible inputs. Therefore, to ensure that type-checking itself terminates, functions that are not total are treated as constants at the type level, and don't evaluate further.
我很难理解第二个要点的含义。
- 类型检查器如何声称代码类型检查是否存在其签名中不完整的函数？根据定义，是否会有一些未定义类型的输入？
- 当他说常量时，他的意思和the docs中的意思一样吗，比如
是常数？如果是这样，那如何使类型检查器完成其工作？one: Nat one = 1 - 如果类型级函数仅在编译时存在，如果它不是完整的，是否会对其求值？如果不是，它有什么作用？
部分类型级函数在 Skolem 意义上被视为常量：部分函数的调用 f 保持 f 没有进一步的意义。
让我们看一个例子。这里 f 是部分前置函数：
f : Nat -> Nat
f (S x) = x
如果我们然后尝试在类型中使用它，它不会减少，即使 f 3 会减少到 2:
bad : f 3 = 2
bad = Refl
When checking right hand side of bad with expected type
f 3 = 2Type mismatch between
2 = 2(Type ofRefl) andf 3 = 2(Expected type)
所以f在这里是一个原子常数，只代表它自己。当然，因为它 确实 代表它自己，下面仍然是类型检查：
good : f 3 = f 3
good = Refl