在依赖类型的编程语言中，Type-in-Type 是否适用于编程？
In a dependently typed programming language is Type-in-Type practical for programming?
在具有依赖类型的语言中，您可以使用 Type-in-Type 来简化语言并赋予它很多功能。这使得语言在逻辑上不一致，但如果您只对编程感兴趣而不是定理证明，这可能不是问题。
在 Cayenne 论文（一种用于编程的依赖类型语言）中提到了类型输入，即 "the unstratified type system would make it impossible during type checking to determine if an expression corresponds to a type or a real value and it would be impossible to remove the types at runtime"（第 2.4 节）。
关于这个我有两个问题：
- 在某些依赖类型的语言（如 Agda）中，您可以明确说明应删除哪些变量。那样的话Type-in-Type还会出问题吗？
- 我们可以使用
Kind 将层次结构额外扩展一步，其中 Type : Kind 和 Kind : Kind。这仍然不一致，但现在您似乎可以知道术语是类型还是值。这是正确的吗？
the unstratified type system would make it impossible during type
checking to determine if an expression corresponds to a type or a real
value and it would be impossible to remove the types at runtime
这是不正确的。 Type-in-type 防止擦除 proofs，但它不防止擦除类型，假设我们有参数多态性，没有类型化操作。最近的 GHC Haskell 是一个同时支持 type-in-type、type erasure 和 type-level 计算但不支持 proof erasure 的系统的例子。在依赖类型设置中，我们总是知道一个术语是否是一个类型；我们只是检查它的类型是否是 Type.
类型擦除就是擦除类型为Type的所有东西。
证明擦除比较复杂。假设我们有一个像 Coq 中那样的 Prop 宇宙，它旨在成为一个计算上无关类型的宇宙。在这里，我们可以使用一些 p : Bool = Int 证明将 Bool-s 强制转换为 Int。如果语言是一致的，则没有 Bool = Int 的封闭证明，因此封闭程序执行永远不会遇到这种强制转换。因此，即使我们删除所有强制转换，封闭程序执行也是安全的。
如果语言不一致，只有证明矛盾的方法是无限循环，则有Bool = Int的发散封闭证明。现在，封闭的程序执行实际上可以证明是错误的；但是我们仍然可以拥有类型安全，通过要求强制转换必须评估证明参数。然后，每当我们通过虚假强制执行时，程序就会循环，因此执行永远不会到达程序的不健全部分。
这里的关键点可能是A = B : Prop支持强制转换，它消除到计算相关的宇宙，但是参数Type宇宙根本没有消除原理，不能影响计算。
可以通过多种方式概括擦除。例如，我们可能有 any 具有单个构造函数的归纳数据类型（并且没有从其他地方不可用的存储数据，例如类型索引），并尝试擦除该构造函数上的每个匹配项.如果语言是完整的，这又是合理的，否则就不是。如果我们没有Prop宇宙，我们仍然可以像这样进行擦除。 IIRC 伊德里斯经常这样做。
我只想添加一条我认为与问题相关的注释。 Formality，一种基于自我类型的最小证明语言，是非终止的。我参与了关于 Formality 是否会出现段错误的 Reddit 讨论。一种可能发生的方法是，如果您可以证明 Nat == String，然后将 42 :: Nat 转换为 42 :: String，然后将其作为字符串打印出来，例如。但 不是 情况。虽然您可以在形式上证明 String == Int：
nat_is_string: Nat == String
nat_is_string
并且您可以使用它来将 Nat 转换为 String:
nat_str: String
42 :: rewrite x in x with nat_is_string
任何 print nat_str 的尝试，您的程序都不会发生段错误，它只会挂起。那是因为你不能抹去 Formality 中的平等证据。要理解为什么，让我们看看 Equal.rewrite 的定义（用于将 42 转换为 String）：
Equal.rewrite<A: Type, a: A, b: A>(e: Equal(A,a,b))<P: A -> Type>(x: P(a)): P(b)
case e {
refl: x
} : P(e.b)
一旦我们擦除类型，rewrite 的正常形式就变成了 λe. λx. e(x)。 e 存在相等性证据。在上面的示例中，nat_str 的正常形式是 而不是 42，而是 nat_is_string(42)。由于 nat_is_string 是等式证明，因此它有两个选择：要么停止并成为恒等式，在这种情况下它只是 return 42，要么永远挂起。在这种情况下，它不会停止，所以 nat_is_string(42) 永远不会 return 42。因此，它无法打印，任何使用它的尝试都会导致您的整个程序挂起，但不会导致段错误。
所以，简而言之，自我类型允许我们对 Equal、rewrite / subst 进行编码，并擦除所有类型信息，但不擦除相等性证据本身。
在具有依赖类型的语言中，您可以使用 Type-in-Type 来简化语言并赋予它很多功能。这使得语言在逻辑上不一致，但如果您只对编程感兴趣而不是定理证明，这可能不是问题。
在 Cayenne 论文（一种用于编程的依赖类型语言）中提到了类型输入，即 "the unstratified type system would make it impossible during type checking to determine if an expression corresponds to a type or a real value and it would be impossible to remove the types at runtime"（第 2.4 节）。
关于这个我有两个问题：
- 在某些依赖类型的语言（如 Agda）中，您可以明确说明应删除哪些变量。那样的话Type-in-Type还会出问题吗？
- 我们可以使用
Kind将层次结构额外扩展一步，其中Type : Kind和Kind : Kind。这仍然不一致，但现在您似乎可以知道术语是类型还是值。这是正确的吗？
the unstratified type system would make it impossible during type checking to determine if an expression corresponds to a type or a real value and it would be impossible to remove the types at runtime
这是不正确的。 Type-in-type 防止擦除 proofs，但它不防止擦除类型，假设我们有参数多态性，没有类型化操作。最近的 GHC Haskell 是一个同时支持 type-in-type、type erasure 和 type-level 计算但不支持 proof erasure 的系统的例子。在依赖类型设置中，我们总是知道一个术语是否是一个类型；我们只是检查它的类型是否是 Type.
类型擦除就是擦除类型为Type的所有东西。
证明擦除比较复杂。假设我们有一个像 Coq 中那样的 Prop 宇宙，它旨在成为一个计算上无关类型的宇宙。在这里，我们可以使用一些 p : Bool = Int 证明将 Bool-s 强制转换为 Int。如果语言是一致的，则没有 Bool = Int 的封闭证明，因此封闭程序执行永远不会遇到这种强制转换。因此，即使我们删除所有强制转换，封闭程序执行也是安全的。
如果语言不一致，只有证明矛盾的方法是无限循环，则有Bool = Int的发散封闭证明。现在，封闭的程序执行实际上可以证明是错误的；但是我们仍然可以拥有类型安全，通过要求强制转换必须评估证明参数。然后，每当我们通过虚假强制执行时，程序就会循环，因此执行永远不会到达程序的不健全部分。
这里的关键点可能是A = B : Prop支持强制转换，它消除到计算相关的宇宙，但是参数Type宇宙根本没有消除原理，不能影响计算。
可以通过多种方式概括擦除。例如，我们可能有 any 具有单个构造函数的归纳数据类型（并且没有从其他地方不可用的存储数据，例如类型索引），并尝试擦除该构造函数上的每个匹配项.如果语言是完整的，这又是合理的，否则就不是。如果我们没有Prop宇宙，我们仍然可以像这样进行擦除。 IIRC 伊德里斯经常这样做。
我只想添加一条我认为与问题相关的注释。 Formality，一种基于自我类型的最小证明语言，是非终止的。我参与了关于 Formality 是否会出现段错误的 Reddit 讨论。一种可能发生的方法是，如果您可以证明 Nat == String，然后将 42 :: Nat 转换为 42 :: String，然后将其作为字符串打印出来，例如。但 不是 情况。虽然您可以在形式上证明 String == Int：
nat_is_string: Nat == String
nat_is_string
并且您可以使用它来将 Nat 转换为 String:
nat_str: String
42 :: rewrite x in x with nat_is_string
任何 print nat_str 的尝试，您的程序都不会发生段错误，它只会挂起。那是因为你不能抹去 Formality 中的平等证据。要理解为什么，让我们看看 Equal.rewrite 的定义（用于将 42 转换为 String）：
Equal.rewrite<A: Type, a: A, b: A>(e: Equal(A,a,b))<P: A -> Type>(x: P(a)): P(b)
case e {
refl: x
} : P(e.b)
一旦我们擦除类型，rewrite 的正常形式就变成了 λe. λx. e(x)。 e 存在相等性证据。在上面的示例中，nat_str 的正常形式是 而不是 42，而是 nat_is_string(42)。由于 nat_is_string 是等式证明，因此它有两个选择：要么停止并成为恒等式，在这种情况下它只是 return 42，要么永远挂起。在这种情况下，它不会停止，所以 nat_is_string(42) 永远不会 return 42。因此，它无法打印，任何使用它的尝试都会导致您的整个程序挂起，但不会导致段错误。
所以，简而言之，自我类型允许我们对 Equal、rewrite / subst 进行编码，并擦除所有类型信息，但不擦除相等性证据本身。