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.3k
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
型システムを知りたい人のための型検査器作成入門
mame
15
4.4k
TRICK 2025 Results
mame
0
4.4k
Writing Ruby Scripts with TypeProf
mame
1
840
An Invitation to TRICK: How to write weird Ruby programs
mame
1
1k
TypeProf進捗
mame
0
60
Good first issues of TypeProf
mame
4
8.2k
Revisiting TypeProf - IDE support as a primary feature
mame
1
2.7k
error_highlight: User-friendly Error Diagnostics
mame
0
36
TRICK 2022 Results
mame
0
73
Other Decks in Programming
See All in Programming
Claude Code で Astro blog を Pages から Workers へ移行してみた
codehex
0
170
なぜ今、Terraformの本を書いたのか? - 著者陣に聞く!『Terraformではじめる実践IaC』登壇資料
fufuhu
3
390
PHPカンファレンス関西2025 基調講演
sugimotokei
6
1.1k
SQLアンチパターン第2版 データベースプログラミングで陥りがちな失敗とその対策 / Intro to SQL Antipatterns 2nd
twada
PRO
36
11k
書き捨てではなく継続開発可能なコードをAIコーディングエージェントで書くために意識していること
shuyakinjo
0
190
バイブスあるコーディングで ~PHP~ 便利ツールをつくるプラクティス
uzulla
1
320
LLMは麻雀を知らなすぎるから俺が教育してやる
po3rin
3
1.9k
はじめてのWeb API体験 ー 飲食店検索アプリを作ろうー
akinko_0915
0
180
DataformでPythonする / dataform-de-python
snhryt
0
150
プロダクトという一杯を作る - プロダクトチームが味の責任を持つまでの煮込み奮闘記
hiliteeternal
0
370
Bedrock AgentCore ObservabilityによるAIエージェントの運用
licux
8
560
MCPで実現できる、Webサービス利用体験について
syumai
7
2.4k
Featured
See All Featured
Practical Tips for Bootstrapping Information Extraction Pipelines
honnibal
PRO
21
1.4k
Agile that works and the tools we love
rasmusluckow
329
21k
Scaling GitHub
holman
461
140k
Dealing with People You Can't Stand - Big Design 2015
cassininazir
367
26k
Evolution of real-time – Irina Nazarova, EuRuKo, 2024
irinanazarova
8
870
Save Time (by Creating Custom Rails Generators)
garrettdimon
PRO
31
1.3k
GraphQLとの向き合い方2022年版
quramy
49
14k
VelocityConf: Rendering Performance Case Studies
addyosmani
332
24k
Easily Structure & Communicate Ideas using Wireframe
afnizarnur
194
16k
Designing for Performance
lara
610
69k
Building an army of robots
kneath
306
45k
The Power of CSS Pseudo Elements
geoffreycrofte
77
5.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年たってもイベントが開催されるほど愛読されていて うれしいです