Comment lire cette «preuve» du GHC Core?

Question 1

J'ai écrit ce petit morceau de Haskell pour comprendre comment GHC prouve que pour les nombres naturels, vous ne pouvez que diviser par deux les nombres pairs:

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

Les parties pertinentes du noyau deviennent:

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 }

Je connais le flux général de la conversion des types à travers des instances de la famille de types Flip, mais il y a certaines choses que je ne peux pas suivre complètement:

Quelle est la signification de @~ <Nat.Flip x_apH>_N? est-ce l'instance Flip pour x? En quoi cela diffère- @ (Nat.Flip x_apH)t-il? Je suis à la fois intéressé < >et_N

Concernant le premier casting dans halve:

Que signifient dt_dK6, dt1_dK7et dt2_dK8reposer? Je comprends qu'il s'agit d'une sorte de preuve d'équivalence, mais laquelle est laquelle?
Je comprends que ça Sympasse par une équivalence à l'envers
Que font les ;'s? Les preuves d'équivalence sont-elles simplement appliquées séquentiellement?
Quels sont ces _Net _Rsuffixes?
Sont TFCo:R:Flip[0]et TFCo:R:Flip[1]les instances de Flip?

Question 2

@~ est l'application de la coercition.

Les crochets indiquent une coercition réflexive de leur type contenu avec un rôle donné par la lettre soulignée.

Ainsi <Nat.Flip x_ap0H>_Nest une preuve d'égalité qui Nat.Flip x_apHest égale à Nat.Flip x_apHnominalement (en tant que types égaux et pas seulement des représentations égales).

PS a beaucoup d'arguments. Nous regardons le constructeur intelligent $WPSet nous pouvons voir que les deux premiers sont les types de x et y respectivement. Nous avons la preuve que l'argument constructeur est Flip x(dans ce cas, nous avons Flip x ~ Even. Nous avons alors les preuves x ~ Flip yet y ~ Flip x. L'argument final est une valeur de ParNat x.

Je vais maintenant parcourir le premier casting de type Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd

Nous commençons par (Nat.ParNat ...)_R. Ceci est une application de constructeur de type. Il lève la preuve de x_aIX ~# 'Nat.Oddà Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd. Les Rmoyens dont elle fait ce qui signifie representationally que les types sont isomorphes mais pas le même (dans ce cas , ils sont les mêmes , mais on n'a pas besoin que les connaissances pour effectuer la distribution).

Maintenant, nous regardons le corps principal de la preuve (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]). ;signifie transitivité c'est-à-dire appliquer ces preuves dans l'ordre.

dt1_dK7est une preuve de x_aIX ~# Nat.Flip y_aIY.

Si nous regardons (dt2_dK8 ; Sym dt_dK6). dt2_dK8spectacles y_aIY ~# Nat.Flip x_aIX. dt_dK6est de type 'Nat.Even ~# Nat.Flip x_aIX. Donc Sym dt_dK6est de type Nat.Flip x_aIX ~# 'Nat.Evenet (dt2_dK8 ; Sym dt_dK6)est de typey_aIY ~# 'Nat.Even

C'est donc (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_Nune preuve que Nat.Flip y_aIY ~# Nat.Flip 'Nat.Even.

Nat.TFCo:R:Flip[0]est la première règle de flip qui est Nat.Flip 'Nat.Even ~# 'Nat.Odd'.

En les mettant ensemble, nous obtenons (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0])un type x_aIX #~ 'Nat.Odd.

Le deuxième casting plus compliqué est un peu plus difficile à élaborer mais devrait fonctionner sur le même principe.

Answer 1