非全函数在类型级别被视为常量？

Question

在 Type-Driven Development with Idris，第 6 章中，他说

• 类型级函数只存在于编译时 ...
• 只有总计的函数才会在类型级别进行评估。不完全的函数可能不会终止，或者可能不会覆盖所有可能的输入。因此，为了确保类型检查本身终止，不完全的函数在类型级别被视为常量，并且不会进一步评估。

我很难理解第二个要点的含义。

• 类型检查器如何声明代码类型检查是否存在其签名中不完全的函数？根据定义，不会有一些未定义类型的输入吗？
• 当他说恒定时，他的意思是否与the docs 中的意思相同，比如

  one: Nat
  one = 1
  

  是一个常数？如果是这样，那如何使类型检查器完成其工作？
• 如果一个类型级函数仅在编译时存在，如果它不是全部，它是否会被评估？如果不是，它的用途是什么？

Answer 1

部分类型级函数在 Skolem 意义上被视为常量：部分函数的调用 f 仍然是 f 没有进一步的意义。

让我们看一个例子。这里f是一个部分前驱函数：

f : Nat -> Nat
f (S x) = x

如果我们然后尝试在一个类型中使用它，它不会减少，即使 f 3 会减少到 2：

bad : f 3 = 2
bad = Refl

使用预期类型检查错误的右侧时 f 3 = 2

之间的类型不匹配 2 = 2（Refl 的类型） 和 f 3 = 2（预期类型）

所以f 在这里是一个原子常数，只代表它自己。当然，因为它确实代表它自己，所以下面仍然会进行类型检查：

good : f 3 = f 3
good = Refl