Lab*_*kak 5 type-theory dependent-type
在具有依赖类型的语言中，您可以使用 Type-in-Type 来简化语言并赋予它很多功能。这使得语言在逻辑上不一致，但如果您只对编程感兴趣而不对定理证明感兴趣，这可能不是问题。
在Cayenne论文（一种用于编程的依赖类型语言）中提到了 Type-in-Type，“未分层的类型系统将使在类型检查期间无法确定表达式对应于类型还是实值，并且不可能在运行时删除类型”（第 2.4 节）。
我对此有两个问题：
KindwhereType : Kind和将层次结构扩展一个额外的步骤Kind : Kind。这仍然不一致，但现在您似乎可以知道术语是类型还是值。这样对吗？非分层类型系统将使得在类型检查期间无法确定表达式是否对应于类型或实际值，并且无法在运行时删除类型
这是不正确的。Type-in-type 可以防止删除proofs，但它不会防止删除类型，假设我们有参数多态性而没有 typecase 操作。最近的 GHC Haskell 是同时支持 type-in-type、类型擦除和类型级计算，但不支持证明擦除的系统的一个例子。在独立类型设置中，我们总是知道一个术语是否是一种类型；我们只检查它的类型是否是Type.
类型擦除只是擦除所有带有 type 的东西Type。
证明擦除更加复杂。假设我们有一个Prop像 Coq 中那样的宇宙，它的目的是成为一个由计算上不相关的类型组成的宇宙。在这里，我们可以使用一些p : Bool = Int证据来强制Bool-s 为Int。如果语言是一致的，那么就没有封闭的证明，Bool = Int所以封闭的程序执行永远不会遇到这样的强制。因此，即使我们删除所有强制，封闭的程序执行也是安全的。
如果语言不一致，并且证明矛盾的唯一方法是通过无限循环，则存在 的发散封闭证明Bool = Int。现在，封闭的程序执行实际上可以证明虚假性；但我们仍然可以通过要求强制必须评估证明参数来实现类型安全。然后，每当我们通过虚假强制时，程序就会循环，因此执行永远不会到达程序中不健全的部分。
也许这里的关键点是A = B : Prop支持强制，它消除到计算相关的宇宙中，但参数Type宇宙根本没有消除原理，不能影响计算。
擦除可以通过多种方式进行概括。例如，我们可能有任何具有单个构造函数的归纳数据类型（并且没有存储从其他地方无法获得的数据，例如类型索引），并尝试删除该构造函数上的每个匹配。如果语言是完整的，那么这也是合理的，反之则不然。如果我们没有Prop宇宙，我们仍然可以像这样进行擦除。IIRC Idris 经常这样做。