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

2022.07.27

この記事は公開されてから1年以上経過しています。情報が古い可能性がありますので、ご注意ください。

はじめに

引き続き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を構成することができました。