dependent-type - 在依赖类型的编程语言中，Type-in​​-Type 是否适用于编程？

Question

在具有依赖类型的语言中，您可以使用 Type-in​​-Type 来简化语言并赋予它很多功能。这使得语言在逻辑上不一致，但如果您只对编程感兴趣而不对定理证明感兴趣，这可能不是问题。

在 Cayenne论文(一种用于编程的依赖类型语言)提到 Type-in​​-Type “未分层的类型系统将使在类型检查期间无法确定表达式对应于类型还是实值，并且不可能在运行时删除类型”(第 2.4 节)。

我对此有两个问题:

在某些依赖类型的语言(如 Agda)中，您可以明确说明应该删除哪些变量。在那种情况下，Type-in​​-Type 还会引起问题吗？

我们可以使用 Kind 将层次结构再扩展一步。哪里Type : Kind和 Kind : Kind .这仍然不一致，但现在您似乎可以知道术语是类型还是值。这样对吗？

Answer 1

the unstratified type system would make it impossible during typechecking to determine if an expression corresponds to a type or a realvalue and it would be impossible to remove the types at runtime

这是不正确的。 Type-in​​-type 防止删除证明，但它不防止删除类型，假设我们有没有类型化操作的参数多态性。最近的 GHC Haskell 是一个系统的例子，它同时支持类型输入、类型删除和类型级计算，但不支持证明删除。在依赖类型设置中，我们总是知道一个术语是否是一个类型；我们只检查它的类型是否是 Type .
类型删除只是删除类型 Type 的所有内容.
证明删除更复杂。假设我们有一个 Prop就像 Coq 中的 Universe，它旨在成为计算上不相关类型的 Universe。在这里，我们可以使用一些 p : Bool = Int胁迫证明 Bool -s 到 Int .如果语言一致，则没有 Bool = Int的封闭证明如此封闭的程序执行从未遇到过这样的强制。因此，即使我们清除了所有强制，封闭程序的执行也是安全的。
如果语言不一致，证明矛盾的唯一方法是无限循环，则有 Bool = Int 的发散闭证明。 .现在，封闭的程序执行实际上可以证明是错误的；但是我们仍然可以有类型安全，通过要求强制必须评估证明参数。然后，每当我们通过 false 强制执行时，程序就会循环，因此执行永远不会到达程序的不健全部分。
这里的关键点可能是 A = B : Prop支持强制，它消除了计算相关的宇宙，但参数 Type宇宙根本没有消元原理，不能影响计算。
删除可以通过多种方式进行概括。例如，我们可能有任何具有单个构造函数的归纳数据类型(并且没有从其他地方无法获得的存储数据，例如类型索引)，并尝试删除该构造函数上的每个匹配项。如果语言是完整的，这又是合理的，否则就不是。如果我们没有 Prop宇宙，我们仍然可以像这样删除。 IIRC Idris 经常这样做。