😊

日常のプログラミングに圏論を応用する - 代数的データ型とVisitorパターンの同型性

2023/10/13に公開

代数的データ型の重要性は広く知られている（と思う）が、一般に使われるプログラミング言語にはまだまだ浸透していない。
代数的データ型で物事を考える習慣がつくと、これをサポートしない言語で仕事をするのはフラストレーションが溜まる。
幸いなことに、代数的データ型を直接にはサポートしない言語でも、代数的データ型と“実質同じ”型を定義する方法がある。
本記事では、代数的データ型の比較的シンプルな例を取り上げて、それを定義する方法と、それが上手くいく圏論的な理由を簡単に紹介する。

サンプル言語はTypeScript^[1]だが、総称型（ジェネリクス）をサポートする言語であれば上手くコード化できるはずである。

Maybe型

代数的データ型のシンプルな例として、今回は Maybe を取り上げたい。
任意の型 T について、型 Maybe<T> とは、値が“ない”ことを示す値 Nothing か、値 t: T が“ある”ことを示す値 Just(t) を持つ型である。
null参照の発明は10億ドルに相当する誤りだったとする話は有名であるが、この問題に対処する方法の1つが Maybe<T> 型を使うこと^[2]である。

このように値がAかもしれないしBかもしれないというような複数の可能性を持つ型を考えたいときは代数的データ型の出番である。
例えばHaskellでは以下のように定義できる。

data Maybe a = Nothing | Just a

記号 | は“または”と読むと良い。
しかし、プログラミング言語で“または”を表せる型システムを持つものは多くはない。
そこで、10億ドルの損失を未然に防ぐためにも、これを代替する方法が望まれる。

Visitorパターン

実は、代数的データ型に相当するオブジェクト指向的な概念は昔から良く知られていた。
これをVisitorパターンと言う。
Visitorパターンはデータの訪問者 DataVisitor<R> と、それを受け入れるデータ Data の2つから構成されるパターンである。

interface IDataVisitor<R> { /* ... */ }
interface IData { /* ... */ }

今回は Maybe<T> 型について考えているので、これにVisitorパターンを適用するということは、以下の2つのインターフェース IMaybeVisitor<T, R> と IMaybe<T> を定義することに相当する。

interface IMaybeVisitor<T, R> { /* ... */ }
interface IMaybe<T> { /* ... */ }

まず、IMaybeVisitor<T, R> は Maybe<T> 値を“訪問”し、何らかの結果である R 値を返す役割を持つ。
訪問者が Maybe<T> 値を訪問するときには2つの可能性がある。
1つはそれが値 Nothing である場合、もう1つはそれが値 Just(value) である場合である。
訪問者はあり得るすべての場合に対応できなければならない。
つまり、それぞれの場合について R 値を返すアルゴリズムを持っていなければならない。

Nothing 値のときに何らかの R 値を返すメソッドを visitNothing、Just(value) 値のときに R 値を返すメソッドを visitJust と命名すると、IMaybeVisitor<T, R> は以下のようなインターフェースとなる。

interface IMaybeVisitor<T, R> {
  visitNothing: R;
  visitJust(value: T): R;
}

次に、データ IMaybe<T> を定義する。
このデータは先ほど定義した訪問者 IMaybeVisitor<T, R> を受け入れて、訪問者が作成した結果をそのまま返す。
ここで重要な条件として、データは訪問者を選り好みしないというものがある。
つまり、IMaybeVisitor<T, string> であろうと IMaybe<T, IMaybe<number>> であろうと、データ IMaybe<T> は任意の R について訪問者 IMaybeVisitor<T, R> を受け入れるということだ。
このことはジェネリクスを用いて表すことができ、IMaybe<T> は以下のようなインターフェースとなる。

interface IMaybe<T> {
  accept<R>(visitor: IMaybeVisitor<T, R>): R;
}

ここでのポイントは、IMaybe<T> は型 R に依存しないということである。
R のジェネリック性は IMaybe<T> 型に宿るのではなく、accept メソッドに宿る。

