See. 型システム入門 プログラミング言語と型の理論 | Amazon
メモ
- まずは5, 9, 11章読んでマスターするのがオススメ、と以下動画で訳者の方が言ってる
- 3章は簡単なことを大袈裟に言ってるだけな気がする
- 11章でバリアント、オプション、列挙型、全部出てきて最高すぎる
- 15章の部分型付けも知りたかったやつ
- 18章の型システムからみるオブジェクト指向も面白い
- 19.3 で Nominal typing（名前的部分型）、Structual typing（構造的部分型）の話出てくる
- 22章で型推論（シンプルなやつだけど）
- 数式はほぼ飛ばして文章の部分ばかり読んでる
知りたかったこと
型システムのメリットを分かりやすく
TAPL 1.2 に書いてあったので自分なりに要約する。
- エラーの検出
- 静的型検査の最も分かりやすい恩恵、プログラミングのエラーを実行前に検出できる
- 型検査時の方がエラー箇所を正確に特定できることが多い
- 抽象化
- モジュールのインターフェース（これ自身「モジュールの型」とみなせる）と実装を切り離して設計・議論することで、インターフェースをより抽象的に捉えることができる
- ドキュメント化
- 型宣言によりコードを理解しやすくなる、またこのドキュメントは静的型解析によって常に検査されるので古くなることもない
- 言語の安全性
- 静的型の安全性とは違う話らしい、、あまり理解できなかった
- 効率性
- 型情報を用いてコンパイラの最適化に貢献
👆 に加えて、今なら IDE による補完などもメリットに入ると思う
Also see. 私と型システムとポエム - The curse of λ
代数的データ型とは
TAPL 読む前の知識
- Haskell 代数的データ型 超入門 - Qiita
- 以下の3つを合わせて代数的データ型（ADT）という？
- 列挙型: いわゆる enum
- 直積型: いわゆる struct
- 直和型: いわゆる union
- 以下の3つを合わせて代数的データ型（ADT）という？
- 代数的データ型 - Wikipedia
- Wikipedia 的には代数的データ型とは直和型のことで、直積型と列挙型は特殊な例として扱われてる
- すごい Haskell 7 章にも記載あり
TAPL 読んだあと
- ...
部分型付けについて
- 構造的部分型とは
A: { a: number } :> B: { a: number, b: string }の A, B のように、親の型の構造が子のそれを含有する時、部分型であるとみなす型システム - 名前的部分型とは
B extends Aのような宣言があった場合のみ部分型であるとみなす型システム - A が親（上位型）で B が子（部分型）、子の方が親より多くのフィールドを持つ(!)
- TAPL 15.2 にフィールドの数が多い方がより小さい型（部分型 = 子の型）であるのは意外かもしれない。って書いてて自分がずっと引っかかってたところだったので最高！となった。 曰く、「フィールドが多い型の方がより要求の厳しい（より情報量のある）仕様を構成し、値のより小さな集合を形成することになるため」
- 共変と反変についても15.2に書いてある
