如何阅读这个 GHC Core 的“证明”？

Question

如何阅读这个 GHC Core 的“证明”？

haskellghcproofhaskell-platformformal-verification

85

我用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的实例吗？

- Mathijs Kwik

6

我不确定，但我的猜测是_N和_R分别代表名义角色和表象角色：http://www.haskell.org/ghc/docs/latest/html/users_guide/roles.html#idp25254608 - chi

访问https://dev59.com/dm025IYBdhLWcg3wQDhb，希望你能得到一个想法。 - Hemant Ramphul

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Alex · Accepted Answer

@~ 是强制应用。

尖括号表示带有下划线字母角色的其包含类型的反身强制。

因此，<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。

第二个更复杂的强制转换可能比较难理解，但应该遵循同样的原则。