이 GHC 핵심 "증거"를 읽는 방법?

이 GHC 핵심 "증거"를 읽는 방법?

---

나는 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등가를 거꾸로 통과 한다는 것을 이해합니다.
• What do the ;'s do? Are the equivalence proofs just applied sequentially?
• What are these _N and _R suffixes?
• Are TFCo:R:Flip[0] and TFCo: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.

참고URL : https://stackoverflow.com/questions/26524223/how-to-read-this-ghc-core-proof