依赖强制语言的一致性是啥意思？

Posted 2023-02-18

【中文标题】依赖强制语言的一致性是啥意思？

【英文标题】：What does it mean to rely on the consistency of a coercion language?依赖强制语言的一致性是什么意思？

【发布时间】：2018-05-24 08:40:55

【问题描述】：

来自https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell，

与 Coq 和 Agda 不同，Haskell 依赖于强制语言的一致性，它不受 * :: * 的威胁。有关详细信息，请参阅论文。

引用的“论文”是broken link，但是，通过谷歌搜索和阅读它，我注意到它描述了如何向系统 FC 添加显式类型相等，但没有直接解决隐含的问题：它是什么意味着依赖强制语言的一致性？

【参考方案1】：

Coq 和 Agda 是依赖类型的total 语言。它们的灵感来自于它们相关的类型理论基础，其中涉及（类型化的）lambda 演算，它（强）归一化。这意味着减少任何 lambda 项最终都必须停止。

这个属性使得使用 Coq 和 Agda 作为证明系统成为可能：人们可以使用它们来证明数学事实。事实上，通过库里-霍华德的对应关系，如果

someExpression :: someType

那么someType对应一个逻辑（直觉）重言式。

在 Haskell 中，情况并非如此，因为任何类型都可以被“证明”

undefined :: someType

即我们可以使用“底部”值作弊。这使得 Haskell，作为一个逻辑，不一致。例如，我们可以证明undefined :: Data.Void.Void，它对应于逻辑“假”命题。这很糟糕，但这是为无限递归付出的必要代价，它允许非终止程序。

相比之下，Coq 和 Agda 只有原始递归（不能永远递归）。

现在，重点。众所周知，将公理* :: * 添加到 Coq / Agda 会使逻辑不再一致。我们可以使用 Girard 悖论推导出“错误”的证明。那会很糟糕，因为我们甚至可以证明lemma :: Int :~: String 之类的东西，并推导出一个强制函数coerce :: Int -> String。

lemma :: Int :~: String
lemma = -- exploit Girard's paradox here

-- using Haskell syntax:
coerce :: Int -> String
coerce x = case lemma of Refl -> x

如果我们天真地实现了这一点，coerce 将简单地执行不安全的强制转换，重新解释底层位——毕竟，lemma 证明了这些类型是完全一样的！这样我们甚至会失去运行时类型的安全性。厄运在等待。

在 Haskell 中，即使我们不添加 * :: *，无论如何我们都是不一致的，所以我们可以简单地拥有

lemma = undefined

并派生出coerce！因此，添加* :: * 并不会真正增加问题的数量。这只是不一致的另一个来源。

然后有人可能想知道为什么在 Haskell 中 coerce 是类型安全的。好吧，在 Haskell 中 case lemma of Refl ->... 强制评估 lemma。这只能触发异常，或者无法终止，因此永远不会到达... 部分。与 Agda / Coq 不同，Haskell不能将 coerce 优化为不安全的演员表。

引用的段落提到了 Haskell 的另一个方面：强制语言。在内部，当我们编写时

case lemma1 of
  Refl -> case lemma2 of
    Refl -> ...
      ...
        Refl -> expression

我们引入了许多必须利用的类型等式来证明expression 确实具有所需的类型。在 Coq 中，程序员必须使用复杂的匹配形式（依赖匹配）来证明在何处以及如何利用类型等式。在 Haskell 中，编译器为我们编写了这个证明（在 Coq 中，类型系统更丰富，我认为这将涉及更高阶的统一，这是无法确定的）。这个证明不是用 Haskell 写的！事实上，Haskell 是不一致的，所以我们不能依赖它。相反，Haskell 使用另一种自定义强制语言来保证是一致的。我们只需要依靠它。

如果我们转储 Core，我们可以看到一些内部强制语言。例如，编译传递性证明

trans :: a :~: b -> b :~: c -> a :~: c
trans Refl Refl = Refl

我们得到

GADTtransitivity.trans
  :: forall a_au9 b_aua c_aub.
     a_au9 :~: b_aua -> b_aua :~: c_aub -> a_au9 :~: c_aub
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType]
GADTtransitivity.trans =
  \ (@ a_auB)
    (@ b_auC)
    (@ c_auD)
    (ds_dLB :: a_auB :~: b_auC)
    (ds1_dLC :: b_auC :~: c_auD) ->
    case ds_dLB of _ [Occ=Dead]  Refl cobox0_auF ->
    case ds1_dLC of _ [Occ=Dead]  Refl cobox1_auG ->
    (Data.Type.Equality.$WRefl @ * @ a_auB)
    `cast` ((<a_auB>_N :~: (Sym cobox0_auF ; Sym cobox1_auG))_R
            :: ((a_auB :~: a_auB) :: *) ~R# ((a_auB :~: c_auD) :: *))
    
    

注意最后的cast，它利用了强制语言中的证明

(<a_auB>_N :~: (Sym cobox0_auF ; Sym cobox1_auG))_R

在这个证明中，我们可以看到Sym cobox0_auF ; Sym cobox1_auG，我猜它使用对称性Sym 和传递性; 来达到想要的目标：证明Refl :: a_auB :~: a_auB 确实可以安全地转换为想要的a_auB :~: c_auD。

最后，请注意，我很确定这些证明会在 GHC 编译期间被丢弃，并且cast 最终会在运行时减少为不安全的强制转换（case 仍然评估两个输入证明，以保留类型安全）。但是，拥有中间证明可以有力地确保编译器做的是正确的事情。

【讨论】：

“然后在 GHC 编译期间丢弃此类证明”。希望，但肯定不总是。要是……

@Alec 不，我有理由确定它们在某些时候会被删除。请注意，a :~: b 证明不会被删除，而是 - 只有特殊强制语言中的证明是（我认为）。

确实，Sulzmann 等人。说“像类型一样，强制在运行程序之前被删除，因此它们保证没有运行时成本。” (dl.acm.org/citation.cfm?id=1190324) 并且可以公平地假设此属性保留在 GHC Core 中，它建立在本文的未来演变之上。

“但这是为无限递归付出的必要代价，它允许非终止程序”。为了完整起见，在 Agda 中存在 corecursion，它是另一种允许非终止程序同时也保证“前进进度”的方式。