型システムを自分で設計したいと思ったので「型システム入門 プログラミング言語と型の理論」（原題：Types and Programming Languages, 略して TaPL）を読んで勉強している。

この記事は私の雑な理解を吐き出したものであり、あまりまとまっていない。しかし、何かしらをアウトプットすることに意義がある（ｷﾘｯ

単純型

一番基本になるやつ。

Curry-Howard 対応では、命題論理に対応する。

部分型付け (subtyping)

Float 型の項が必要とされる箇所に Int 型の項を投入できる、みたいなやつ。

C/C++ や Java といった言語でおなじみ。

Haskell には部分型付けはない…が、型適用（後述）が暗黙なので、一つの（全称型のついた）項に複数の（具体的な）型がつくことがある。これは普通は部分型付けとは呼ばない…と思う（自信なし）。

Top と Bottom

Top は部分型関係における最大元、 Bottom は部分型関係における最小元のことである。

Top は任意の型の値を保持できる object 型っぽいやつのことと思っていいだろう。Bottom は「値を持たない型」あるいは関数が「制御を返さない」ことを表すのに使える型とも言える。

TypeScript の any 型は Top で、 never 型は Bottom と言える。…が、 TypeScript の any 型は、任意の型の上位型として振る舞うと同時に、任意の型の部分型としても振る舞う（だからと言って任意の型が任意の型の subtype となるわけではない。any が特別というか、部分型関係の any を挟んだ推移性が制限されていると言った方がより正確か）。とにかく TypeScript の any はヤバい。

Bottom を導入すると、 Bottom 型の項に対して関数適用できるようになるので、型検査器の複雑さが増すらしい。

部分集合意味論 vs 型強制意味論

部分集合意味論というのは、部分型の値は（部分集合のように）自然に上位型の値としてみなせるという解釈のことである。

型強制意味論は、部分型の値を上位型の値としてみなす際には何らかの変換を行う、という解釈のことである。

TypeScript の場合は、型とは全体集合（ターゲット言語の値全体）の部分集合を指定するものであるから、部分集合意味論を採用していると言って良いだろう。（コンパイル時に型変換のようなものは挟まらないはず）

型が実行時の表現（固定長整数 vs 浮動小数点数 vs ポインタ）を規定するタイプの処理系の場合は、必然的に型強制意味論になるだろう。

整合性 (coherence)

型強制意味論では、部分型の項を上位型の項に変換するやり方が一通りであるとは限らない。例えば、 Int <: String の変換関数が 1 を “1” に変換し、 Float <: String の変換関数が 1 を “1.0” に変換する場合、 Int を直接 String に変換するのと、 Int を Float 経由で String に変換するので結果が変わってしまう。

このようなことが起こらない、つまり、どのような経路で変換しても結果が変わらないという性質を、整合性という。

圏論の言葉を使えば、「部分型関係の圏から、型と関数の圏への、部分型関係に対して変換関数を対応させる関係が関手となっていること」と定式化できる。

交差型 (intersection type) と 合併型 (union type)

交差型は、関数のオーバーロードに対してうまい型をつける。

これらは TypeScript にあることで知っている方も多いだろう。TypeScript では合併型の方が先に実装されたが、歴史的には交差型の方が先で、合併型は交差型の双対概念として考案されたようだ（？）。

関数のオーバーロードができると言っても、好き勝手な関数のオーバーロードを許すと整合性が成り立たなくなるので、要注意である。

「型システム入門」は入門書なので、これらのトピックについては紹介程度にとどまっている。

再帰型 (recursive type)

今回のモチベーション的にそこまで関心はないので…飛ばす！（ｦｲ

多相型 (polymorphic type)

個別の型について似たような関数をたくさん書くのではなく、型パラメーターを取る総称的な関数を1個用意して、そいつに型適用するようにしましょう、というやつ。

単純型付きラムダ計算に多相型を加えたものは、 System F と呼ばれる。

Church エンコーディングによって代数的データ型を実現できる。

型抽象、型適用

通常のラムダ抽象が項でパラメトライズされた項ならば、型抽象は型でパラメトライズされた項である。

型抽象の記法には、型システム入門では小文字のラムダを再利用している。他の文献では、大文字のラムダ (Λ) を使っているものも見受けられる。

後述する自作 System F 処理系では、入力のしやすさ的に ASCII 文字を使いたかったので、はてなマークを使って ?a. という記法にした。この記法では多相的な恒等関数は ?a. \x:a. a と書ける（この項の型は forall a. a -> a）。

通常の関数適用は項に項を適用するが、型適用は項に型を適用する。自作処理系では、型システム入門に倣って x [ty] という記法にした。

Haskell vs System F

