実装言語に依存しないプログラミング

私を含めほとんどの人はお気に入りのプログラミング言語がいくつかあって、その言語での記法をベースにプログラムを考えることが多いと思う。
例えば、整数のリストを表現するとき、JavaScriptに慣れている人は数値の配列 [1, 2, 3] が思い浮かび、C#に慣れている人は new List<int>() {1, 2, 3} が思い浮かぶ。
これらの表現は整数のリストという概念的存在を、どのように0と1のバイナリで表してメモリに格納するか？というような実装上の詳細とセットだ。
現にC#の例では整数を、符号付き32ビット整数 int として実装するところまで決めさせられている。
このような実装の詳細は計算効率に関わってくるので、どのようなデータ構造を選ぶかはもちろん重要である。
しかし、実装段階であればともかく、草案を練っている段階で実装の詳細を指定するのは面倒だと感じる場面が出てきた。^[1]
検討段階では単に概念的なリストを扱いたいだけであり、例えば要素を末尾に追加するのに $O(n)$ かかったり、要素の重複チェックに $O(n^2)$ かかったりするとして、それは些末な問題である。
そのリストに対して行いたい操作が決まった後でデータ構造を検討すればよいだけだからだ。
検討段階でプログラミング言語を使ってプログラムを書いても良いのだが、途中でデータ構造が変わると大抵の場合インターフェースも変わるので、プログラムの書き直しが必要になって面倒である。

言語としての数学

数学と言うと計算をさせられたり、定規とコンパスを使って作図をさせられたりというイメージがあるかもしれない。
ここでいう数学とは、論理学と集合論のことだ。
論理学と集合論は、静的型検査を行ってくれるコンパイラが存在しない頃から知られており、人間にも扱いやすいように設計されている。

先ほどのリストの例で言うと、数学においてはそのような概念を列と呼ぶ。
例えば、数の列は数列と呼ぶ。列は集合論においては単なる関数である。^[2]
JavaScriptの例で言うと、["Apple", "Banana", "Cherry"] は各インデックス i に対して文字列を割り当てる関数と見なせる。

$$\begin{bmatrix} &0 &\mapsto &\mathtt{“Apple”} &\\ &1 &\mapsto &\mathtt{“Banana”} &\\ &2 &\mapsto &\mathtt{“Cherry”} &\\ \end{bmatrix}$$

定義域は $\{0, 1, 2\}$ である。

文字列全体の集合を $\mathtt{String}$ とすると、配列の長さ $3$ である文字列の配列全体の集合は $\{0, 1, 2\} \to \mathtt{String}$ と書ける。

一般に、配列の長さ $N$ である $X$ の配列全体は $\{0,\ldots,N-1\} \to X$ と表せる。

非負整数全体の集合を $\mathbb{N} = \{0, 1, \ldots, \}$ とすると、$X$ の無限列（例えば遅延リスト）は $\mathbb{N} \to X$ の要素として表せる。

JavaScriptでは範囲外のインデックスを指定すると undefined を返す。
この要領で、$X$ の有限列（長さ不定）を $\mathbb{N} \to X \cup \{\mathtt{undefined}\}$ で表すことができる。

タプル (42, "Alice") （JavaScriptでは [42, "Alice"]）は順序対 $\langle 42, \mathtt{“Alice”} \rangle$ として表せる。
第一成分が整数、第二成分が文字列である順序対全体の集合を $\mathbb{Z} \times \mathtt{String}$ と表す。

これも配列と同様で、

$$\begin{bmatrix} &1 &\mapsto &42 &\\ &2 &\mapsto &\mathtt{“Alice”} &\\ \end{bmatrix}$$

と書くことができる。
余域が引数に応じて変わることを除けばこれも単なる関数として見なせる。^[3]

インデックスの集合は $\mathbb{N}$ やその部分集合に限らない。
特定の文字列の有限集合をインデックスの集合とすれば構造体やレコード、プレーンオブジェクトなどと呼ばれるデータ構造を模すことができる。

{
    id: 42,
    name: "Alice"
}

$$\begin{bmatrix} &\mathtt{“id”} &\mapsto &42 &\\ &\mathtt{“name”} &\mapsto &\mathtt{“Alice”} &\\ \end{bmatrix}$$

では、id が正の整数で name が文字列であるようなオブジェクトの集合はどのようにして表せるだろうか？
正の整数全体の集合を $\mathbb{N}^{+}$ とする。
この問いに対しては、集合の内包表記を使うことで答えることができる。

$$\left\{ \begin{bmatrix} &\mathtt{“id”} &\mapsto &x &\\ &\mathtt{“name”} &\mapsto &y &\\ \end{bmatrix} \mid x \in \mathbb{N}^{+} \land y \in \mathtt{String} \right\}$$

ここで説明した関数の概念を使うと、配列、リスト（有限、無限）、タプル、連想配列、構造体、レコード、プレーンオブジェクト、辞書などを表すことができる。
実装上の詳細を捨象してしまえば、これらはすべて単なる関数である。

代数的データ

もちろん、これだけでは物足りない。
成功するかもしれないし失敗するかもしれない結果を、あるプログラミング言語では例外機構（try-catch）を使って記述する。
Haskellのような言語では Either 型を使うかもしれない。

