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

Question

Я написал этот маленький кусочек 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 } 

I знают общий поток литья типов через экземпляры семейства типа 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?

Answer 1

@~ - применение при принуждении.

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

Таким образом, <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 означает, что он делает это representationally означает, что типы изоморфны, но не то же самое (в этом случае они одинаковы но нам не нужны эти знания для выполнения броска).

Теперь мы рассмотрим основной корпус доказательства (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.

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