¿Cómo leer esta “prueba” de GHC Core?

Question 1

Escribí este pequeño fragmento de Haskell para descubrir cómo GHC demuestra que para los números naturales, solo puedes dividir a la mitad los pares:

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

Las partes relevantes del núcleo se convierten en:

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 }

Conozco el flujo general de conversión de tipos a través de instancias de la familia de tipos Flip, pero hay algunas cosas que no puedo seguir por completo:

¿Cuál es el significado de @~ <Nat.Flip x_apH>_N? ¿Es la instancia de Flip para x? ¿En qué se diferencia eso de @ (Nat.Flip x_apH)? Estoy interesado en < >y_N

Respecto al primer elenco en halve:

¿Qué significan dt_dK6, dt1_dK7y dt2_dK8representan? Entiendo que son una especie de prueba de equivalencia, pero ¿cuál es cuál?
Entiendo que Sympasa por una equivalencia al revés
¿Qué hacen los ;? ¿Las pruebas de equivalencia se aplican de forma secuencial?
¿Qué son estos _Ny los _Rsufijos?
Son TFCo:R:Flip[0]y TFCo:R:Flip[1]las instancias de Flip?

Question 2

@~ es aplicación de coerción.

Los paréntesis angulares denotan una coerción reflexiva de su tipo contenido con el papel dado por la letra subrayada.

Por <Nat.Flip x_ap0H>_Nlo tanto, es una prueba de igualdad que Nat.Flip x_apHes igual a Nat.Flip x_apHnominalmente (como tipos iguales, no solo representaciones iguales).

PD tiene muchos argumentos. Observamos el constructor inteligente $WPSy podemos ver que los dos primeros son los tipos de xey respectivamente. Tenemos la prueba de que el argumento del constructor es Flip x(en este caso tenemos Flip x ~ Even. Luego tenemos las pruebas x ~ Flip yy y ~ Flip x. El argumento final es un valor de ParNat x.

Ahora analizaré el primer elenco de tipos Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd

Empezamos con (Nat.ParNat ...)_R. Esta es una aplicación de constructor de tipos. Levanta la prueba de x_aIX ~# 'Nat.Odda Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd. Los Rmedios lo hace representacionalmente lo que significa que los tipos son isomorfos, pero no es lo mismo (en este caso son los mismos, pero que no es necesario que el conocimiento para llevar a cabo el reparto).

Ahora miramos el cuerpo principal de la prueba (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]). ;significa transitividad, es decir, aplicar estas pruebas en orden.

dt1_dK7es una prueba de x_aIX ~# Nat.Flip y_aIY.

Si miramos (dt2_dK8 ; Sym dt_dK6). dt2_dK8muestra y_aIY ~# Nat.Flip x_aIX. dt_dK6es de tipo 'Nat.Even ~# Nat.Flip x_aIX. Entonces Sym dt_dK6es de tipo Nat.Flip x_aIX ~# 'Nat.Eveny (dt2_dK8 ; Sym dt_dK6)es de tipoy_aIY ~# 'Nat.Even

Así (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_Nes una prueba de eso Nat.Flip y_aIY ~# Nat.Flip 'Nat.Even.

Nat.TFCo:R:Flip[0]es la primera regla del flip que es Nat.Flip 'Nat.Even ~# 'Nat.Odd'.

Poniendo estos juntos tenemos (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0])tipo x_aIX #~ 'Nat.Odd.

El segundo elenco más complicado es un poco más difícil de resolver, pero debería funcionar con el mismo principio.

Answer 1