观察类型理论中的模式匹配
Pattern matching in Observational Type Theory
在 Towards Observational Type Theory 的“5. 完整 OTT”部分的末尾，作者展示了如何在 OTT 中定义可强制构造的索引数据类型。这个想法基本上是像这样将索引数据类型转换为参数化：
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) 的底部也提到了这项技术：
The fix, of course, is to do what the GADT people did, and define
inductive families explicitly upto propositional equality. And then of
course you can transport them, by transisitivity.
然而，Haskell 中的类型检查器知道范围内的相等约束，并在类型检查期间实际使用它们。例如。我们可以写
f :: a ~ b => a -> b
f x = x
它在类型论中不起作用，因为在范围内有 a ~ b 的证明不足以用这个等式重写：证明也必须是 refl ，因为在存在错误假设的情况下，由于终止问题（类似于 this），类型检查变得不可判定。因此，当您在 Haskell m 中的 Fin m 上进行模式匹配时，每个分支中的 suc n 都被重写为 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 中的模式匹配是如何工作的？如果这确实是一个问题，是否有任何方法可以缓解它？
我想我会派出这个。我觉得这是一个奇怪的问题，但那是因为我自己的特殊旅程。简短的回答是：不要在 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
在内核 Haskell中，详细说明了某种
f {q} x = coerce q x
但它不在你的脸上。而且它也不在编译代码中。 OTT 等式证明，如 Haskell 等式证明，可以在使用 closed 项进行计算之前被删除。
题外话。为了清楚Haskell中平等数据的地位，GADT
data Eq :: k -> k -> * where
Refl :: Eq x x
真的给你
Refl :: x ~ y -> Eq x y
但是因为类型系统在逻辑上不健全，类型安全依赖于对该类型的严格模式匹配：你不能擦除 Refl 并且你真的必须计算它并在 [=59= 处匹配它]时间，但是你可以擦除x~y证明对应的数据。在 OTT 中，整个命题片段对于开放式术语是证明无关的，对于封闭式计算是可擦除的。 题外话结束
这个或那个数据类型的相等性的可判定性不是特别相关（至少，如果你有身份证明的唯一性则不是；如果你不总是有 UIP，可判定性有时是获得它的一种方式）。模式匹配中出现的等式问题是关于任意 open 表达式的。那是很多绳子。但是机器当然可以决定由变量构建的一阶表达式和完全应用的构造函数组成的片段（这就是 Agda 在拆分案例时所做的事情：如果约束太奇怪，事情就会失败）。 OTT 应该允许我们进一步推进更高阶统一的可判定片段。如果你知道 (forall x. f x = t[x]) 未知 f，那等同于 f = \ x -> t[x].
因此，"no pattern matching in OTT" 一直是经过深思熟虑的设计选择，因为我们一直希望它成为我们已经知道如何进行的翻译的详细说明目标。相反，它是内核理论能力的严格升级。
在 Towards Observational Type Theory 的“5. 完整 OTT”部分的末尾，作者展示了如何在 OTT 中定义可强制构造的索引数据类型。这个想法基本上是像这样将索引数据类型转换为参数化：
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) 的底部也提到了这项技术：
The fix, of course, is to do what the GADT people did, and define inductive families explicitly upto propositional equality. And then of course you can transport them, by transisitivity.
然而，Haskell 中的类型检查器知道范围内的相等约束，并在类型检查期间实际使用它们。例如。我们可以写
f :: a ~ b => a -> b
f x = x
它在类型论中不起作用，因为在范围内有 a ~ b 的证明不足以用这个等式重写：证明也必须是 refl ，因为在存在错误假设的情况下，由于终止问题（类似于 this），类型检查变得不可判定。因此，当您在 Haskell m 中的 Fin m 上进行模式匹配时，每个分支中的 suc n 都被重写为 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 中的模式匹配是如何工作的？如果这确实是一个问题，是否有任何方法可以缓解它？
我想我会派出这个。我觉得这是一个奇怪的问题，但那是因为我自己的特殊旅程。简短的回答是：不要在 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
在内核 Haskell中，详细说明了某种
f {q} x = coerce q x
但它不在你的脸上。而且它也不在编译代码中。 OTT 等式证明，如 Haskell 等式证明，可以在使用 closed 项进行计算之前被删除。
题外话。为了清楚Haskell中平等数据的地位，GADT
data Eq :: k -> k -> * where
Refl :: Eq x x
真的给你
Refl :: x ~ y -> Eq x y
但是因为类型系统在逻辑上不健全，类型安全依赖于对该类型的严格模式匹配：你不能擦除 Refl 并且你真的必须计算它并在 [=59= 处匹配它]时间，但是你可以擦除x~y证明对应的数据。在 OTT 中，整个命题片段对于开放式术语是证明无关的，对于封闭式计算是可擦除的。 题外话结束
这个或那个数据类型的相等性的可判定性不是特别相关（至少，如果你有身份证明的唯一性则不是；如果你不总是有 UIP，可判定性有时是获得它的一种方式）。模式匹配中出现的等式问题是关于任意 open 表达式的。那是很多绳子。但是机器当然可以决定由变量构建的一阶表达式和完全应用的构造函数组成的片段（这就是 Agda 在拆分案例时所做的事情：如果约束太奇怪，事情就会失败）。 OTT 应该允许我们进一步推进更高阶统一的可判定片段。如果你知道 (forall x. f x = t[x]) 未知 f，那等同于 f = \ x -> t[x].
因此，"no pattern matching in OTT" 一直是经过深思熟虑的设计选择，因为我们一直希望它成为我们已经知道如何进行的翻译的详细说明目标。相反，它是内核理论能力的严格升级。