26-07-18

ニコニコのAI予測でコメントを複製する機能が意味不明で良い。存在する意味が無い。

• 総再生数推移がこのまま線形的に勧めば、10年以内にマイナスに踏み込むから動向が気になる。

コンピュータは凪ある永遠の趣味なので、私は今後も続けられる。OB

素朴なコンピュータの使用ほど面白いことはない。何か特定の活動ではなく、コンピュータから派生する全だ。

少し前に型検査を自作してみて、理論的な部分も少し入門できた。型理論の研究者が素人から入門するまでをまとめてくれていて役に立ったので、気になるなら参考にすべきだろう。彼のサーベイ論文など全体的に著者本人の足跡を辿れるように線が引かれいてる物が多くて本当に有用だった。彼の指南無しで双方向検査を理解できるまではやれなかった。

• https://cha.fan/articles/5u9DV2LWWcjgJ8c7ha7T

訳して無機質に列挙してみた↓

1. 静的型付き関数型言語（Haskell推奨、OCaml/SML可）を習得する。代数的データ型を型の加法・乗法として、集合の和・直積に対応させて理解する。

2. ラムダ計算（STLC、Hindley-Milner）の型システムの構造を理解する。型推論アルゴリズムの習得は不要。

3. 依存型を持つ言語（Agda / Lean / Idris2 / Arend）を表層的に学習する。rewriteの概念と等式型に対する直観を形成する。厳密な理解は不要。

4. 型理論の記法を習得する。対象：シーケント計算・自然演繹の判断形式、横線記法、Γ、⊢、コロン、代入 u[v/x]。STLCの型検査規則（少なくともラムダバインダ関連）を暗記で再現できる状態にする。任意の新規構文に対して代入操作の定義を導出できるようにする。証明論（⊨等）の学習は不要。

5. 形成規則・導入規則・除去規則・計算規則・η-等価性・宇宙階層を理解する。

6. 入門的な論文を読む。対象例：oktt（宇宙部分を除く）、arXiv:2103.15408、quantitative type theory。双方向型検査の構造と、それが双方向である理由を理解する。この段階でelaborationや圏論に着手しない。

7a. **設計方面**：
   - 圏論の基礎：前層、引き戻しを理解する。
   - 証明論における「モデル」＝型理論における「意味論」の概念を理解する。
   - デカルト閉圏（CCC）がSTLCのモデルとなる理由を理解する。
   - 文脈圏を学習する（Andrew Pitts, *Categorical Logic* 第1–2章）。代入と文脈の圏論的モデル化を理解する。
   - CwF（categories with families）を学習する。CwFが型の値への依存を記述でき、CCCでは不可能である理由を理解する。LCCC（局所デカルト閉圏）は非推奨：型が値に依存する本質を捉えておらず、対応する型理論が外延的。
   - CwFの応用を学習する。例：QCwF（quantitative type theory論文）。QCwFがquantitative type theoryのモデルとなる理由と、消去に用いられる関手を特定する。
   - Grothendieckファイブレーションを理解する。概括圏（comprehension category）を理解する。CwFおよびCwA（categories with attributes）の一般化として位置づける。
   - CwFにおける各型（Π型・和型・積型）の表現を理解する。
   - CwFにおける宇宙多相の表現を理解する。2種の定式化：CwU、およびN→CwFの関手にlift操作を定義する方式。

7b. **実装方面**：
   - elaborationの概念を学習する。参照：Mini-TT、LambdaPi.pdf、arXiv:2105.14840。conversion check、spine、telescopeを理解する。
   - de Bruijn index、de Bruijn levelを理解する。
   - 簡易な依存型理論を実装する。要件：Π型、sum type、単変数・非ネストのパターンマッチング。検証：Leibniz equality関連の定理の証明、自然数の加法交換律の定義と証明。複雑なパターンマッチングには着手しない。
   - 暗黙引数の脱糖と求解を実装する。参照：elaboration-zoo。pattern unificationの解決対象と実装を理解する。
   - 多変数・ネスト許容のパターンマッチングのelaborationを実装する。検証：indexed赤黒木（色・黒高さを型にエンコード）の記述。forced patternの必要性を確認する。
   - 型クラス、宇宙多相を実装する。
   - 既存の定理証明器のコード・論文を読む。大規模：Agda、Arend、Idris2、Lean4。小規模：[ditto](https://github.com/ditto/ditto)、[sixty](https://github.com/ollef/sixty)。

私は7a,bの最初辺りまで理解できた。型理論は何を勉強するか迷走する時間が多いとネット上の雰囲気を感じた。

なので研究者がロードマップを作ってくれるのは本当にありがたいよね。そのおかげで型の使用については納得できた。型の実装は少し寝かせる時間を作ろうと思う。これを参照するまでは型エラーと実行エラーの違いについてもピンときてなかったんだよね。まさかschemeから関数型言語などと繋がって、それが数学の証明になったと思った瞬間に圏論と直観主義数学とλの大三角形が怪しげな天体を広げて,宇宙になっていくとは思わなかった。プログラミングの世界観とはλのファンタジーなのは言うまでもない。

直積や直和など、実際に触れないと認識がズレることなど、プログラミングで言われるタームの原典に強制的に触れないといけないので、定義のビタ当てが起きて、十分にやる価値はある。これをする前は悪い意味で哲学的な用語の使い方をしていた。反省

あとplfaもいいぞ！

• https://plfa.github.io/

agdaは証明支援系の中でかなり気に入ったモノだ。使ってみたら分かるけど、あまりにシンプルで構築的すぎる。だが理解するにはこれ以上ない。

やはり再構築はいい。明日死ぬと分かっても、再構築するだろう。知識とは受容ではなく、構築だから。暗記や言語化も、知識を構築する導線を強める訓練だ。

プログラミングにおけるIntやBoolが集合だと説明されるものが多かったが、圏論の入門書を一周した時点で納得できた。 agdaの記法と組み合わせるとかなり簡単だと思う。ただ素の脳容量を越える内容だった。前にブログに書いた気がする。 集合に条件を付与していって、プログラミングで使う型として見做す。実装で理想的な状態ではなくなるけど、何を見て作られた概念なのかは原典を当たることで納得できたのでよかった。