12年前の『型システム入門』翻訳の思い出話

Transcript

1. 12年前の 『型システム入門』 翻訳の思い出話 遠藤 侑介 2024/07/24 @カワるガワるTAPLカタるヨる

2. 自己紹介：遠藤侑介 • プログラミング言語Rubyのフルタイム開発者 • STORESという会社で Rubyのための型解析器TypeProfを開発してます • 『型システム入門』（TAPL）の翻訳者のひとり • 今日は主にこっちの話

3. 遠藤が翻訳した章 • 2章『数学的準備』 • 14章『例外』 • 15章『部分型付け』 • 22章『型再構築』 •

   23章『全称型』 • 24章『存在型』 • 29章『型演算子とカインド』 • 30章『高階多層』 • 全体の3～4割くらい担当した ここ

4. Q. TAPL読んだ？ • 半分以上～全部読み終えた • お疲れさまでした • これから読みたい～読み始めたところ • おすすめの読み方をご紹介

5. Q. なぜTAPLを読もうと思った？ • 型システムを基礎から学びたいから • OK、上からぜんぶ読んでください • TypeScriptの型システムを理解したいから • ちょっとたいへんかも

6. TypeScriptの特徴はTAPLで学べない • TAPLはあくまで「入門」 • gradual typingは言及なし（というかTAPL出版後にできた） • local type inferenceはわずかに言及があるのみ

   • とはいえ、他の本も知らない • いい感じに斜め読みするのがおすすめ ※話者はTypeScriptの型システムに詳しいわけではないです

7. TAPLの章構成 • 章の依存グラフ • 『序文』に載ってます

8. おすすめの斜め読み • 2章『数学的準備』 • 3章『型無し算術式』 • 5章『型無しラムダ計算』 • プログラミング言語理論の 基礎を学ぶ

   • ラムダ計算 • 操作的意味論

9. おすすめの斜め読み • 8章『型付き算術式』 • 9章『型付きラムダ計算』 • 11章『単純な拡張』 • 型システムの基礎を学ぶ •

   ML言語のコアがわかる • OCamlを触ってるとわかりやすい • 進行と保存（いわゆる型安全性）

10. おすすめの斜め読み • 15章『部分型付け』 • 部分型を学ぶ • type User={name: string}; function

    f(val: User) {…} に {name:"x", age:20} を渡せる • TypeScriptを知っていると ちょっとわかりやすそう！

11. おすすめの斜め読み • 23章『全称型』 • 型変数、ジェネリクスを学ぶ • function f<T>(val: T) {…}

    • ただし λT. λval:T. ... と書く • たぶんここまで読めば十分

12. 興味あればおすすめ • 20章『再帰型』 • 再帰的な宣言になっている型 • type T = {

    x: T } | …

13. 興味あればおすすめ • 22章『型再構築』 • いわゆる型推論の話 • 型推論に触れるのはこの章だけ • ただし、ML前提なので注意 •

    引数の型を明記するTypeScriptとは だいぶ前提が異なっている（と思う）

14. 興味あればおすすめ • 26章『有界量化』 • 型変数のextendsの話 • type User={name: string}; function

    f<T extends User>(val: T) {...}

15. 興味あればおすすめ • 29章『型演算子とカインド』 • 型レベルの関数の話 • 型レベルプログラミングや 型クラスにつながると思う （けど話者もあまり詳しくない）

16. 物足りなければ • 12章『正規化』 • 16章『部分型付けのメタ理論』 • 21章『再帰型のメタ理論』 • TAPL最難の章 •

    28章『有界量化のメタ理論』

17. 今日の話 • TAPLのおすすめの読み方 • 翻訳思い出話

18. TAPLとの出会い • 大学の輪講 • 23章『全称型』を担当した • 準備不足で先輩にとても怒られた • 翻訳のきっかけ •

    今井健男、酒井、遠藤で別の本を訳した • いつの間にか「次はTAPL」になってた