Haskell と System F を比較してみよう。

• 純粋な System F （不動点コンビネータなし）では再帰関数を書けないが、 Haskell では書ける。
• 素の Haskell では、型抽象/全称型を明示的に書けない。
  • GHC 拡張 (ExplicitForAll) により、型シグネチャに全称型 forall を書けるようになる。
  • 私の把握している限り、 Haskell において型抽象を明示的に書く方法はない。適切な型注釈を書けば必要ないからか。
  • ちなみに、 GHC Core では通常の（項に関する）ラムダ抽象と型抽象を同じ Lam というコンストラクタで表すらしい。
• 素の Haskell では、型適用を明示的に書けない。
  • GHC 拡張 (TypeApplications) で書けるようになる。
• 素の Haskell では、引数に全称型が含まれる関数型を書けない。
  • (forall a. a -> a -> a) -> Int みたいな型の関数を書けない、という意味。
  • GHC 拡張 (RankNTypes) により書けるようになる。
  • Rank 2 と Rank 3 以上では型再構築に関して違いがあるらしい。しかし最近の GHC では Rank2Types は deprecated で、 RankNTypes と同じ意味になるらしい。
• 素の Haskell では、型変数の動く範囲は単型（forall を含まない型）に制限されている。
  • GHC 拡張 (ImpredicativeTypes) により、 forall を含む型を動かせるようになる。

素の Haskell は System F と比べてかなり控えめだが、 GHC Core が System F の亜種というだけあって、 GHC 拡張を有効にすれば System F の大概の機能は Haskell で使えるようになる。

型消去意味論 vs 型渡し意味論

型抽象と型適用をどう実装するか？という問題。

• 型消去意味論
  • 「型なんて飾りです。偉い人には(ry」
  • パラメトライズされた型を void * とか object 型とか variant 型として実装するタイプのジェネリクスはこっちだと思っていいだろう。Haskell の多相（ボックス化された値を扱う）や Java のジェネリクスなど。
  • TypeScript のような、型なしのスクリプト言語に翻訳される場合もこっち。
• 型渡し意味論
  • 型適用の度に型を代入していく。
  • C++ のテンプレートや Rust の多相のようなコンパイル時にコードを複製するタイプ、あるいは、実行時にバイトコードを複製するするタイプのジェネリクスはこっちに近いだろうか。

多相型 + 部分型付け（有界量化）

有界量化とは、型パラメーターに対して部分型関係による制約を与えたものである。forall a. が forall a <: B. （型変数 a は型 B の部分型を動く）のようになる。Top 型があれば、非有界な量化と有界量化を統一できる。

System F に部分型付けと有界量化を加えたものは、 System F_<: (System Fsub) と呼ばれる。

Java のジェネリクスを extends で制限するやつは有界量化っぽい。

型演算子・高階多相

型でパラメトライズされた型を作れる。カインドとかが出てくるやつ。

今回のモチベーション的にそこまで関心はないので真面目に読んでいない（ｦｲ

依存型 (dependent types)

項でパラメトライズされた型を作れる。

Curry-Howard 対応では、述語論理に対応する。

「型システム入門」は入門書なので、依存型は「発展」的なトピックの扱いであり、あまり詳しく書いてあるとは言えない。

Lambda Cube

単純ラムダ計算に対する拡張の方向性うち3つ、すなわち、多相型（型に依存する項）、高階型（型に依存する型）、依存型（項に依存する型）を図で表したものを Lambda Cube という。全部入りしたものは Calculus of Constructions (CoC) と呼ばれる。

部分型付けはこれらの拡張の方向性とは独立である。はず。

自分で実装

本を読んでも手を動かさないと身につかないので、実装している。

https://github.com/minoki/LambdaQuest

現時点では、 System F の実装と、 System Fsub の実装がそれっぽく動いている。

自分の言語にどれを取り入れるか

自分で作る言語にどれを取り入れるかという設計の問題は難しい。当たり前だが、無節操に、無制限にどれもこれも入れるのが良い言語というわけではない（型再構築等の良い性質が失われるので）。

• 部分型付けは入れたい。
  • Int <: Real みたいなやつを入れたい。
  • 交差型で関数オーバーロードを実現したい。
  • 整合性は成り立つようにしたい。
• 何らかの多相性を入れたいが、どの程度の多相性を許可するかが問題である。
  • ML 系の言語を参考にするべきか。
• 型クラスみたいな機能も欲しいかもしれない。
  • 「型システム入門」は入門書なので、型クラスのような応用的なトピックについてはほとんど書かれていない。
  • さすがに最初から型クラスを入れるのは言語設計の負荷が高すぎるので、当面は棚上げすることになるだろう。