如何阅读这个GHC核心“certificate”？

我写了这个Haskell的一小部分来弄清GHC如何certificate对于自然数，你只能减半：

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies #-} module Nat where data Nat = Z | S Nat data Parity = Even | Odd type family Flip (x :: Parity) :: Parity where Flip Even = Odd Flip Odd = Even data ParNat :: Parity -> * where PZ :: ParNat Even PS :: (x ~ Flip y, y ~ Flip x) => ParNat x -> ParNat (Flip x) halve :: ParNat Even -> Nat halve PZ = Z halve (PS a) = helper a where helper :: ParNat Odd -> Nat helper (PS b) = S (halve b) 

核心的相关部分变成：

 Nat.$WPZ :: Nat.ParNat 'Nat.Even Nat.$WPZ = Nat.PZ @ 'Nat.Even @~ <'Nat.Even>_N Nat.$WPS :: forall (x_apH :: Nat.Parity) (y_apI :: Nat.Parity). (x_apH ~ Nat.Flip y_apI, y_apI ~ Nat.Flip x_apH) => Nat.ParNat x_apH -> Nat.ParNat (Nat.Flip x_apH) Nat.$WPS = \ (@ (x_apH :: Nat.Parity)) (@ (y_apI :: Nat.Parity)) (dt_aqR :: x_apH ~ Nat.Flip y_apI) (dt_aqS :: y_apI ~ Nat.Flip x_apH) (dt_aqT :: Nat.ParNat x_apH) -> case dt_aqR of _ { GHC.Types.Eq# dt_aqU -> case dt_aqS of _ { GHC.Types.Eq# dt_aqV -> Nat.PS @ (Nat.Flip x_apH) @ x_apH @ y_apI @~ <Nat.Flip x_apH>_N @~ dt_aqU @~ dt_aqV dt_aqT } } Rec { Nat.halve :: Nat.ParNat 'Nat.Even -> Nat.Nat Nat.halve = \ (ds_dJB :: Nat.ParNat 'Nat.Even) -> case ds_dJB of _ { Nat.PZ dt_dKD -> Nat.Z; Nat.PS @ x_aIX @ y_aIY dt_dK6 dt1_dK7 dt2_dK8 a_apK -> case a_apK `cast` ((Nat.ParNat (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N ; Nat.TFCo:R:Flip[0]))_R :: Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd) of _ { Nat.PS @ x1_aJ4 @ y1_aJ5 dt3_dKa dt4_dKb dt5_dKc b_apM -> Nat.S (Nat.halve (b_apM `cast` ((Nat.ParNat (dt4_dKb ; (Nat.Flip (dt5_dKc ; Sym dt3_dKa ; Sym Nat.TFCo:R:Flip[0] ; (Nat.Flip (dt_dK6 ; Sym dt2_dK8))_N ; Sym dt1_dK7))_N ; Sym dt_dK6))_R :: Nat.ParNat x1_aJ4 ~# Nat.ParNat 'Nat.Even))) } } end Rec } 

我知道通过Fliptypes的实例来投射types的一般stream程，但有一些我不能完全遵循的东西：

• @~ <Nat.Flip x_apH>_N是什么意思？ 它是X的Flip实例吗？ 这与@ (Nat.Flip x_apH)什么不同？ 我对< >和_N都感兴趣

关于第一个铸造的halve ：

• dt_dK6 ， dt1_dK7和dt2_dK8代表什么？ 我明白他们是某种对等的certificate，但哪个是哪个？
• 我明白Sym反向运行等价
• 干什么？ 是吗？ 等值certificate是否按顺序应用？
• 这些_N和_R后缀是什么？
• 是TFCo:R:Flip[0]和TFCo:R:Flip[1]翻转的实例？

Answer 1

@~是强制申请。

尖括号表示其所包含types的自反强制，并带有下划线字母的作用。

因此， <Nat.Flip x_ap0H>_N是一个平等的certificate， Nat.Flip x_apH等于Nat.Flip x_apH名义上（作为平等的types不只是平等的表示）。

PS有很多争论。 我们看看智能的构造函数$WPS ，我们可以看到前两个分别是x和y的types。 我们certificate构造函数的参数是Flip x （在这种情况下，我们有Flip x ~ Even ParNat x然后我们得到ParNat x x ~ Flip y和ParNat x的certificate，最后一个参数是ParNat x的值。

我现在将通过typesNat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd的第一个演员Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd

我们从(Nat.ParNat ...)_R开始。 这是一个types构造器应用程序。 它将x_aIX ~# 'Nat.Odd的certificatex_aIX ~# 'Nat.Odd到Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd 。 R表示这意味着这种types是同构的，但不是相同的（在这种情况下它们是相同的，但是我们不需要这些知识来执行演员）。

现在我们看certificate的主体(dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]) 。 ; 意味着过渡性，即按顺序应用这些certificate。

dt1_dK7是x_aIX ~# Nat.Flip y_aIY的certificate。

如果我们看一下(dt2_dK8 ; Sym dt_dK6) 。 dt2_dK8显示y_aIY ~# Nat.Flip x_aIX 。 dt_dK6的types是'Nat.Even ~# Nat.Flip x_aIX 。 所以Sym dt_dK6的types是Nat.Flip x_aIX ~# 'Nat.Even和(dt2_dK8 ; Sym dt_dK6)的types是y_aIY ~# 'Nat.Even

因此(Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N是一个certificateNat.Flip y_aIY ~# Nat.Flip 'Nat.Even 。

Nat.TFCo:R:Flip[0]是Nat.Flip 'Nat.Even ~# 'Nat.Odd'的翻Nat.Flip 'Nat.Even ~# 'Nat.Odd'的第一个规则。

把它们放在一起，我们得到(dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0])具有typesx_aIX #~ 'Nat.Odd 。

第二个更复杂的演员有点难，但应该按照相同的原则工作。