日々の流転

λ. “Generic Programming with Adjunctions” by Ralf Hinze

2010-04-24 の Functional Programming Meeting 2010で紹介されていたもの。

Ψ : Nat(C(-,A), C(F-,A)) が与えらたときに、x ∘ in = Ψ x を満たす一意な x = (|Ψ|)_Id : μF→A が、Mendler-style fold (Mendler-style catamorphism) 。

これを拡張し、随伴 L ⊣ R と Ψ : Nat(C(L-,A), C(L(F-),A)) が与えられたときに、x ∘ L(in) = Ψx を満たす一意な x = (|Ψ|)_L : L(μF) → A を定義し、これを Adjoint fold と呼んでいる。 これは、随伴を Φ: C(LA, B) → D(A, RB) とすると、(|Ψ|)_L = Φ^-1 (|Φ ∘ Ψ ∘ Φ^-1 |)_Id という風に通常の Mendler-style fold に還元できる。

Adjoint fold の良いところは、引数にμFが直接現れずにコンテキストの中に現れているような再帰関数でも、そのコンテキストを表す関手が右随伴を持てば扱えること。 例えば、

append :: ([a], [a]) → [a]
append ([], ys) = ys
append (x:xs, ys) = x : (append xs ys)

を考えると、F(X) = Maybe (A, X) とおいて μF ≅ [a] で、L(X) = (X, μF) は右随伴 R(X) = (μF ⇒ X) を持つので、

Ψ : ∀X. (LX → μF) → (LFx → μF)
Ψ f (Nothing, ys) = ys
Ψ f (Just (a,x), ys) = a : f (x,ys)

append : (μF,μF) → μF
append = (|Ψ|)_L

という風に、Adjoint fold の形で書ける。

Fusion for adjoint folds から Type fusion へのつながりがイマイチよく分からなかった。 Fusion for adjoint folds が α(|Ψ|)_L = (|Ψ'|)_L' ⇐ α∘Ψ = Ψ'∘α なのに対して、 Type fusion が L(μF) ≅ μG ⇐ L∘F ≅ G∘L と、 νF ≅ R(νG) ⇐ F∘R ≅ R∘G で、 同じ形になっているのは分かるし、後者の証明に前者が使えるのもわかるのだけど、形の上での類似性だけで本質的な関係が何かあったりしないのだろうか?

Type fusion の証明は、以下で十分なのではないかと思った。 swap : L∘F ≅ G∘L が与えれているとき、ψ: GB→B に対して、Ψ ∈ Nat(C(L-,B), C(LF-, B)) を、Ψ(h) = ψ ∘ Gh ∘ swap とおくと、(|Ψ|)_L : LμF → B は h ∘ Lin_F = ψ ∘ Gh ∘ swap すなわち h ∘ Lin_F ∘ swap^-1 = ψ ∘ Gh を満たす一意な射なので、Lin_F ∘ swap^-1 は G の initial algebra 。

Type fusion を利用してのメモ化の導出も面白かった。

参考

• Categorical programming with inductive and coinductive types - ヒビルテ(2004-06-29)