19. TAPL翻訳プロジェクト：メンバー • 監訳者：東北大学 住井英二郎先生 • 原著者のPierce先生と共同研究されていた方 • 名前貸しなどではなく、とてもコミットしていただいた • 翻訳者

    • 今井健男、酒井、遠藤、黒木（東芝の研究所の同僚） • 今井敬吾、今井宜洋、才川（名古屋のOCaml勉強会） • （今井が3人もいるのは偶然）

20. TAPL翻訳プロジェクト：期間 企画立ち上げ 2011/05 2011/07 メンバー 集め 翻訳開始 2011/09 編集開始 2012/10

    2012/12 公募 レビュー 脱稿 2013/02 2013/03 発売 1年以上！ かかりすぎ？

21. 訳語の議論: typing statement • 型付け言明 • 型付け判断 • 型判定 •

    型付け判定 • 型付け関係式 • 型付け判定式 • 型付け判断式 「言明」が 直訳でよい？ 「型判定」が すでに普及？ 論理学で judgmentは 「判断」が定訳 「式」がないと わかりにくい typing judgmentと 同義

22. 訳語の議論: (Church) encoding • 符号化 • エンコード • 組込み •

    埋込み • 表現 CSで「符号化」は 誤解をまねく 「チャーチ表現」 が定訳？ 「表現」は representと 紛らわしい？ encodeとrepresentの 全出現を確認した。 混乱はない！

23. 訳語の議論: English • 「英語と同じくらい簡単に読める」という文脈 • 英語 • 日本語 • 母国語

    • 自然言語 日本語訳では 「日本語」でよい？ 原文でJapaneseと 書いてあったと 誤読する 「原文ではEnglishと書いてある」 と訳注をつけよう 訳注単体で見ると 意味不明 訳注をもっと 説明的にしよう やりすぎだ 意訳して「自然言語」は？

24. 訳語の議論: he/she/they • 彼 • 彼女 • 彼ら • 人名に置き換える

    「彼ら」はよいが 「彼」「彼女」に抵抗が… 別によくない？ できるだけ避けたい パッチ 書きました 一部 間違ってない？ 原文だけ見ても 誰を指しているか 曖昧… 参考文献を追って 特定した！

25. "A is X" にもいろいろな訳がある • ニュートラルな訳 • 「AはXである」 • 「BやCではなくA」という文脈での正しい訳

    • 「AこそがXである」「XなのはAだ」 • 「YやZではなくX」という文脈での正しい訳 • 「AはXなのである」「AはまさにXだ」 • 英語は日本語ほど微妙なニュアンスが明示されにくい • 正しく訳すには、まず正確な理解が必要 ※住井先生の受け売り

26. 次々見つかる原文の問題 (1) • 特に演習にちらほらバグがあった • 解答は「自明」だけ → 補題が弱くて証明できなかったとか • （もちろん、いずれも修正は可能でした）

    • 『監訳者序文』より • 「遠藤氏は、… 演習の解答などに多くの非自明な誤りを発 見し、世界中で最も（…原著者よりも？）注意深く TAPL を 読んだのではないかと思われる」 • 住井先生の監修のおかげで誤りを検証できた

27. 次々見つかる原文の問題 (2) • 「◯◯が～～を証明した」 • レビュアー「彼が証明したのは別の性質では？」 →大論文サーベイ大会開始 • リグレッションバグ •

    第8版で直っていた問題が第9版で復活していたとか • 型推論の計算量が実用上問題ない理由 • 説明に矛盾があったり、遅くなる理由が間違ってたり • 22.7節の長めの訳注につながった • すべて原著者に報告済 • https://www.cis.upenn.edu/~bcpierce/tapl/errata.txt

28. もちろん訳者側の問題も多数 • 誤訳 • 内容の誤解にもとづくものから、単なる書き間違いまで • 自然言語は型チェックも自動テストもできない（言い訳） • 訳者が多いことを活かし、相互レビューしまくってがんばった •

    訳語のぶれ • 訳者が多いので訳語の統一がとても大変だった • 相互レビューとgrepでがんばりまくった

29. まとめ • TAPLのおすすめの読み方を紹介しました • 15章と23章を目指してがんばって • TAPLを翻訳したときのエピソードを紹介しました • こだわって訳したので、とても時間がかかりました •

    12年たってもイベントが開催されるほど愛読されていて うれしいです