[解決済み] GHC Coreの "証明 "をどう読むか？

質問

私はこの小さな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)

coreの該当部分がなる。

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のインスタンスですか？

どのように解決するには？

@~ は強制適用です。

角括弧はその中に含まれる型の再帰的強制を表し、ロールは下線付きの文字で与えられる。

したがって <Nat.Flip x_ap0H>_N が等号であることの証明であり Nat.Flip x_apH とは等しい。 Nat.Flip x_apH と名目上等しくなります（等しい表現だけでなく、等しい型として）。

PSには多くの引数があります。私たちはスマートなコンストラクタである $WPS を見てみると、最初の 2 つはそれぞれ 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 .

2つ目のより複雑なキャストは少し難しいですが、同じ原理で動作するはずです。