如何阅读GHC核心"证据"？

Question

我写了一小部分Haskell来弄清楚GHC如何证明对于自然数,你只能将偶数的一半:

{-# 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 }

我知道通过Flip类型系列的实例来转换类型的一般流程,但有些事情我无法完全遵循:

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

关于第一次演员halve:

• 什么dt_dK6,dt1_dK7并dt2_dK8代表什么？我知道它们是某种等价证明,但哪个是哪个？
• 据我所知,Sym向后贯穿等价
• 这;是做什么的？等效证明是否仅按顺序应用？
• 这些_N和_R后缀是什么？
• 是TFCo:R:Flip[0]和TFCo:R:Flip[1]Flip的实例？

Answer 1

@~ 是胁迫申请.

尖括号表示其所包含类型的反身强制与强调字母给出的作用.

因此<Nat.Flip x_ap0H>_N,等价证明Nat.Flip x_apH等于Nat.Flip x_apH名义上(作为相等的类型而不仅仅是相等的表示).

PS有很多争论.我们看一下智能构造函数$WPS,我们可以看到前两个分别是x和y的类型.我们已经证明了构造函数的参数是Flip x(在这种情况下我们有Flip x ~ Even.然后我们有证明x ~ Flip y和y ~ Flip x.最后的参数是一个值ParNat x.)

我现在将介绍第一个类型的演员表 Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd

我们一开始(Nat.ParNat ...)_R.这是一个类型构造函数应用程序.它提升的证明x_aIX ~# 'Nat.Odd来Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd.该R意味着它这个表象意味着该类型是同构的,但不一样的(在这种情况下,他们是相同的,但我们并不需要这些知识来执行转换).

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

dt1_dK7是证明x_aIX ~# Nat.Flip y_aIY.

如果我们看一下(dt2_dK8 ; Sym dt_dK6).dt2_dK8节目y_aIY ~# Nat.Flip x_aIX.dt_dK6是类型的 'Nat.Even ~# Nat.Flip x_aIX.所以Sym dt_dK6是类型Nat.Flip x_aIX ~# 'Nat.Even和(dt2_dK8 ; Sym dt_dK6)类型y_aIY ~# 'Nat.Even

因此(Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N证明了这一点Nat.Flip y_aIY ~# Nat.Flip 'Nat.Even.

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

把这些放在一起我们得到(dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0])了类型x_aIX #~ 'Nat.Odd.

第二个更复杂的演员阵容有点难以解决,但应该按照相同的原则工作.