如何阅读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是什么意思？ 它是x的Flip实例吗？ 这与@ (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 x_aIX ~# Nat.ParNat 'Nat.Odd
我们从(Nat.ParNat ...)_R 。 这是一个类型构造器应用程序。 它将x_aIX ~# 'Nat.Odd的证明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'的第一个翻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 。
第二个更复杂的演员有点难，但应该按照相同的原则工作。
链接地址: http://www.djcxy.com/p/5699.html