观察类型理论中的模式匹配

Question

在Towards Observational Type Theory 的“5. Full OTT”部分的最后，作者展示了如何在 OTT 中定义 coercible-under-constructors 索引数据类型。这个想法基本上是将索引数据类型转换为参数化，如下所示：

data IFin : ℕ -> Set where
  zero : ∀ {n} -> IFin (suc n)
  suc  : ∀ {n} -> IFin n -> IFin (suc n)

data PFin (m : ℕ) : Set where
  zero : ∀ {n} -> suc n ≡ m -> PFin m
  suc  : ∀ {n} -> suc n ≡ m -> PFin n -> PFin m

Conor 在observational type theory (delivery) 的底部也提到了这种技术：

当然，解决方法是做 GADT 人所做的事情，并定义 归纳家庭明确地上升到命题平等。然后的 当然，您可以通过传递性来传输它们。

然而，Haskell 中的类型检查器知道范围内的相等约束，并在类型检查期间实际使用它们。例如。我们可以写

f :: a ~ b => a -> b
f x = x

在类型论中它不起作用，因为在范围内有一个 a ~ b 的证明不足以用这个等式重写：这个证明也必须是 refl，因为在由于终止问题（例如this），错误的假设类型检查变得无法确定。因此，当您在 Haskell 中对 Fin m 进行模式匹配时，m 在每个分支中都会被重写为 suc n，但这在类型论中不会发生，而是留下了 suc n ~ m 的明确证明。在 OTT 中，根本不可能对证明进行模式匹配，因此您既不能假装证明是 refl，也不能真正要求它。只能将证明提供给 coerce 或忽略它。

这使得编写任何涉及索引数据类型的东西变得非常困难。例如。向量的通常三行（包括类型签名）lookup 变成了这个野兽：

vlookupₑ : ∀ {n m a} {α : Level a} {A : Univ α} -> ⟦ n ≅ m ⇒ fin n ⇒ vec A m ⇒ A ⟧
vlookupₑ         p (fzeroₑ q)       (vconsₑ r x xs)      = x
vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vconsₑ {m′} r x xs) =
  vlookupₑ (left (suc n′) {m} {suc m′} (trans (suc n′) {n} {m} q p) r) i xs
vlookupₑ {n} {m} p (fzeroₑ {n′} q)  (vnilₑ r)            =
  ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r
vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vnilₑ r)            =
  ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r

vlookup : ∀ {n a} {α : Level a} {A : Univ α} -> Fin n -> Vec A n -> ⟦ A ⟧
vlookup {n} = vlookupₑ (refl n)

可以稍微简化一下，因为如果具有可判定相等的数据类型的两个元素明显相等，那么它们在通常的内涵意义上也是相等的，并且自然数确实具有可判定相等，所以我们可以强制所有方程与其内涵对应物和模式匹配，但这会破坏vlookup 的一些计算属性，并且无论如何都是冗长的。在更复杂的情况下处理无法确定相等性的索引几乎是不可能的。

我的推理正确吗？ OTT 中的模式匹配是如何工作的？如果这确实是一个问题，有什么方法可以缓解它？

Answer 1

我想我会派上这个。我觉得这是一个奇怪的问题，但那是因为我自己的特殊旅程。简短的回答是：不要在 OTT 或任何内核类型理论中进行模式匹配。这与永远不进行模式匹配是不一样的。

长答案基本上是我的博士论文。

在我的博士论文中，我展示了如何将以模式匹配风格编写的高级程序详细说明为内核类型理论，该理论仅具有归纳数据类型的归纳原则和对命题相等性的适当处理。模式匹配的阐述引入了关于数据类型索引的命题方程，然后通过统一解决它们。那时，我使用的是内涵平等，但观察平等至少给了你同样的力量。那就是：我的模式匹配技术（并因此将其排除在内核理论之外），隐藏所有等式猪圈笑话，早于升级到观察平等。你用来说明你的观点的可怕的 vlookup 可能对应于精化过程的输出，但输入不必那么糟糕。很好的定义

vlookup : Fin n -> Vec X n -> X
vlookup fz     (vcons x xs) = x
vlookup (fs i) (vcons x xs) = vlookup i xs

阐述得很好。在此过程中发生的方程求解与 Agda 在元级别通过模式匹配检查定义或 Haskell 所做的方程求解相同。不要被类似的程序所迷惑

f :: a ~ b => a -> b
f x = x

在 kernel Haskell 中，详细说明了某种

f {q} x = coerce q x

但它不在你的脸上。而且它也不在编译代码中。 OTT 等式证明，就像 Haskell 等式证明一样，可以在使用 封闭 项进行计算之前擦除。

题外话。为了清楚地了解 Haskell 中平等数据的状态，GADT

data Eq :: k -> k -> * where
  Refl :: Eq x x

真的给你

Refl :: x ~ y -> Eq x y

但是由于类型系统在逻辑上不健全，类型安全依赖于对该类型的严格模式匹配：你不能删除 Refl 并且你确实必须在运行时计算并匹配它，但是你 可以擦除x~y证明对应的数据。在 OTT 中，整个命题片段对于开放项是证明无关的，对于封闭计算是可擦除的。 题外话结束。

这种或那种数据类型的相等性的可判定性并不是特别相关（至少，如果您有身份证明的唯一性，则不是；如果您并不总是有 UIP，可判定性有时是一种获得它的方法）。模式匹配中出现的等式问题是在任意 open 表达式上。那是很多绳子。但是机器当然可以决定由变量构建的一阶表达式和完全应用的构造函数组成的片段（这就是 Agda 在拆分案例时所做的事情：如果约束太奇怪，那就太糟糕了）。 OTT 应该允许我们进一步推进高阶统一的可判定片段。如果您知道(forall x. f x = t[x]) 为未知的f，则相当于f = \ x -> t[x]。

因此，“OTT 中没有模式匹配”一直是经过深思熟虑的设计选择，因为我们一直希望它成为我们已经知道如何进行翻译的详细目标。相反，它是内核理论能力的严格升级。