dependent-type - 为什么我不能在 MMT(使用 PLF)中使用带有类型参数的定义？

Question

我正在尝试使用 ur:?PLF 定义对:

theory pairs : ur:?PLF =
    pair :      {a : type} a ⟶ a ⟶ (a ⟶ a ⟶ a) ⟶ a ❙    // okay     ❙
    pair_kind = {a : type} a ⟶ a ⟶ (a ⟶ a ⟶ a) ⟶ a ❙    // not okay ❙
❚

pair 的声明符合我的预期。但是，pair_kind 的定义没有。

这是预期的行为吗？我不明白这是怎么回事。

Answer 1

您正在使用 PLF，它使用浅层多态性 扩展了 LF - 浅层意味着类型的量化仅允许在类型的外部。

为了实现这一点，表达式 {a : type} ... 不允许自己输入类型，否则您可以不受限制地自由量化类型。

这在 PLF 中的工作方式是 {a : type} ... 形式的表达式 inhabitable 但是 - 正如我提到的 - 不是 typed 。 Inhabitable 意思是，它可以作为常量的“类型”出现。因为它不是类型化的，所以您不能在表达式中使用该类型的常量(如 pair)，除非您提供类型参数。所以 pair 没有类型，但是 pair A(对于某些类型 A)有。

这就是为什么 pair : {a : type} ... 被接受的原因。

当您执行 pair_kind = {a : type} ... 时，您提供表达式作为定义而不提供类型，这意味着 MMT 将尝试推断一个 - 并且(因为此表达式未键入)失败。

如果你想让pair_kind工作，你需要使用更强的类型系统。例如 LFX 中的 ?LFHierarchy，它有一个累积的宇宙层次结构(U n 代表每个正整数 n)，并将 type 定义为 U 0 和 kind 为 U 1。