Comment lire cette «preuve» GHC Core?

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

{-# 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 kernel deviennent:

 Nat.$WPZ :: Nat.ParNat 'Nat.Even Nat.$WPZ = Nat.PZ @ '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 @~ _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 stream général de transtypage des types par le biais d’instances de la famille de type Flip, mais il y a certaines choses que je ne peux pas suivre complètement:

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

En ce qui concerne la première dissortingbution en halve :

  • Que dt_dK6 , dt1_dK7 et dt2_dK8 ? Je comprends qu’ils sont une sorte de preuves d’équivalence, mais qui est qui?
  • Je comprends que Sym traverse une équivalence à l’envers
  • Qu’est-ce que le est-ce le cas? Les preuves d’équivalence sont-elles simplement appliquées séquentiellement?
  • Quels sont ces suffixes _N et _R ?
  • Sont TFCo:R:Flip[0] et TFCo:R:Flip[1] les instances de Flip?

@~ est une application de coercition.

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

Ainsi, _N est une preuve d’égalité que Nat.Flip x_apH est égal à Nat.Flip x_apH (en tant que types égaux et pas seulement des représentations égales).

PS a beaucoup d’arguments. Nous examinons le constructeur intelligent $WPS et 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 y et 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 soulève la preuve de x_aIX ~# 'Nat.Odd à Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd . Le R signifie qu’il fait cela de manière représentative, ce qui signifie que les types sont isomorphes mais pas les mêmes (dans ce cas, ils sont identiques mais nous n’avons pas besoin de cette connaissance pour effectuer le transtypage).

Nous examinons maintenant le corps principal de la preuve (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]) . ; signifie transitivty c’est-à-dire appliquer ces preuves dans l’ordre.

dt1_dK7 est une preuve de x_aIX ~# Nat.Flip y_aIY .

Si nous regardons (dt2_dK8 ; Sym dt_dK6) . dt2_dK8 montre y_aIY ~# Nat.Flip x_aIX . dt_dK6 est de type 'Nat.Even ~# Nat.Flip x_aIX . Donc, Sym dt_dK6 est de type Nat.Flip x_aIX ~# 'Nat.Even et (dt2_dK8 ; Sym dt_dK6) est de type y_aIY ~# 'Nat.Even

Ainsi, (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N est une 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' .

Ensemble, nous obtenons (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]) a le type x_aIX #~ 'Nat.Odd .

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