日々の流転

λ. 米田の補題とCPS変換

檜山さんのところで米田の補題とCPS変換の関係の話が紹介されていた。まだ読んでいないのだけど、多分こういう話だろうと思うので、読む前にちょっとメモ。

「locally-small な圏 C、関手 F : C→Set、対象 A∈|C| について自然同型 Nat(hom(A,-), F) ≅ FA が成り立つ」というのが米田の補題。 ところで、自然変換と多相関数は似たようなものなので、これを多相ラムダ計算の型で書くと、大体 ∀X. (A→X)→FX ≅ FA となる。 ここで、Fとして恒等関手を用いると ∀X. (A→X)→X ≅ A となり、同型は以下のΦとΨによって表現される。

id : ∀X. X → X
id = ΛX. λx:X. x

Φ : (∀X. (A→X) → X) → A
Φ = λα:(∀X. (A→X) → X). α A (id A)

Ψ : A → (∀X. (A→X) → X)
Ψ = λa:A. ΛX. λk:A→X. k a

これはまさにある種のCPS変換になっている。

これが同型であることを多相ラムダ計算で示すには、通常の簡約規則と関数の外延性だけでは不十分で、パラメトリシティが必要になる(証明は Theorems for free! (20050218#p03) を参照)。 また、元の ∀X. (A→X)→FX ≅ FA も同様にパラメトリシティを用いて証明可能。→ 米田の補題と多相ラムダ計算

【2009-07-15 追記】 CPS A = (∀X. (A→X) → X) とおくことにする。 型 A と型 CPS A が同型なわけだけど、そうすると A→B と CPS A → CPS B も同型対応するようになる。

Φ' : (CPS A → CPS B) → (A→B)
Φ' = λg : CPS A → CPS B. λa : A. Φ (g (Ψ a))
    = λg : CPS A → CPS B. λa : A. (g (ΛX. λk:A→X. k a)) B (id B)

Ψ' : (A→B) → (CPS A → CPS B)
Ψ' = Ψ (f (Φ α))
    = λf : A → B. λα : CPS A. ΛX. λk : B→X. α (λa : A. k (f a))

ついでにHaskellで書いておく。

{-# LANGUAGE RankNTypes #-}

type CPS a = forall x. (a -> x) -> x

-- 値のCPS変換
psi :: a -> CPS a
psi a = \k -> k a

phi :: CPS a -> a
phi x = x id

-- 関数のCPS変換
psi' :: (a -> b) -> (CPS a -> CPS b)
psi' f = \x k -> x (k . f)

phi' :: (CPS a -> CPS b) -> (a -> b)
phi' g = \a -> g (\k -> k a) id