haskell - ¿Cómo leer este GHC Core "prueba"?

proof haskell-platform

Question

Escribí esta pequeña parte de Haskell para descubrir cómo GHC demuestra que para los números naturales, solo puedes reducir 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 tipo Flip, pero hay algunas cosas que no puedo seguir completamente:

• ¿Cuál es el significado de @~ <Nat.Flip x_apH>_N ? ¿Es la instancia de Flip para x? ¿Cómo difiere eso de @ (Nat.Flip x_apH) ? Estoy interesado en < > y _N

En cuanto al primer reparto en la halve :

• ¿Qué significan dt_dK6 , dt1_dK7 y dt2_dK8 ? Entiendo que son algún tipo de pruebas de equivalencia, pero ¿cuál es cuál?
• Entiendo que Sym ejecuta una equivalencia al revés
• Que hace el ; Qué hacer? ¿Las pruebas de equivalencia se aplican secuencialmente?
• ¿Cuáles son estos sufijos _N y _R ?
• ¿Son TFCo:R:Flip[0] y TFCo:R:Flip[1] las instancias de Flip?

Answer 1

@~ es una aplicación de coerción.

Los corchetes angulares denotan una coacción reflexiva de su tipo contenido con el papel dado por la letra subrayada.

Por lo tanto, <Nat.Flip x_ap0H>_N es una prueba de igualdad de que Nat.Flip x_apH es igual a Nat.Flip x_apH nominal (como tipos iguales, no solo representaciones iguales).

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

Ahora caminaré a través del primer elenco del tipo Nat.ParNat x_aIX ~# Nat.ParNat ''Nat.Odd

Comenzamos con (Nat.ParNat ...)_R Esta es una aplicación de constructor de tipo. Levanta la prueba de x_aIX ~# ''Nat.Odd a Nat.ParNat x_aIX ~# Nat.ParNat ''Nat.Odd . La R significa que representa esto representacionalmente, lo que significa que los tipos son isomorfos pero no iguales (en este caso son los mismos, pero no necesitamos ese conocimiento para realizar 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_dK7 es una prueba de x_aIX ~# Nat.Flip y_aIY .

Si miramos (dt2_dK8 ; Sym dt_dK6) . dt2_dK8 muestra y_aIY ~# Nat.Flip x_aIX . dt_dK6 es del tipo ''Nat.Even ~# Nat.Flip x_aIX . Entonces Sym dt_dK6 es del tipo Nat.Flip x_aIX ~# ''Nat.Even y (dt2_dK8 ; Sym dt_dK6) es de tipo y_aIY ~# ''Nat.Even

Por lo tanto, (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N es una prueba de que Nat.Flip y_aIY ~# Nat.Flip ''Nat.Even .

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

Poniéndolos juntos, obtenemos (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]) tiene el tipo x_aIX #~ ''Nat.Odd .

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