プログラミング言語の関数が帰納的関数の理論で何に相当するか調べるのは難しそうなので、いったん随伴関手について ChatGPT で調べてみることにします。
Option の随伴関手はどのようなものですか
と入力すると以下の結果となりました。
`Option` 型の随伴関手を考えるには、関手の定義と随伴性を確認する必要があります。まず、`Option` 型とは、ある型 `A` に対して以下のように定義される型のことです。
つまり、`Option(A)` は「`A` の要素」または「何もない（`None`）」を持つデータ型です。
`Option` 型の関手としての振る舞い
`Option` は エンド関手
であり、集合 `A` に対して `Option(A) = A + 1` を対応させ、関数 `f: A → B` に対して、次のような関数 `Option(f): Option(A) → Option(B)` を対応させます。
この `Option` 関手は、随伴関手の構造を持つことが知られています。
`Option` の随伴関手構造
`Option` は 自由・忘却の随伴性 を持ちます。具体的には、次の 2 つの関手を考えます。
1. `Option` 関手
これは、集合 `A` を 基点付き集合 `(A + 1, None)` に対応させる関手です。ここで、`1` は「基点」を表します。2. 忘却関手
これは、基点付き集合 `(B, b_0)` を基点を忘れて `B` に対応させる関手です。このとき、`Option` は次の随伴性を持ちます。
これは 自由関手
が忘却関手
の左随伴であること を意味します。
つまり、`Option` は集合 `A` に対して基点付き集合 `(A + 1, None)` を構成する自由関手として機能し、その右随伴は基点付き集合の基点を忘れる関手になります。
直感的な理解
- `Option` が左随伴（自由関手）: `A` から `Option(A)` への自然な埋め込みが存在する。（`A` の要素は `Some(x)` になり、`None` も加えられる）
- `Option` の右随伴（忘却関手）: 基点付き集合 `(B, b_0)` の基点情報を忘れて、ただの集合 `B` にする。
このように、`Option` 型は 基点付き集合の圏 との関係で随伴関手の構造を持つことがわかります。
まとめ
- `Option(A) = A + 1` はエンド関手として定義される。
- `Option` は 自由関手
- この随伴性は「基点付き集合」との関係を示している。
このように、`Option` 型の随伴関手の構造は、圏論的に見ると「基点付き集合を導入する自由関手」として理解できます。
これは違いました。
