观察型理论中的模式匹配 [英] Pattern matching in Observational Type Theory
问题描述
在走向观察型理论的5. Full OTT部分的最后，作者展示了如何定义强制 - OTT中的构造器下索引数据类型。这个想法基本上是将索引数据类型转换为像这样的参数化数据：
data IFin：ℕ - >设置
zero：∀{n} - > IFin（suc n）
suc：∀{n} - > IFin n - > IFin（suc n）
data PFin（m：ℕ）：设置
zero：∀{n} - > suc n≡m - > PFin m
suc：∀{n} - > suc n≡m - > PFin n - > PFin m
Conor还在：
当然，这个解决办法是做GADT人做的事，并明确定义
归纳族，直到命题平等。然后
当然可以通过transisitivity传输它们。
然而，Haskell中的类型检查器知道等式约束在范围内，并在类型检查时实际使用它们。例如。我们可以写出：
f :: a〜b => a - > b
fx = x
它在类型理论中不起作用，因为它不够在范围内有 a〜b 的证据可以用这个等式来重写：证明也必须是 refl ，因为在虚假假设的存在下，类型检查由于终止问题而变得不可判定（诸如 this ）。因此，当你在Haskell m 中重写 suc n code>在每个分支中，但这不可能发生在类型理论中，而是留下明确的证明 suc n〜m 。在OTT中，根本不可能对证据进行模式匹配，因此您既不能假装证明是 refl ，也不需要实际证明。只能向 coerce 提供证明或者忽略它。
这使得很难写任何东西涉及索引数据类型。例如。通常的三行代码（包括类型签名） lookup 成为这个野兽：
vlookupₑp（fzeroₑq）（vconsₑrx xs）= x
vlookupₑ{n} {m} p（fsucₑ{n'} qi ）（vconsₑ{m'} rx xs）=
vlookupₑ（left（suc n'）{m} {suc m'}（trans（suc n'）{n} {m} qp）r）i xs
vlookupₑ{n} {m} p（fzeroₑ{n'} q）（vnilₑr）=
⊥-elim $ left（suc n'）{m} {0} '）{n} {m} qp）r
vlookupₑ{n} {m} p（fsucₑ{n'} qi）（vnilₑr）=
⊥-elim $ left（suc n'） {m} {0}（trans（suc n'）{n} {m} qp）r
vlookup：∀{na} {α：等级a} {A：Univα} - > ; Fin n - > Vec A n - > ⟦A⟧
vlookup {n} =vlookupₑ（refl n）
可能是因为如果一个具有可判定的等式的数据类型的两个元素是明显相等的，那么它们在通常的内涵意义上也是相等的，并且自然数确实具有可判定的相等性，因此我们可以将所有等式强迫为它们的内涵对应物，并且模式匹配，但这会破坏 vlookup 的一些计算属性，并且无论如何都是冗长的。几乎不可能处理更复杂的指数，而这些指数的平等性是无法决定的。
我的推理是否正确？ OTT中的模式匹配是如何工作的？如果这确实是一个问题，有什么办法可以缓解它吗？
我想我会介绍这一个。我觉得这是一个奇怪的问题，但那是因为我自己的特定旅程。简短的答案是：不要在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 - >在 kernel Haskell中，详细阐述了如何在内核中使用这些内核。 某种形式的
f {q} x =胁迫qx
但它不在你的脸上。而且它也不在编译代码中。 OTT平等证明与Haskell平等证明一样，可以在使用 closed 条件进行计算之前删除。
Digression。要清楚Haskell中的平等数据的状态，GADT
data Eq :: k - > k - > *其中
Refl :: Eq xx
真的会带给您
Refl :: x〜y - >公式xy
但是由于类型系统在逻辑上不合理，类型安全依赖于严格的模式匹配键入：你不能擦除 Refl ，并且你真的必须计算它并在运行时匹配它，但是你可以擦除对应于证明 x〜y 。在OTT中，整个命题片断对于开放式术语来说是证明无关的，并且对于闭式计算而言是可擦除的。
在这个或那个数据类型上相等的可判定性并不特别相关（至少，如果你有唯一性的身份证明;如果你不总是有UIP，decidability是有时得到它的一种方法）。在模式匹配中出现的等式问题在任意 open 表达式上。这是很多绳索。但是机器当然可以决定由变量构建的一阶表达式和完全应用的构造函数组成的片段（这就是Agda在分割案例时所做的事情：如果约束条件太奇怪，那只是条形图）。 OTT应该使我们能够进一步推进高阶统一的可判断的片段。如果您知道（forall x。fx = t [x]）为未知 f ，则相当于 f = \ x - >因此，OTT中没有模式匹配一直是一个有意的设计选择，正如我们一直打算的那样。t [x] 。
成为我们已经知道如何去做的翻译的阐述目标。相反，它是内核理论力量的严格升级。
In the end of the "5. Full OTT" section of Towards Observational Type Theory the authors show how to define coercible-under-constructors indexed data types in OTT. The idea is basically to turn indexed data types into parameterized like this:
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 also mentions this technique at the bottom of 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.
However a type checker in Haskell is aware of equality constraints in scope and actually uses them during type checking. E.g. we can write
f :: a ~ b => a -> b
f x = x
It doesn't work so in type theory, since it's not enough to have a proof of a ~ b in scope to be able to rewrite by this equation: that proof also must be refl, because in the presense of a false hypothesis type checking becomes undecidable due to termination issues (something like this). So when you pattern match on Fin m in Haskell m gets rewritten to suc n in each branch, but that can't happen in type theory, instead you're left with an explicit proof of suc n ~ m. In OTT it's not possible to pattern match on proofs at all, hence you can neither pretend the proof is refl nor actually require that. It's only possible to supply the proof to coerce or just ignore it.
This makes it very hard to write anything that involves indexed data types. E.g. the usual three-lines (including the type signature) lookup for vectors becomes this beast:
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)
It could be a bit simplified, since if two elements of a data type that has decidable equality are observably equal, then they are also equal in the usual intensional sense, and natural numbers do have decidable equality, so we can coerce all the equations to their intensional counterparts and pattern match on them, but that would break some computational properties of vlookup and is verbose anyway. It's nearly impossible to deal in more complicated cases with indices which equality cannot be decided.
Is my reasoning correct? How is pattern matching in OTT meant to work? If this is a problem indeed, are there any ways to mitigate it?
解决方案 I guess I'll field this one. I find it a strange question, but that's because of my own particular journey. The short answer is: don't do pattern matching in OTT, or in any kernel type theory. Which is not the same thing as to not do pattern matching ever.
The long answer is basically my PhD thesis.
In my PhD thesis, I show how to elaborate high-level programs written in a pattern matching style into a kernel type theory which has only the induction principles for inductive datatypes and a suitable treatment of propositional equality. The elaboration of pattern matching introduces propositional equations on datatype indices, then solves them by unification. Back then, I was using an intensional equality, but observational equality gives you at least the same power. That is: my technology for elaborating pattern matching (and thus keeping it out of the kernel theory), hiding all the equational piggery-jokery, predates the upgrade to observational equality. The ghastly vlookup you've used to illustrate your point might correspond to the output of the elaboration process, but the input need not be that bad. The nice definition
vlookup : Fin n -> Vec X n -> X
vlookup fz (vcons x xs) = x
vlookup (fs i) (vcons x xs) = vlookup i xs
elaborates just fine. The equation-solving that happens along the way is just the same equation-solving that Agda does at the meta-level when checking a definition by pattern matching, or that Haskell does. Don't be fooled by programs like
f :: a ~ b => a -> b
f x = x
In kernel Haskell, that elaborates to some sort of
f {q} x = coerce q x
but it's not in your face. And it's not in compiled code, either. OTT equality proofs, like Haskell equality proofs, can be erased before computing with closed terms.
Digression. To be clear about the status of equality data in Haskell, the GADT
data Eq :: k -> k -> * where
Refl :: Eq x x
really gives you
Refl :: x ~ y -> Eq x y
but because the type system is not logically sound, type safety relies on strict pattern matching on that type: you can't erase Refl and you really must compute it and match it at run time, but you can erase the data corresponding to the proof of x~y. In OTT, the entire propositional fragment is proof-irrelevant for open terms and erasable for closed computation. End of digression.
The decidability of equality on this or that datatype is not especially relevant (at least, not if you have uniqueness of identity proofs; if you don't always have UIP, decidability is one way to get it sometimes). The equational problems which show up in pattern matching are on arbitrary open expressions. That's a lot of rope. But a machine can certainly decide the fragment which consists of first-order expressions built from variables and fully applied constructors (and that's what Agda does when you split cases: if the constraints are too weird, the thing just barfs). OTT should allow us to push a bit further into the decidable fragments of higher-order unification. If you know (forall x. f x = t[x]) for unknown f, that's equivalent to f = \ x -> t[x].
So, "no pattern matching in OTT" has always been a deliberate design choice, as we always intended it to be an elaboration target for a translation we already knew how to do. Rather, it's a strict upgrade in kernel theory power.
这篇关于观察型理论中的模式匹配的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
