haskell - 依赖强制语言的一致性是什么意思？

Question

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

unlike Coq and Agda, Haskell relies on the consistency of a coercion language, which is not threatened by * :: *. See the paper for more details.

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

Answer 1

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

这一特性使得使用 Coq 和 Agda 作为证明系统成为可能:人们可以使用它们来证明数学事实。事实上，通过 Curry-Howard 对应关系，如果

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 .这只能触发异常，或者无法终止，所以 ...部分永远达不到。 Haskell 无法优化 coerce作为一个不安全的 Actor ，不像 Agda/Coq。

引用的段落提到了 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 仍然评估两个输入证明，以保持类型安全)。但是，拥有中间证明可以有力地确保编译器做的是正确的事情。