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

Question

在“5. Full 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 

康纳尔还提到在observational type theory (delivery)底部这项技术：

的修复，当然是做什么的GADT人们做了，并明确定义归纳的家庭直至命题平等。然后 当然你可以运输他们，通过transisitivity。

但是，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 : 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 

被愚弄在内核哈斯克尔，即阐述对某种

f {q} x = coerce q x 

，但它不是在你的脸上。而且它也不在编译代码中。 OTT平等证明与Haskell平等证明一样，可以在计算前用关闭条款进行擦除。

Digression。要清楚在Haskell平等数据的状况，GADT

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

真的给你

Refl :: x ~ y -> Eq x y 

但由于类型系统是不是逻辑的声音，类型安全依赖于严格的模式匹配上这种类型：你不能擦除Refl，你真的必须计算它并在运行时匹配它，但你可以通过擦除对应于x~y的证明的数据。在OTT中，整个命题片断对于开放式术语来说是证明无关的，并且对于闭式计算而言是可擦除的。 结束离题。

在这个或那个数据类型上相等的可判定性不是特别相关的（至少，如果你有唯一性的身份证明;如果你不总是有UIP，可判定性是有时得到它的一种方法）。在模式匹配中出现的等式问题在任意开放式表达式中。这是很多绳索。但是机器当然可以决定由变量构建的一阶表达式和完全应用的构造函数组成的片段（这就是Agda在分割案例时所做的事情：如果约束条件太奇怪，那只是条形图）。 OTT应该使我们能够进一步推进高阶统一的可判断的片段。如果您知道(forall x. f x = t[x])未知f，那么相当于f = \ x -> t[x]。因此，“OTT中没有模式匹配”一直是故意的设计选择，因为我们一直希望它成为我们已经知道如何去做的翻译的阐述目标。相反，这是核心理论力量的严格提升。