如何阅读这个 GHC 核心的“证明”？

我写 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 的实例吗？
1374 次浏览
小开
最佳答案

@~ is coercion application.

The angle brackets denote a reflexive coercion of their contained type with role given by the underscored letter.

Thus <Nat.Flip x_ap0H>_N is an equality proof that Nat.Flip x_apH is equal to Nat.Flip x_apH nominally (as equal types not just equal representations).

PS has a lot of arguments. We look at the smart constructor $WPS and we can see the first two are the types of x and y respectively. We have proof that the constructor argument is Flip x (in this case we have Flip x ~ Even. We then have the proofs x ~ Flip y and y ~ Flip x. The final argument is a value of ParNat x.

I will now walk through the first cast of type Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd

We start with (Nat.ParNat ...)_R. This is a type constructor application. It lifts the proof of x_aIX ~# 'Nat.Odd to Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd. The R means it does this representationally meaning that the types are isomorphic but not the same (in this case they are the same but we don't need that knowledge to perform the cast).

Now we look at main body of the proof (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]). ; means transitivty i.e. apply these proofs in order.

dt1_dK7 is a proof of x_aIX ~# Nat.Flip y_aIY.

If we look at (dt2_dK8 ; Sym dt_dK6). dt2_dK8 shows y_aIY ~# Nat.Flip x_aIX. dt_dK6 is of type 'Nat.Even ~# Nat.Flip x_aIX. So Sym dt_dK6 is of type Nat.Flip x_aIX ~# 'Nat.Even and (dt2_dK8 ; Sym dt_dK6) is of type y_aIY ~# 'Nat.Even

Thus (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N is a proof that Nat.Flip y_aIY ~# Nat.Flip 'Nat.Even.

Nat.TFCo:R:Flip[0] is the first rule of flip which is Nat.Flip 'Nat.Even ~# 'Nat.Odd' .

Putting these together we get (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]) has type x_aIX #~ 'Nat.Odd.

The second more complicated cast is a bit harder to work out but should work on the same principle.


提交答案