依靠强制语言的一致性意味着什么？

Question

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

与Coq和Agda不同,Haskell依赖于强制语言的一致性,而不受*::*的威胁.有关详细信息,请参阅该文章.

引用的"论文"是一个断开的链接,但是,通过谷歌搜索并阅读它,我注意到它描述了如何向系统FC添加显式的类型相等,但没有直接解决隐含的问题:依赖于它的一致性是什么意思强制语言？

Answer 1

Coq和Agda是依赖类型的总语言.它们的灵感来自于它们的相对类型理论基础,它们涉及(强)正规化的(类型)lambda演算.这意味着减少任何lambda术语最终都必须停止.

该属性使得可以使用Coq和Agda作为证明系统:可以使用它们来证明数学事实.的确,通过库里 - 霍华德的通信,如果

someExpression :: someType

然后someType对应于逻辑(直觉)重言式.

在Haskell中,情况并非如此,因为任何类型都可以"证明"

undefined :: someType

即我们可以使用"底部"值作弊.这使得Haskell作为一种逻辑不一致.例如,我们可以证明undefined :: Data.Void.Void,这对应于逻辑"错误"命题.这很糟糕,但是无限递归需要付出代价,这允许非终止程序.

相比之下,Coq和Agda只有原始递归(永远不会永远递归).

现在,到了这一点.众所周知,将公理添加* :: *到Coq/Agda会使逻辑不再一致.我们可以使用吉拉德的悖论得出"假"的证明.那将是非常糟糕的,因为我们甚至可以证明这样的事情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仍然会评估两个输入证明,以保持类型安全).但是,拥有一个中间证明可以确保编译器正在做正确的事情.