wassup?

プログラミング、ボドゲ、ボカロ

Dart 2の型を読む・void型に代入できる値とは?

Flutterに採用されているDartでは、void型に好きな値を代入することができます。

void main() {
  void x = 2;
}

型が値を定める言語に慣れていると、これは奇妙に思えます。しかし、型が振る舞いを定める言語であると思うと、これが自然と感じられるようになります。

ついでに、Dart 2の型の仕様書を読んでDartの型の上下を解説します。

と思って読んでたんですが、この仕様書はかなり不完全ですね‥。 Never型のこととかどこにも書かれていなかった‥。

仕様書 Dart 2.2

void型の振る舞い

型が値を定める言語では、voidは値の存在しない型となっています。そのため、voidの関数から値を返そうとするとコンパイルエラーになるし、void型の変数は存在できません。

Dartでは、void型は何の振る舞いもできない型となっています。任意の値は振る舞いをしない型として振る舞うことが可能です。そのため、Dartでは任意の値をvoid型に代入することができます。

一度void型に落ちた型は他の型に型変換ができなくなります。

Dartの型の一覧と仕様書の読み方

void型が任意の値を代入できるということを仕様書から読み解きます。

このときに、記号を3つほど知っている必要があります。

型S <: 型T は「型Sは型Tの派生型」であると読みます。また、派生型Sは元の型Tへ代入可能です。

記号の向きを忘れがちなのですが、|型S| < |型T| であるという雰囲気を感じ取りましょう。

型環境Γ |- 命題P は 「型環境Γにおいて命題Pを示せる」と読みます。

上下に命題が書かれた長い横棒は「上から下が導出できるとする」と読みます。

次の導出木は、上に何も書かれていないので、いつでも成り立つということを述べています。

f:id:wass80:20210408132757p:plain

つまり、任意の型Sは任意の型Sとして振る舞うことができると言っています。当然ですね。

Object型 Dynamic型 void型

f:id:wass80:20210408132945p:plain

Object型 Dynamic型 void型は任意の値を代入できます。それぞれの実際の振る舞いは型の導出木には現れていません。

Object型は==ができます。

Dynamic型は何でもできる型です。 動的に様々なチェックがなされます。

void型は何もできない型です。 何かをするとコンパイルエラーです。

⊥型(ボトム型)

f:id:wass80:20210408133414p:plain

数学には現れにくいが、計算機科学だと頻出する⊥型です。

⊥型はループや例外などにより値を返さない関数につく型です。

例えば、「intを受け取って⊥を返す関数」は実際には値を返しません。 値を返さない関数は「任意の型を返す関数」として、型推論時は振る舞うことができます。

⊥型を明示的にコード内で記述する場合は Never が使えます。

Null型

f:id:wass80:20210408133426p:plain

Null型は⊥型以外のすべての型の派生型であると述べています。

ですがこれは悲しいので、null-safetyモードの場合はObject?の派生型でしかなくなるようです。

understanding null-safety