型と関数の圏におけるカリー化

2022.07.27

はじめに

引き続きCategory Theory for ProgrammersをScalaで書き下していきます。

プログラミングにおける型とその値を集合と考えると別の型の集合に対する射の全体もまた集合(Hom集合)です。型の集合とHom集合が同じ集合に含まれるような圏を考えます。

関数の集合から任意の関数zそれに対する引数aおよび関数の戻り値b を任意に取り、積 z×aからbへの射g (𝑔∷𝑧×𝑎→𝑏) を考えます。普遍的構成によってzから ユニークな射h (h ∷ 𝑧 → (𝑎 ⇒ 𝑏) )をもつ対象 を(a ⇒ b)と呼び、次のような射evalを伴います。

𝑔 ∷ 𝑧×𝑎 → 𝑏
h ∷ 𝑧 → (𝑎 ⇒ 𝑏)
𝑒𝑣𝑎𝑙 ∷ ((𝑎 ⇒ 𝑏) × 𝑎) → 𝑏

これによってg は以下のように分解できます。

𝑔 = 𝑒𝑣𝑎𝑙 ∘ (h × id)

これは2引数の関数から「1つの引数を取って関数を返す関数」への変換(カリー化)に対応します。上記で示されているようにgをhとevalを使って構成できることをScalaで確かめてみます。

Scalaでのカリー化

type F[A, B] = A => B

// 𝑔 ∷ 𝑧×𝑎 → 𝑏
def g[A, B, C, D](z: F[C, D], a: A): B = ???
// h ∷ 𝑧 → (𝑎 ⇒ 𝑏)
def h[A, B, C, D](z: F[C, D]): (A => B) = ???
// 𝑒𝑣𝑎𝑙 ∷ ((𝑎 ⇒ 𝑏) × 𝑎) → 𝑏
def eval[A, B](f: A => B, a: A): B = ???
// 𝑔 = 𝑒𝑣𝑎𝑙 ∘ (h × id)
def g2[A, B, C, D](z: F[C, D], a: A): B = eval(h(z), identity(a))

g,hおよびevalの具体的な実装は避けましたがこれらを使って同様のシグネチャの関数 g2を構成することができました。