How to read this GHC Core "proof"?
I wrote this small bit of Haskell to figure out how GHC proves that for natural numbers, you can only halve the even ones:
{-# 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)
The relevant parts of core become:
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 know the general flow of casting the types through instances of the Flip type family, but there are some things that I cannot completely follow:
- What's the meaning of
@~ <Nat.Flip x_apH>_N
? is it the Flip instance for x? How does that differ from@ (Nat.Flip x_apH)
? I'm both interested in< >
and_N
Regarding the first cast in halve
:
- What do
dt_dK6
,dt1_dK7
anddt2_dK8
stand for? I understand they are some kind of equivalence proofs, but which is which? - I understand that
Sym
runs through an equivalence backwards - What do the
;
's do? Are the equivalence proofs just applied sequentially? - What are these
_N
and_R
suffixes? - Are
TFCo:R:Flip[0]
andTFCo:R:Flip[1]
the instances of Flip?
@~
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.