これを記述するには、関数としての構造体の記法を借用し、そこにタグを付けるのが最も簡便だ。
整数をHTTP経由で取得するような処理を想定しよう。

$$\begin{bmatrix} &\mathtt{“type”} &\mapsto &\mathtt{“Success”} &\\ &\mathtt{“payload”} &\mapsto &42 &\\ \end{bmatrix}$$

$$\begin{bmatrix} &\mathtt{“type”} &\mapsto &\mathtt{“Failure”} &\\ &\mathtt{“error”} &\mapsto &\mathtt{“404 Not Found”} &\\ \end{bmatrix}$$

このような値全体の集合は次のように書ける。

$$\left\{ \begin{bmatrix} &\mathtt{“type”} &\mapsto &\mathtt{“Success”} &\\ &\mathtt{“payload”} &\mapsto &x &\\ \end{bmatrix} \mid x \in \mathbb{Z} \right\} \cup \left\{ \begin{bmatrix} &\mathtt{“type”} &\mapsto &\mathtt{“Failure”} &\\ &\mathtt{“error”} &\mapsto &y &\\ \end{bmatrix} \mid y \in \mathtt{String} \right\}$$

Haskellのような言語ではそのまま素直に実装できるし、TypeScriptのような言語であればタグ付きユニオンとして実装すればよい。
実装に際して言語的なサポートが得られない場合は、次のように単なる構造体として実装するかもしれない。（精度は下がる）

$$\left\{ \begin{bmatrix} &\mathtt{“type”} &\mapsto &t &\\ &\mathtt{“payload”} &\mapsto &x &\\ &\mathtt{“error”} &\mapsto &y &\\ \end{bmatrix} \mid t \in \{\mathtt{Success}, \mathtt{Failure}\} \land x \in \mathbb{Z} \cup \{\mathtt{undefined}\} \land y \in \mathtt{String} \cup \{\mathtt{undefined}\} \right\}$$

また、代数的データを記述できるので、そのままThe Elm Architectureのような有限機械を記述することができる。

実装の詳細を省略する

プログラミング言語では計算のステップを逐一記述しなくてはならない。
これはプログラムがコンピュータによって実行されるためには必要なことであるが、一々計算方法を記述しなくてはならないのは煩わしい。
例えば、配列 arr があるとき、その配列に要素 0 が含まれるかどうかを判定し、それに応じて処理が変わるとしよう。
このとき、プログラミング言語ではコレクションの各要素を反復する foreach 文（JavaScriptでは for ... of 文）を使うのが普通だが、これは要素を走査する順番が暗黙の内に決定される。

論理学にはこの手の記述をするための便利な記法 $\exists$ がある。
$\exists i \in \mathbb{N}.\space \mathtt{arr}[i] = 0$ と書くと、これは真偽を表す文で、arr が要素 0 を持つときに真、それ以外のときに偽となる。
この文は arr の各要素をどのような順番で検査するかについて何も述べない。
単に要素があるかどうかだけを記述している。
実装の際に改めて線形探索するか二分探索するかを決めればよい。

徹底的に実装を捨象した思考をするためには数学的記法を使うのがよい。
ここまではデータ構造、特にコレクションの実装についての捨象を主に述べてきた。
実装を捨象する思考は、実装が特定の技術に依存するときには更に有効になってくる。
例えばHTTP通信で何らかのデータを取得してくるというような処理を考えてみよう。
これはまさに実装の捨象が有効に働く例であると思う。

リクエストはJSONかもしれないしXMLかもしれないが、それは（構造体のような）数学における単なる関数で表すことができる。
レスポンスも同様にJSONかXMLで返ってくるとして、これは成功するかもしれないし失敗するかもしれない。
これはまさに代数的データとして表すのがよい。
HTTP通信の部分は捨象してしまえばよい。例えば、クライアントサイドのJavaScriptでブラウザ標準の fetch APIを使うのか、古式ゆかしき XHR を使うのか、はたまた axiom のようなライブラリを使うのかは些末な問題である。
リクエストの集合とレスポンス（失敗する可能性を含む）の集合が決まれば、HTTP通信はそれらの単なる関数として抽象化できる。
レスポンスは失敗する可能性があるので、例えばステータスコードを見てリトライすることになったとしよう。
この場合、HTTP通信の細かいロジックを実装する前にリトライのロジックを確立させたいかもしれない。

パフォーマンスに厳しい要件が無い限り、実装の詳細はできる限り省略し、まずは草案を完成させたい。
実装の詳細を捨象した数学的記述から、AIか何かが実行効率を忖度してプログラムを自動生成してくれれば一番良いのだが、そのような技術の存在を私は知らない。

脚注

1. プログラミング言語で草案を書くとそれはそのまま動くプロトタイプになるのだが、プロトタイプを作るのには時間がかかりすぎる。かといって、草案を記述しないことにはその仕様・設計で十分であるかどうかを検討する術がない。

2. そして、関数は集合論においては単なる集合である。

3. このような関数を依存関数と言う。依存関数の型を扱うことができるプログラミング言語も存在する。