入門 型入門

[hayashi-ay]

https://techbookfest.org/product/5798421917073408

[hayashi-ay]

第1章 影響を受けた言語、与えた言語

[hayashi-ay]

第2章 プログラミングにおける順序

2.1 ソート関数における順序

2.2 部分型や依存の関係における順序集合

Scala3の型ヒエラルキー。型ヒエラルキーは有向非巡回グラフ。 Scala3は合弁型（union type）と交差型（intersection type）をサポートしている。 合弁型、交差型はそれぞれ型の上界（upper bound）と下界（lower bound）を決定する。 任意の2つの型について上限と下限が存在するのでScala3の型システムは束（lattice）であるといえる。

例）

• String | Int Upper bound はString | Int型になる。 String ≤ T かつ Int ≤ Tを満たす最小。String ≤ T かつ Int ≤ T かつ T < (String | Int）であるような型Tは存在しない。
• Countable & Selectable Lower boundはCountable & Selectable型になる。T ≤ Countable かつ T ≤ Selectableを満たす最大。

用語集

全順序（total order）

集合での二項関係で推移律、反対称律、完全律の全てを満たすもののこと。

1. If a ≤ b and b≤ c then a ≤ c (推移律: transitive)
2. If a ≤ b and b ≤ a then a = b (反対称律: antisymmetric)
3. a ≤ b or b ≤ a (完全律、比較可能性: strongly connected, formerly called total)

また完全性から反射性も満たすことがいえる。

4. a ≤ a (反射性: reflexive)

• https://en.wikipedia.org/wiki/Total_order
• https://en.wikipedia.org/wiki/Order_theory

[hayashi-ay]

第3章 値か参照か

3.3 値呼びか参照呼びか

プログラムの中の四季をどんな順で評価していくかを評価戦略（評価順序）という。

[hayashi-ay]

第4章 添字か引数か

match文により要素の型を指す仕組みをmatch typeという。

[hayashi-ay]

第5章 3つの型消去

型消去（type erasure）とは型変数が存在するクラスや構造体において型変数を消去すること。

5.1 Swiftにおける型消去テクニック

5.2 Javaの型消去

Javaにおける型消去はジェネリクスと型実現のためにコンパイル時に行われる処理のうちの1つである。Javaソースファイル中に書いた型変数はJVMには渡されない。

5.2.3 まとめ

Javaは型消去することでジェネリクス型を実現した。全ての型変数を1つの型に置き換えることからこの手法は同種変換（homogenous translation）とよばれる。個別の型に置き換える手法は異種変換（hoterogeneous translation）と呼ばれる。C++のテンプレートは異種変換を採用していて、プログラムのサイズは大きくなるが実行性能では勝る。

5.3 TypeScriptにおける型消去

TypeScriptにおける型消去とは、トランスパイルしてJavaScriptコードにする際に型情報などが取り除かれることを指す。

[hayashi-ay]

第6章 部分型

6.1 部分型か継承か

型Sが型Tの部分型であるということは以下のように定義される。

• 型Tに対して行える操作を型Sにも行うことができる
• 型Tを書くべきところに型Sを書くことができる

6.2 トップ型とボトム型

言語によっては「すべての型の上位型である型」「すべての型の部分型である型」が用意されている。前者をトップ型、校舎をボトム型という。

6.2.2 TypeScriptのトップ型とボトム型

TypeScriptのトップ型はunknow、ボトム型はneverである。

[hayashi-ay]

型システムについてもっと深く理解したいけれど、一歩を踏み出すのが大変そうだったのでまず型システム入門の入門書と称している本書を手に取りました。本書の内容でも初めて知ることが多かったです。理論には踏み込まないが、外観がうっすらとつかめた感じがします。ちゃんと型システムを理解するにはそれのベースとなっている順序集合などの理論もある程度抑えていないといけなさそうなことが思いました。型システムに入門する際に詰まったらまた本書を読んでみようと思います。