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

Question

在走向观察类型理论的"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

康纳还在观察类型理论(交付)的底部提到了这种技术:

当然,解决方法是做GADT人员所做的事情,并明确地将归纳家族定义为命题平等.当然,你可以通过变性来运输它们.

但是,Haskell中的类型检查器知道范围中的等式约束,并且在类型检查期间实际使用它们.我们可以写

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

它不会因此在类型理论的工作,因为它是不够的,有一个证明a ~ b的范围能够通过这个公式改写:该证明还必须是refl因为在一个错误的假设类型检查的presense,成为不可判定因终止问题(类似这样).因此,当您Fin m在Haskell中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

在内核 Haskell中,详细阐述了某种

f {q} x = coerce q x

但它不在你的脸上.它也不是编译代码.像Haskell等式证明一样,OTT等式证明可以在用闭合项计算之前被删除.

题外话.要明确Haskell中的平等数据的状态,即GADT

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

真的给你了

Refl :: x ~ y -> Eq x y

但由于类型系统在逻辑上不合理,类型安全依赖于该类型的严格模式匹配:您无法擦除Refl,您必须在运行时计算并匹配它,但您可以擦除对应于证明的数据x~y.在OTT中,整个命题片段对于开放项是证明无关的,并且对于闭合计算是可擦除的.离题结束.

对此数据类型或该数据类型的相等性的可判定性并不特别相关(至少,如果您具有身份证明的唯一性;如果您不总是具有UIP,则可判定性是获取它的一种方式).模式匹配中出现的等式问题是在任意开放表达式上.这是很多绳索.但是机器当然可以决定片段,其中包含从变量和完全应用的构造函数构建的一阶表达式(这就是当你分割案例时Agda所做的事情:如果约束太奇怪,那就是barfs).OTT应该允许我们进一步推进高阶统一的可判定片段.如果你知道(forall x. f x = t[x])未知f,那相当于f = \ x -> t[x].

因此,"OTT中没有模式匹配"一直是一个深思熟虑的设计选择,因为我们一直希望它成为我们已经知道如何做的翻译的精心设计目标.相反,它是内核理论力量的严格升级.