🪴 Quartz 4.0

Search

SearchSearch

「名前的型システムと構造的型システムの違い」加筆案

Dec 01, 2023, 14 min read

いきさつ

おさらい image

  • メモリに0と1が並んでいるだけでは、それが整数なのか浮動小数点数なのかわからない。
  • そこでint n;などと宣言することで「これは整数だよ」という情報を変数につけるのが静的型付け
  • 「この値は整数だよ」という情報を値につけるのが動的型付け
    • (余談: 「これは型付けではない、動的検査と呼ぶべきだ」と考える人もいるが、読者が目にする確率の高い用語を優先している。参考: 動的型付けは動的検査)

P.129 「動的型付け > メリットとデメリット」ではこう書いた。

  • このような方法で値の種類を扱うことで、従来の静的型付け言語ではできなかったような柔軟な処理ができるようになりました。実行時まで型を決めないことや、実行時に型が変わることが可能になったのです。しかし、これはデメリットでもありました。静的型付け言語は、コンパイル時に型が決まり、コンパイル時に型の整合性がチェックされました。この型チェックのおかげで、一部のバグには実行する前に気付くことができました。しかし動的型付け言語ではそれができなくなってしまいました。

このデメリットを解決したいというニーズが高まった。特にJavaScriptでそのニーズが強かった。

  • Flashが衰退したことによって、ブラウザ上で高度なユーザー体験を提供するニーズがJavaScriptで解決されるようになり、JavaScriptで大規模なプログラムが書かれるようになった。
  • JavaScriptの多くはユーザの手元のブラウザ上で実行される。そのため、プログラマの手元で実行されるプログラムに比べて、問題が起きた時に事後的に情報を収集して問題を解決することが難しい。事前に問題に気づきたい。
  • ブラウザ上で動くJavaScriptは、グラフィカルな表示をし、ユーザからの入力を受け付けることが多い。ユーザはプログラマの予想外の操作をすることも多い。また人間とのやり取りを含む手順はテストの自動化が難しい。

このデメリットを解消するアプローチは2つある。

  • A: 既存の言語に、処理に影響を与えない形で型の情報を付け加えて、それを使って静的検査をする。
  • B: 静的型付けの言語でプログラムを記述し、それを動的型付けの言語に変換する

Aのアプローチ

  • 例えば動的型付け言語のPythonでは2015年に型検査が標準ライブラリとして提供された。言語自体は動的型付けのままだが、型の情報を付け加えることができ、その情報に矛盾する扱いがあった場合に警告する仕組みだ。
  • JavaScriptにおいては2009年にリリースされたGoogle Closure Compilerがこのアプローチを採用した。JavaScriptとしての実行に影響のないコメントの形で関数の引数や返り値の型を宣言する。コンパイラはコメントが付与されたソースコードを読んで、型検査を行う。
    • (GoogleがどんなサービスにGoogle Closure Compilerを使っていたかわかれば加筆する)
      • Gmail, Google Calendar, Google Maps, Google Docs
    • 例えばサイボウズのkintoneの実装には、2012年時点で10万行のJavaScriptのコードがあった。これに対する型検査はGoogle Closure Compilerが使われていた。

Bのアプローチ

  • 2005年にHaxeがリリースされた。2011年にGoogleによってDartがリリースされた。翌2012年にはMicrosoftによってTypeScriptがリリースされた。
  • この3つ以外にもたくさんの言語が作られたが、ここでは説明しない。

「静的型付け」は一枚岩ではない

「静的型付けの言語でプログラムを記述し、それをJavaScriptに変換する」の「静的型付け」の部分は、言語によって異なる。Dartは2011年にリリースされたが、2018年に型の仕組みを変えて再リリースされた。また「静的型付け」という言葉で「Javaみたいな型付けの仕組み」と連想されやすいが、これは必ずしも正しくない。

