Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
12年前の『型システム入門』翻訳の思い出話
Search
Yusuke Endoh
July 23, 2024
Programming
14
2.1k
12年前の『型システム入門』翻訳の思い出話
@ カワるガワるTAPLカタるヨる
https://taplts.connpass.com/event/320294/
Yusuke Endoh
July 23, 2024
Tweet
Share
More Decks by Yusuke Endoh
See All by Yusuke Endoh
An Invitation to TRICK: How to write weird Ruby programs
mame
1
870
TypeProf進捗
mame
0
36
Good first issues of TypeProf
mame
4
7.2k
Revisiting TypeProf - IDE support as a primary feature
mame
1
2.5k
error_highlight: User-friendly Error Diagnostics
mame
0
25
TRICK 2022 Results
mame
0
47
クックパッド春の超絶技巧パンまつり 超絶技巧プログラミング編 資料
mame
0
51
Enjoy Ruby Programming in IDE and TypeProf
mame
0
41
TypeProf for IDE: Enrich Development Experience without Annotations
mame
0
35
Other Decks in Programming
See All in Programming
Kubernetesで実現できるPlatform Engineering の現在地
nwiizo
2
1.7k
マルチアカウント環境での、そこまでがんばらない RI/SP 運用設計
wa6sn
0
400
RailsでCQRS/ESをやってみたきづき
suzukimar
2
1.5k
バックエンドNode.js × フロントエンドDeno で開発して得られた知見
ayame113
5
1.3k
GDG Super.init(version=6) - From Where to Wear : 모바일 개발자가 워치에서 발견한 인사이트
haeti2
0
560
生産性アップのためのAI個人活用
kunoyasu
0
480
データベースエンジニアの仕事を楽にする。PgAssistantの紹介
nnaka2992
9
4.1k
‘무차별 LGTM~👍’만 외치던 우리가 ‘고봉밥 코드 리뷰’를?
hannah0731
0
520
20250326_生成AIによる_レビュー承認システムの実現.pdf
takahiromatsui
17
5.2k
ニックトレイン登壇資料
ryotakurokawa
0
140
Gunma.web #55
tinykitten
0
130
Preact、HooksとSignalsの両立 / Preact: Harmonizing Hooks and Signals
ssssota
1
630
Featured
See All Featured
CSS Pre-Processors: Stylus, Less & Sass
bermonpainter
356
30k
ピンチをチャンスに:未来をつくるプロダクトロードマップ #pmconf2020
aki_iinuma
118
51k
How to Ace a Technical Interview
jacobian
276
23k
Designing Dashboards & Data Visualisations in Web Apps
destraynor
231
53k
Designing Experiences People Love
moore
141
23k
The World Runs on Bad Software
bkeepers
PRO
67
11k
Building Better People: How to give real-time feedback that sticks.
wjessup
367
19k
Agile that works and the tools we love
rasmusluckow
328
21k
Visualizing Your Data: Incorporating Mongo into Loggly Infrastructure
mongodb
45
9.5k
The Pragmatic Product Professional
lauravandoore
33
6.5k
YesSQL, Process and Tooling at Scale
rocio
172
14k
Refactoring Trust on Your Teams (GOTO; Chicago 2020)
rmw
34
2.9k
Transcript
12年前の 『型システム入門』 翻訳の思い出話 遠藤 侑介 2024/07/24 @カワるガワるTAPLカタるヨる
自己紹介:遠藤侑介 • プログラミング言語Rubyのフルタイム開発者 • STORESという会社で Rubyのための型解析器TypeProfを開発してます • 『型システム入門』(TAPL)の翻訳者のひとり • 今日は主にこっちの話
遠藤が翻訳した章 • 2章『数学的準備』 • 14章『例外』 • 15章『部分型付け』 • 22章『型再構築』 •
23章『全称型』 • 24章『存在型』 • 29章『型演算子とカインド』 • 30章『高階多層』 • 全体の3~4割くらい担当した ここ
Q. TAPL読んだ? • 半分以上~全部読み終えた • お疲れさまでした • これから読みたい~読み始めたところ • おすすめの読み方をご紹介
Q. なぜTAPLを読もうと思った? • 型システムを基礎から学びたいから • OK、上からぜんぶ読んでください • TypeScriptの型システムを理解したいから • ちょっとたいへんかも
TypeScriptの特徴はTAPLで学べない • TAPLはあくまで「入門」 • gradual typingは言及なし(というかTAPL出版後にできた) • local type inferenceはわずかに言及があるのみ
• とはいえ、他の本も知らない • いい感じに斜め読みするのがおすすめ ※話者はTypeScriptの型システムに詳しいわけではないです
TAPLの章構成 • 章の依存グラフ • 『序文』に載ってます
おすすめの斜め読み • 2章『数学的準備』 • 3章『型無し算術式』 • 5章『型無しラムダ計算』 • プログラミング言語理論の 基礎を学ぶ
• ラムダ計算 • 操作的意味論
おすすめの斜め読み • 8章『型付き算術式』 • 9章『型付きラムダ計算』 • 11章『単純な拡張』 • 型システムの基礎を学ぶ •
ML言語のコアがわかる • OCamlを触ってるとわかりやすい • 進行と保存(いわゆる型安全性)
おすすめの斜め読み • 15章『部分型付け』 • 部分型を学ぶ • type User={name: string}; function
f(val: User) {…} に {name:"x", age:20} を渡せる • TypeScriptを知っていると ちょっとわかりやすそう!
おすすめの斜め読み • 23章『全称型』 • 型変数、ジェネリクスを学ぶ • function f<T>(val: T) {…}
• ただし λT. λval:T. ... と書く • たぶんここまで読めば十分
興味あればおすすめ • 20章『再帰型』 • 再帰的な宣言になっている型 • type T = {
x: T } | …
興味あればおすすめ • 22章『型再構築』 • いわゆる型推論の話 • 型推論に触れるのはこの章だけ • ただし、ML前提なので注意 •
引数の型を明記するTypeScriptとは だいぶ前提が異なっている(と思う)
興味あればおすすめ • 26章『有界量化』 • 型変数のextendsの話 • type User={name: string}; function
f<T extends User>(val: T) {...}
興味あればおすすめ • 29章『型演算子とカインド』 • 型レベルの関数の話 • 型レベルプログラミングや 型クラスにつながると思う (けど話者もあまり詳しくない)
物足りなければ • 12章『正規化』 • 16章『部分型付けのメタ理論』 • 21章『再帰型のメタ理論』 • TAPL最難の章 •
28章『有界量化のメタ理論』
今日の話 • TAPLのおすすめの読み方 • 翻訳思い出話
TAPLとの出会い • 大学の輪講 • 23章『全称型』を担当した • 準備不足で先輩にとても怒られた • 翻訳のきっかけ •
今井健男、酒井、遠藤で別の本を訳した • いつの間にか「次はTAPL」になってた
TAPL翻訳プロジェクト:メンバー • 監訳者:東北大学 住井英二郎先生 • 原著者のPierce先生と共同研究されていた方 • 名前貸しなどではなく、とてもコミットしていただいた • 翻訳者
• 今井健男、酒井、遠藤、黒木(東芝の研究所の同僚) • 今井敬吾、今井宜洋、才川(名古屋のOCaml勉強会) • (今井が3人もいるのは偶然)
TAPL翻訳プロジェクト:期間 企画立ち上げ 2011/05 2011/07 メンバー 集め 翻訳開始 2011/09 編集開始 2012/10
2012/12 公募 レビュー 脱稿 2013/02 2013/03 発売 1年以上! かかりすぎ?
訳語の議論: typing statement • 型付け言明 • 型付け判断 • 型判定 •
型付け判定 • 型付け関係式 • 型付け判定式 • 型付け判断式 「言明」が 直訳でよい? 「型判定」が すでに普及? 論理学で judgmentは 「判断」が定訳 「式」がないと わかりにくい typing judgmentと 同義
訳語の議論: (Church) encoding • 符号化 • エンコード • 組込み •
埋込み • 表現 CSで「符号化」は 誤解をまねく 「チャーチ表現」 が定訳? 「表現」は representと 紛らわしい? encodeとrepresentの 全出現を確認した。 混乱はない!
訳語の議論: English • 「英語と同じくらい簡単に読める」という文脈 • 英語 • 日本語 • 母国語
• 自然言語 日本語訳では 「日本語」でよい? 原文でJapaneseと 書いてあったと 誤読する 「原文ではEnglishと書いてある」 と訳注をつけよう 訳注単体で見ると 意味不明 訳注をもっと 説明的にしよう やりすぎだ 意訳して「自然言語」は?
訳語の議論: he/she/they • 彼 • 彼女 • 彼ら • 人名に置き換える
「彼ら」はよいが 「彼」「彼女」に抵抗が… 別によくない? できるだけ避けたい パッチ 書きました 一部 間違ってない? 原文だけ見ても 誰を指しているか 曖昧… 参考文献を追って 特定した!
"A is X" にもいろいろな訳がある • ニュートラルな訳 • 「AはXである」 • 「BやCではなくA」という文脈での正しい訳
• 「AこそがXである」「XなのはAだ」 • 「YやZではなくX」という文脈での正しい訳 • 「AはXなのである」「AはまさにXだ」 • 英語は日本語ほど微妙なニュアンスが明示されにくい • 正しく訳すには、まず正確な理解が必要 ※住井先生の受け売り
次々見つかる原文の問題 (1) • 特に演習にちらほらバグがあった • 解答は「自明」だけ → 補題が弱くて証明できなかったとか • (もちろん、いずれも修正は可能でした)
• 『監訳者序文』より • 「遠藤氏は、… 演習の解答などに多くの非自明な誤りを発 見し、世界中で最も(…原著者よりも?)注意深く TAPL を 読んだのではないかと思われる」 • 住井先生の監修のおかげで誤りを検証できた
次々見つかる原文の問題 (2) • 「◯◯が~~を証明した」 • レビュアー「彼が証明したのは別の性質では?」 →大論文サーベイ大会開始 • リグレッションバグ •
第8版で直っていた問題が第9版で復活していたとか • 型推論の計算量が実用上問題ない理由 • 説明に矛盾があったり、遅くなる理由が間違ってたり • 22.7節の長めの訳注につながった • すべて原著者に報告済 • https://www.cis.upenn.edu/~bcpierce/tapl/errata.txt
もちろん訳者側の問題も多数 • 誤訳 • 内容の誤解にもとづくものから、単なる書き間違いまで • 自然言語は型チェックも自動テストもできない(言い訳) • 訳者が多いことを活かし、相互レビューしまくってがんばった •
訳語のぶれ • 訳者が多いので訳語の統一がとても大変だった • 相互レビューとgrepでがんばりまくった
まとめ • TAPLのおすすめの読み方を紹介しました • 15章と23章を目指してがんばって • TAPLを翻訳したときのエピソードを紹介しました • こだわって訳したので、とても時間がかかりました •
12年たってもイベントが開催されるほど愛読されていて うれしいです