後は IMaybe<T> を実装する具体的なクラスである Just や Nothing を定義して使うだけである。

class Nothing<T> implements IMaybe<T> {
  accept<R>(visitor: IMaybeVisitor<T, R>): R {
    return visitor.visitNothing;
  }
}

class Just<T> implements IMaybe<T> {
  constructor(readonly value: T) {}
  accept<R>(visitor: IMaybeVisitor<T, R>): R {
    return visitor.visitJust(value);
  }
}

圏論的説明

ここからが本記事の主題である。
なぜこの方法が上手くいくのか？
他の代数的データ型にもVisitorパターンは通用するのか？
この手の現象を説明するときは圏論の力を借りるとシンプルに上手くいく。

米田の補題により、共変ホム関手 $\mathrm{Hom}(a, -)$ から $F$ への自然変換と $F \; a$ の要素は一対一に対応する。
ここで $F$ を恒等関手とすると話は単純になる。

上記はTypeScript的に言えばジェネリクスを伴う関数の型 <R>((k: (a: A) => R) => R) と A が“実質同じ”型であるという主張に相当する。
このようなジェネリック関数を、記号 $\forall$ を用いて $\forall R. (A \to R) \to R$ と書くことにする。
これは「任意の型 $R$ について $(A \to R) \to R$ 」と読む。

“実質同じ”というのは過不足なく代替可能であるという意味である。
全く同じというわけではないので、等号 $=$ を使う代わりに記号 $\cong$ を使うことにしよう。
すると、簡単な式変形^[3]により、代替可能な型同士の関係を明らかにすることができる。

\begin{aligned} \mathrm{Maybe} \; T &\cong 1 + T \\ &\cong \forall R. ((1 + T) \to R) \to R \\ &\cong \forall R. (R^{1 + T}) \to R \\ &\cong \forall R. (R^1 \times R^T) \to R \\ &\cong \forall R. (R \times (T \to R)) \to R \\ \end{aligned}

お気づきいただけただろうか？
$R \times (T \to R)$ というのはまさに先ほど定義した IMaybeVisitor<T, R> のことである。
したがって、最終行は IMaybe<T> を表している。

つまり、代数的データ型とそのVisitorパターンによる型が事実上同一であることは圏論的に説明される。

圏論を日常のプログラミングに応用する

このことは抽象的で手の届かない存在のように思える圏論を、身近なプログラミングに応用する方法の1つを提示しているようだ。
代数的データ型をサポートしないプログラミング言語を使っているときにどうしても和の型が必要になった場合には、圏論に訴えかけると良い。

$A$ が代数的データ型のとき、これはいくつかの型の和として表されている。

data A = A1
       | A2
       ...
       | An

しかし、和を直接的に表す方法がそのプログラミング言語にはないとする。
そんなときは米田の補題を使って型の表現方法を変えてしまえば良い。
$A$ と $\forall R. R^A \to R$ は同型である。
指数の和 $R^A$ は累乗の積に変換できるので、以下のような同型性が導かれる。

A \cong \forall R. ((A_{1} \to R) \times (A_{2} \to R) \times \cdots \times (A_{n} \to R)) \to R

多くのプログラミング言語は積の型やジェネリクスをサポートするので、これにより代数的データ型をエンコードできる。
圏論の応用対象は関数型プログラミングだけではなく、プログラミング全般である。

脚注

ただし、TypeScriptはタグ付きユニオンをサポートしているため、Visitorパターンに頼らずに代数的データ型を表すことができる。サンプル言語にTypeScriptを選んだのは、あらゆるアプリケーションはJavaScriptで書かれる運命にあるからである。 ↩︎
ただし、TypeScriptでは null や undefined を型システムで追跡できるので、敢えて Maybe 型を導入する意義は薄い。 ↩︎
関数の型 $A \to B$ を累乗 $B^A$ と見なし、あたかも通常の数の計算のように式変形することは圏論的に正当化される。 ↩︎

GitHubで編集を提案

Maybe型

Visitorパターン

圏論的説明

圏論を日常のプログラミングに応用する

Discussion