Jak czytać ten „dowód” GHC Core?

Question 1

Napisałem ten mały fragment Haskella, aby dowiedzieć się, jak GHC udowadnia, że w przypadku liczb naturalnych można zmniejszyć o połowę tylko te parzyste:

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

Odpowiednie części rdzenia stają się:

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 }

Znam ogólny przebieg rzutowania typów przez instancje z rodziny Flip, ale jest kilka rzeczy, których nie mogę całkowicie zrozumieć:

Co to ma znaczyć @~ <Nat.Flip x_apH>_N? czy jest to instancja Flip dla x? Czym to się różni @ (Nat.Flip x_apH)? Jestem zainteresowany < >i_N

Odnośnie pierwszej obsady w halve:

Czego dt_dK6, dt1_dK7a dt2_dK8skrót? Rozumiem, że są to jakieś dowody równoważności, ale który jest który?
Rozumiem, że Symprowadzi to przez równoważność wstecz
Co ;robią? Czy dowody równoważności są po prostu stosowane sekwencyjnie?
Co to jest _Ni _Rsufiksy?
Czy TFCo:R:Flip[0]i TFCo:R:Flip[1]przypadki Flip?

Question 2

@~ to zastosowanie przymusu.

Nawiasy kątowe oznaczają odruchowy wymuszenie ich typu zawartego z rolą nadaną przez podkreśloną literę.

Tak więc <Nat.Flip x_ap0H>_Njest dowód równości, który Nat.Flip x_apHjest równy Nat.Flip x_apHnominalnie (jako równe typy, a nie tylko równe reprezentacje).

PS ma wiele argumentów. Patrzymy na inteligentnego konstruktora $WPSi widzimy, że pierwsze dwa to typy odpowiednio x i y. Mamy dowód, że argument konstruktora to Flip x(w tym przypadku mamy Flip x ~ Even. Mamy wtedy dowody x ~ Flip yi y ~ Flip x. Ostatnim argumentem jest wartość ParNat x.

Przejdę teraz przez pierwszą obsadę czcionek Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd

Zaczynamy od (Nat.ParNat ...)_R. To jest aplikacja do konstruowania typów. Podnosi dowód x_aIX ~# 'Nat.Oddna Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd. Te Rśrodki to robi to reprezentatywny i oznacza, że typy są izomorficzne, ale nie takie same (w tym przypadku są one takie same, ale nie potrzebujemy tej wiedzy, aby wykonać odlew).

Teraz przyjrzymy się głównej części dowodu (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]). ;oznacza przejściowość, tj. zastosuj te dowody w kolejności.

dt1_dK7jest dowodem x_aIX ~# Nat.Flip y_aIY.

Jeśli spojrzymy na (dt2_dK8 ; Sym dt_dK6). dt2_dK8pokazuje y_aIY ~# Nat.Flip x_aIX. dt_dK6jest typu 'Nat.Even ~# Nat.Flip x_aIX. Więc Sym dt_dK6jest typu Nat.Flip x_aIX ~# 'Nat.Eveni (dt2_dK8 ; Sym dt_dK6)jest typuy_aIY ~# 'Nat.Even

Tak więc (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_Njest to dowód, że Nat.Flip y_aIY ~# Nat.Flip 'Nat.Even.

Nat.TFCo:R:Flip[0]jest pierwszą zasadą przewrotu, która jest Nat.Flip 'Nat.Even ~# 'Nat.Odd'.

Łącząc je razem, otrzymujemy (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0])typ x_aIX #~ 'Nat.Odd.

Druga, bardziej skomplikowana obsada jest nieco trudniejsza do wykonania, ale powinna działać na tej samej zasadzie.