2014年にこの本を書いた時には「動的型付け v.s. 静的型付け」のシンプルな構図で説明できた。2019年現在、かつて「静的型付け」の一言で済まされていた概念が、より細かく分かれていく過渡期にある。Pythonのように、動的型付け言語が事後的に静的型検査を手に入れる例もある。そして「静的型付け」の中に、新たな対立構図「名前的(nominal) v.s. 構造的(structural)」が生まれている。 image

  • (2014年時点に構造的型の言語がなかったわけではなくて、OCamlとかScalaとかがあった。しかしOCamlを使う人はML系言語の型システムについては当然よく知っていて、Javaと混同したりはしなかった。Scalaを使う人はJavaの型システムに不満があって、あえてScalaを選んでいた。今のような「Webのフロントエンドを実装しよう」というシチュエーションの人がDartとTypeScriptを目の前にしてどちらを選ぼうと悩む状況ではなかった。この2つの言語の型システムを「静的型付け」と呼んで同一視すると混乱する。分けて語るための語彙を持つ必要が生まれている。)

名前的型システムと構造的型システムの違い

型Aが求められている文脈で型Bを使うことができるのはどのような場合か？

例えば型Aの変数xに型Bのオブジェクトを代入できるのはどういう場合か？ :

A x;
B y = new B();
x = y;  // OK? NG?
  • (言語にあらかじめ用意されている型には暗黙の型変換など特殊なルールが追加されていることがあるので、ユーザ定義の型に限定した方が良いかも。例えばDart 2.1以降はdouble z = 1;がOK、それ以前はNGだった。こういう挙動の差はここでの本題ではない)

名前的型システム(nominal type system)の言語では、型には名前がついている。たとえ構造がまったく同じでも、名前が違えば違う型である。下記のコードでは、T1とT2は構造がまったく同じなのに、代入するとエラーになる。

Dart

class T1 {
  num x;
}

class T2 {
  num x;
}

void main() {
  T1 a;
  T2 b = new T2();
  a = b;  // ERROR: A value of type 'T2' can't be assigned to a variable of type 'T1'.
}

この種の型システムでは、明示的に「型T2は型T1の部分型(subtype)だ」と宣言することで、T1が求められる文脈でT2を使うことができるようになる。下記のコードではextendsが部分型の宣言にあたる。 Dart

class T1 {
  num x;
}

class T2 extends T1{  // 明示的に「T2はT1の部分型」と宣言した
  num x;
}

void main() {
  T1 a;
  T2 b = new T2();
  a = b;  // OKになった
}

一方で、構造的型システム(structural type system)の言語では、型がどういう構造を持っているかで判断をする。型には名前がついているとは限らないし、たとえ名前が違っても、構造が同じならば互換性があるものとして扱われる。

TypeScript

type T1 = {
    x : number
}

type T2 = {
    x : number
}

let a:T1;
let b:T2 = {x: 1};
a = b; // OK

このコードのlet b:T2 = {x: 1}の、{x: 1}の部分は名前のないオブジェクト型である。 これはT1ともT2とも同じ形をしているので、エラーになることなく代入できる。

1985年に生まれたC++や1995年に生まれたJavaは名前的型システムを採用していた。この2つの言語はとてもメジャーになったので、extendsやimplementsで部分型関係の宣言をすることに慣れ親しんだ人も多いだろう。一方、型理論の研究においては構造的型システムの方が主流だった。その結果、JavaScriptを生成するための静的型付け言語を設計する際に、Javaなどを参考に名前的型システムを採用した言語と、型理論を参考に構造的型システムを採用する言語が混在することになってしまった。

  • (名前的型システムには、部分型かどうかの判定処理が軽いメリットがあった。しかしJava誕生から25年も経つ現在、コンピュータの性能も大きく進歩したため、名前的型システムを選ぶ理由にはならないのではないか。それよりも、Javaに慣れ親しんだ人がたくさんいる、という歴史的経緯が大きいのではないか。)

    • (この辺りはあまり確定的なことが言えないから削っても良いかも)

  • (Javaは2004年にジェネリクス(総称型)の機能を採用した。これは名前的型だったJavaが構造的型とのハイブリッドに進む方向なのだが、それをページを割いて説明するかどうかは要検討)

「名前的型システムと構造的型システムの違い」加筆案メモ

Graph View

Backlinks