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
11
1.5k
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
Good first issues of TypeProf
mame
4
5.2k
Revisiting TypeProf - IDE support as a primary feature
mame
1
2.1k
error_highlight: User-friendly Error Diagnostics
mame
0
13
TRICK 2022 Results
mame
0
9
クックパッド春の超絶技巧パンまつり 超絶技巧プログラミング編 資料
mame
0
15
Enjoy Ruby Programming in IDE and TypeProf
mame
0
17
TypeProf for IDE: Enrich Development Experience without Annotations
mame
0
13
Ruby 3の型解析に向けた計画
mame
0
17
emruby: ブラウザで動くRuby
mame
0
12
Other Decks in Programming
See All in Programming
dotfiles について話したい #湘なんか
stefafafan
2
280
楽しく簡単に!QRコードの読み取り機能を実装しよう
penguinsan_pg
1
190
初めてのiOS関連GitHub ActionsをMarketplaceに公開するまでの実録
konifar
3
200
Wallet API, Verifier APIで実現するIDカード on iPhoneの世界
shitamori1272
1
320
これからの時代の新標準!SwiftTestingへの移行とトラブルシューティング
uetyo
0
440
複雑さに立ち向かうための ソフトウェア開発入門
shiz
2
580
Ebitengineの1vs1ゲーム WebRTCの活用
ponyo877
0
330
フロントエンドカンファレンス北海道2024 『小規模サイトでも使えるVite 〜HTMLコーディングをよりスマートに〜』長谷川広武(ハム)
h2ham
1
2.5k
ゲームボーイアドバンスでSwiftを動かそう
k_koheyi
0
510
ドメイン駆動設計を実践するために必要なもの
bikisuke
3
290
めざせ!WKWebViewマスター! / WKWebView Master
marcy731
3
480
Kotlin 2.0 and Beyond
antonarhipov
2
130
Featured
See All Featured
Teambox: Starting and Learning
jrom
131
8.7k
Faster Mobile Websites
deanohume
304
30k
Designing Experiences People Love
moore
138
23k
Embracing the Ebb and Flow
colly
83
4.4k
Designing the Hi-DPI Web
ddemaree
278
34k
Making the Leap to Tech Lead
cromwellryan
128
8.8k
Navigating Team Friction
lara
183
13k
Into the Great Unknown - MozCon
thekraken
28
1.4k
The Brand Is Dead. Long Live the Brand.
mthomps
53
37k
Learning to Love Humans: Emotional Interface Design
aarron
270
40k
Docker and Python
trallard
39
3k
Producing Creativity
orderedlist
PRO
340
39k
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年たってもイベントが開催されるほど愛読されていて うれしいです