Flutterに採用されているDartでは、void型に好きな値を代入することができます。
void main() { void x = 2; }
型が値を定める言語に慣れていると、これは奇妙に思えます。しかし、型が振る舞いを定める言語であると思うと、これが自然と感じられるようになります。
ついでに、Dart 2の型の仕様書を読んでDartの型の上下を解説します。
と思って読んでたんですが、この仕様書はかなり不完全ですね‥。 Never型のこととかどこにも書かれていなかった‥。
void型の振る舞い
型が値を定める言語では、voidは値の存在しない型となっています。そのため、voidの関数から値を返そうとするとコンパイルエラーになるし、void型の変数は存在できません。
Dartでは、void型は何の振る舞いもできない型となっています。任意の値は振る舞いをしない型として振る舞うことが可能です。そのため、Dartでは任意の値をvoid型に代入することができます。
一度void型に落ちた型は他の型に型変換ができなくなります。
Dartの型の一覧と仕様書の読み方
void型が任意の値を代入できるということを仕様書から読み解きます。
このときに、記号を3つほど知っている必要があります。
型S <: 型T は「型Sは型Tの派生型」であると読みます。また、派生型Sは元の型Tへ代入可能です。
記号の向きを忘れがちなのですが、|型S| < |型T| であるという雰囲気を感じ取りましょう。
型環境Γ |- 命題P は 「型環境Γにおいて命題Pを示せる」と読みます。
上下に命題が書かれた長い横棒は「上から下が導出できるとする」と読みます。
次の導出木は、上に何も書かれていないので、いつでも成り立つということを述べています。
つまり、任意の型Sは任意の型Sとして振る舞うことができると言っています。当然ですね。
Object型 Dynamic型 void型
Object型 Dynamic型 void型は任意の値を代入できます。それぞれの実際の振る舞いは型の導出木には現れていません。
Object型は==ができます。
Dynamic型は何でもできる型です。 動的に様々なチェックがなされます。
void型は何もできない型です。 何かをするとコンパイルエラーです。
⊥型(ボトム型)
数学には現れにくいが、計算機科学だと頻出する⊥型です。
⊥型はループや例外などにより値を返さない関数につく型です。
例えば、「intを受け取って⊥を返す関数」は実際には値を返しません。 値を返さない関数は「任意の型を返す関数」として、型推論時は振る舞うことができます。
⊥型を明示的にコード内で記述する場合は Never が使えます。
Null型
Null型は⊥型以外のすべての型の派生型であると述べています。
ですがこれは悲しいので、null-safetyモードの場合はObject?の派生型でしかなくなるようです。
