Как читать это «доказательство» GHC Core?

Я написал этот небольшой фрагмент Haskell, чтобы выяснить, как GHC доказывает, что для натуральных чисел вы можете уменьшить вдвое только четные:

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

Соответствующие части ядра становятся:

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 }

Я знаю общий поток приведения типов через экземпляры семейства типов Flip, но есть некоторые вещи, которым я не могу полностью следовать:

• В чем смысл @~ <Nat.Flip x_apH>_N? это экземпляр Flip для x? Чем это отличается от @ (Nat.Flip x_apH)? Меня одновременно интересует < >и_N

По поводу первого заброса halve:

• Что делать dt_dK6,dt1_dK7 и на dt2_dK8стенде? Я понимаю, что это какие-то доказательства эквивалентности, но что именно?
• Я это понимаю Sym эквивалентность проходит в обратном направлении
• Что делают ; делают? Применяются ли доказательства эквивалентности последовательно?
• Что это _Nи_R суффиксы?
• Есть TFCo:R:Flip[0]и TFCo:R:Flip[1]экземпляры Flip?

@~ это приложение принуждения.

Угловые скобки обозначают рефлексивное приведение их содержащегося типа с ролью, заданной подчеркнутой буквой.

Таким образом <Nat.Flip x_ap0H>_N, это доказательство равенства, Nat.Flip x_apHкоторое Nat.Flip x_apHноминально равно (как равные типы, а не только равные представления).

PS есть много аргументов. Мы смотрим на интеллектуальный конструктор $WPSи видим, что первые два являются типами x и y соответственно. У нас есть доказательство того, что аргумент конструктора равен Flip x(в данном случае у Flip x ~ Evenнас есть доказательства x ~ Flip yи y ~ Flip x. Последний аргумент - это значение ParNat x.

Теперь я пройдусь по первому типу типа Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd

Начнем с (Nat.ParNat ...)_R. Это приложение-конструктор типов. Это снимает доказательство того, x_aIX ~# 'Nat.Oddчто Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd. Это Rозначает, что типы изоморфны, но не одинаковы (в данном случае они одинаковы, но нам не нужны эти знания для выполнения преобразования).

Теперь посмотрим на основную часть доказательства (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]). ;означает транзитность, т.е. применить эти доказательства по порядку.

dt1_dK7является доказательством x_aIX ~# Nat.Flip y_aIY.

Если мы посмотрим на (dt2_dK8 ; Sym dt_dK6). dt2_dK8показывает y_aIY ~# Nat.Flip x_aIX. dt_dK6типа 'Nat.Even ~# Nat.Flip x_aIX. Так Sym dt_dK6есть типа Nat.Flip x_aIX ~# 'Nat.Evenи (dt2_dK8 ; Sym dt_dK6)типаy_aIY ~# 'Nat.Even

Таким образом , (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_Nявляется доказательством того, что Nat.Flip y_aIY ~# Nat.Flip 'Nat.Even.

Nat.TFCo:R:Flip[0]это первое правило флип, которое есть Nat.Flip 'Nat.Even ~# 'Nat.Odd'.

Собирая их вместе, мы получаем (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0])шрифт x_aIX #~ 'Nat.Odd.

Второе, более сложное приведение немного сложнее, но оно должно работать по тому же принципу.