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
「型システムのしくみ」輪講 第一章
Search
Naoya Furudono
May 09, 2025
Programming
0
69
「型システムのしくみ」輪講 第一章
社内で開催している輪講の発表に用いた資料です
Naoya Furudono
May 09, 2025
Tweet
Share
More Decks by Naoya Furudono
See All by Naoya Furudono
設計と複雑さのはなし
naoyafurudono
0
45
waiwai-aiを入社2ヶ月の エンジニア3人と作るための さいきょうのアーキテクチャ
naoyafurudono
0
430
CLIツール開発をProtocol Buffers スキーマで駆動する
naoyafurudono
1
700
Protocol Buffersスキーマ定義から GoのCLIを生成する
naoyafurudono
0
71
Other Decks in Programming
See All in Programming
リッチエディターを安全に開発・運用するために
unachang113
1
330
ZeroETLで始めるDynamoDBとS3の連携
afooooil
0
140
階層化自動テストで開発に機動力を
ickx
1
460
バイブコーディングの正体——AIエージェントはソフトウェア開発を変えるか?
stakaya
5
560
AI Ramen Fight
yusukebe
0
120
オホーツクでコミュニティを立ち上げた理由―地方出身プログラマの挑戦 / TechRAMEN 2025 Conference
lemonade_37
1
400
Git Sync を超える!OSS で実現する CDK Pull 型デプロイ / Deploying CDK with PipeCD in Pull-style
tkikuc
4
490
SwiftでMCPサーバーを作ろう!
giginet
PRO
2
210
新世界の理解
koriym
0
110
Jakarta EE Meets AI
ivargrimstad
0
530
Understanding Kotlin Multiplatform
l2hyunwoo
0
250
Flutterと Vibe Coding で個人開発!
hyshu
1
190
Featured
See All Featured
Become a Pro
speakerdeck
PRO
29
5.5k
Facilitating Awesome Meetings
lara
54
6.5k
Fantastic passwords and where to find them - at NoRuKo
philnash
51
3.4k
Design and Strategy: How to Deal with People Who Don’t "Get" Design
morganepeng
130
19k
ピンチをチャンスに:未来をつくるプロダクトロードマップ #pmconf2020
aki_iinuma
126
53k
The World Runs on Bad Software
bkeepers
PRO
70
11k
Optimising Largest Contentful Paint
csswizardry
37
3.4k
We Have a Design System, Now What?
morganepeng
53
7.7k
Agile that works and the tools we love
rasmusluckow
329
21k
Fight the Zombie Pattern Library - RWD Summit 2016
marcelosomers
234
17k
Large-scale JavaScript Application Architecture
addyosmani
512
110k
Typedesign – Prime Four
hannesfritz
42
2.7k
Transcript
型システムのしくみ輪講(第一章) 古殿直也 2025-05-09
輪講でやること(復習) 担当者を持ち回りでやる(今回はぼく) 担当範囲が決まっている(今回は第一章) 担当範囲の解釈を説明する(以降のスライドで説明します) 参加者はツッコミとか質問とかをする。すべての参加者が少なくとも一回は質問 すること いつでも質問してOK。担当者の発言を遮ってください 終わらなかったら次回に繰り越し このように本のトピックを議論して理解していきましょう 2
第1章 型システムとは 3
型システムはプログラムのOK / NGを判定する 以下のような OK / NG の判定基準を定めるのが型システム 1 +
true // よくない。NGと判定したい 1 + 2 // 良さそう。OKと判定したい 判定基準は(すなわち型システムは)どのような基準で定義するのが良いだろうか 4
誰がどのように判定基準(型システム)を定義するか 「実はとても難しい問題」 定義の方針を考えるにあたっての歴史的背景としてプログラムの未定義動作があ る 5
1.1 プログラムの未定義動作 6
CやC++には未定義動作がある 言語仕様の定義では、プログラムの動作の一部を仕様で定義しない、とする場合があ る 未定義動作の定義をC17(C言語の仕様)のドラフトから定義を引用 behavior, upon use of a nonportable
or erroneous program construct or of erroneous data, for which this document imposes no requirements Geminiによる翻訳 移植性のない、または誤ったプログラム構成要素や誤ったデータを使用した場合 の振る舞いであって、本ドキュメントが何の要求も課さないもの。 7
未定義動作の例 無効なポインタを参照する 最大の整数に1足した値を計算する 配列の範囲外を参照する そのほかもっと込み入ったものも(C17のドラフトを "undefined behavior"で検索 するとたくさん出てくる) 8
未定義動作をするプログラムを書くと、プログラマは辛い 未定義動作をするプログラムは、その振る舞いが仕様で定められていない 派手に壊れるかもしれない それっぽく動くかもしれない しばらくはうまく動くけど、ある日突然壊れるかもしれない 実際のところはどうか それっぽく動作する OSの保護機能でプロセスが落ちる segmentation faultで落ちるのはこれ
などなど 辛いのでなんとかしたい 9
1.2 歴史的解決策としての「型安全性」 10
未定義動作への対処 コンパイル時に型検査する この本で扱うような型システムが活躍するのはこちらのアプローチ 言語の例: OCaml, Haskell, Go, ... 実行時にたくさん検査する 言語の例:
JavaScript, Ruby, Smalltalk, ... 11
コンパイル時に型検査するアプローチ 未定義動作になるようなプログラムはプログラムと認めない 型検査器でプログラムを検証する。検証が通ったならば、プログラムは決して未 定義動作にならないことを型検査器と言語仕様に求める 12
実行時にたくさん検査するアプローチ(おまけ、蛇足) 未定義動作に踏み込みかけたときに例外を投げたりする 例外を投げるという動作を定義しているので未定義動作はなくせる C言語でも、どんなときに未定義動作になるかは定義されている。それを愚直に実 行時に検証すればよい 13
型安全性は「型システム」と「プログラムの振る舞いの定義」の間の関係 TaPLでは型安全性を「型検査器がOKと判定したプログラムは、定義されていない状態 (行き詰まり状態、stuck)にならない」という性質としている 以下のように解釈しました 型システム: 型検査の仕様 定義されていない状態:未定義動作 型安全性:型検査器がOKと判定したら未定義動作にならないという、型システム とプログラムの振る舞いの定義の間の関係 14
まとめ: 未定義動作に型システムで対処できる 未定義動作は辛い 型検査をして、未定義動作するかもしれないプログラムはコンパイル時に弾く 結果的に、プログラムを動かす段階では絶対に未定義動作に陥らないことを保証 できる 15
1.3 本書における型システムと型安全性 16
前提の確認 TypeScriptプログラムは普通、JavaScriptプログラムに変換されてからJavaScriptと して実行される JavaScript言語には未定義動作がない(少なくともC言語にあるような未定義動作 はなさそう) https://stackoverflow.com/questions/14863430/does-javascript-have- undefined-behaviour ここにあるように、implementation defined な動作はある
細かい話だし、どちらに転んでも型システムのしくみを感覚として理解 するためには問題にならなさそう 17
TypeScriptでは未定義動作ではなく「望ましくなさそうな動作」に対処するた めに型検査する JSには未定義動作がない 何かしら動作が定義されている。望ましい動作かはさておき 実行時に検証して、例外を投げる 不思議な計算結果を無理やり返す 実装に依存するとしている(これはCの仕様でもでもやられている) TSでは未定義動作を防ぐことではなく、 「望ましくなさそうな動作」を防ぐことを 目的に型検査をする
1 + true を計算する際のプログラムの振る舞いはJSで定義されているけど 望ましくなさそう 18
1.4 実装する型検査器のプログラムについて 19
型検査器と対象言語 型検査器が検査対象とする言語を「対象言語」と呼ぶ 例: tsc の対象言語は TypeScript JavaScriptではない go の対象言語は Go
20
今後実装していく型検査器の対象言語はTypeScriptのサブセットである サブセットであるとはどういうことだろうか 例えば arith.tsで実装する型検査器の対象言語 (arith-langとしましょう)が、TypeScript のサブセットであるとはどういうことか 21
ぼくの持っている答え arith-langの(型検査が通る)プログラムはすべて、TypeScriptの(型検査が通る)プロ グラムでもある、ということ。 言い換え: arith.tsで実装する型検査器がOKとするプログラムはすべて、tsc(TypeScript の型検査器)がOKとする、ということ。 クイズ: 最小の対象言語を持つ型検査器はどんな型検査器でしょう 22
クイズの答え どんなプログラムが来てもNGとする型検査器。 23
型検査器の実装を追加して、対象言語を徐々に大きくしていく (arith) 真偽値・数値、条件演算子・足し算 (basic) arith + 関数と変数定義 (obj) basic +
オブジェクト (rec) obj + 再帰関数 + 再帰型 ... TypeScript 24
演習問題 みんな動かせましたか?まだなら早めに試すのが吉です。苦戦したらSlackであらかじ めヘルプを求める、その辺にいる人を捕まえて一緒になんとかしてもらうなどしまし ょう 25
次回 2章の全てを予定しています 26
参考文献 27
C17 のドラフトをここから引用: https://www.open- std.org/jtc1/sc22/wg14/www/projects#9899 28