Arantium Maestum

プログラミング、囲碁、読書の話題

型コンストラクタは型なのか

ツイッターで型コンストラクタが型かどうか?という話があり、ツイートで少し書いたのだがもうちょっとまとめてみる。

TaPLにおける定義
  • 型コンストラクタと型はまったく同じ概念を指す言葉である
  • 型はカインドを持つ
  • カインド*の型を真の型と呼び、これらは0引数の型コンストラクタである
OCamlにおける定義
  • 型とは型コンストラクタの一種であり、特に0引数のものを指す
  • 型コンストラクタはすべてカインドを持つ
  • 型(すなわち0引数の型コンストラクタ)はカインド*である
  • 型コンストラクタは引数としては型をとり、返0以上の引数をもつ型コンストラクタを返す

(まったくの門外漢だけど、Haskellでの定義はTaPLに近い印象)

概念レベルでは食い違っていない。TaPL「真の型と型」とOCaml「型と型コンストラクタ」と呼び替えているが、結局「すべてを統一的に扱えるような概念を導入する」ということがポイントで、概念の切り分け方は同一。

これら概念の説明・習得の流れを考えると:

  1. 「型というのは値の集まりを指すんだよ、例えばintとかboolとか」「なるほど」
  2. 「型に対してパラメトリックな型コンストラクタというものが考えられるよ、例えばlistやoptionとか」「たしかに」
  3. 「型コンストラクタは型を受け取り型を返す関数だと認識できるよ」「あー、まあそうか」
  4. 「実は型コンストラクタこそが型だよ。今まで型だと呼んでたのは0引数の特殊例」

ここで聞いている人が「は?1引数以上の型コンストラクタは何の値の集まりにも対応していないけど?あと(OCamlの)型コンストラクタに引数として渡せないけど?」となるか「あーなるほど、これだと型の世界をラムダ計算で統一的に扱えるな」となるか、がポイントなのかもしれない。

型理論の専門家ではない人も多いOCamlユーザコミュニティ内では4まで行かないのが賢明な気はする。

その反面、型理論の中では「型コンストラクタの世界でラムダ計算が云々」とやるより「型の世界でラムダ計算が云々」という話にしたほうがずっとスッキリする。