型安全性とは結局何なのか

2016-12-08 プログラミング

この記事は第2のドワンゴ Advent Calendar 2016 の8日目です。
日付を跨いでいる？またまたご冗談を、DST(ドワンゴスタンダードタイム)ではまだ8日ですよ。

ちなみに前日は…なんと誰も参加登録をしていませんでした！
結構な勢いで埋まってたんですけど、唯一の空きですね。
前々日はdaneko0123さんでした。

一昨年のアドベントカレンダー記事が「関数型プログラミングとは結局何なのか」、去年の記事が「オブジェクト指向プログラミングとは結局なんなのか」ということで、3年目ともなると記事の方向性が固まりつつある雰囲気が漂いつつ、ネタ切れの空気も漂いつつあります。
そもそも去年の時点で既にドワンゴ社員ではないのにアドベントカレンダーには参加し続けている、というのもアレな話ですが。

なにを書くか考えたのですが、最近null安全に関する記事が話題になり、その中で「型」と「安全性」という2つのトピックについて知られていない部分が多そうだと思ったので、プログラムで扱われる「型」とは何か、型が保証する「安全性」とは何か、についてまとめてみたいと思います。

型とは何か

そもそも、型とは何でしょうか。
型システム入門の第1章では、「型システム」について以下のように書かれています。

型システムとは、プログラムの各部分を、それが計算する値の種類に沿って分類することにより、プログラムがある種の振る舞いを起こさないことを保証する、計算量的に扱いやすい構文的手法である。

後半部分の文章は「システム」に関する記述なので、この文章を読む限りでは「型」とは「プログラムの各部分を、それが計算する値の種類に沿って分類する」ためのもの、あるいはそういった「分類」そのもの、ということが言えそうです。
しかし、『この定義は型システムを、プログラムに関する推論のためのツールだとみなしている』ため『プログラミング言語で用いられる型システムに関するものであるという方向性を反映している』とも書かれています。

そこで、そもそもなぜ型という概念が必要になったのか、歴史を簡単に振り返っておきましょう。

ラッセルのパラドックス

やや話が飛びますが、素朴集合論における有名なパラドックスにラッセルのパラドックスがあります。
これは $X = \{ x | P(x) \}$ を「性質 $P$ を満たすものの集合 $X$ 」として定義し、 $x \in X$ を「値 $x$ が集合 $X$ に含まれる」と定義したときに、 $X = \{ x | x \notin x \}$ を満たすような $X$ について矛盾が生じる、というものです。

ざっくり説明すると、 $X$ は「自分自身を含まない集合」だけを集めた集合です。
このときに「 $X$ は $X$ 自身を含む( $X \in X$ )」と仮定すると、 $X$ は自分自身を含む集合なので自身の定義から $X$ には含まれないことになり矛盾します。
逆に「 $X$ は $X$ 自身を含まない( $X \notin X$ )」と仮定すると、 $X$ は自分自身を含まない集合なので自身の定義から $X$ に含まれることになり矛盾します。

このパラドックスは、素朴集合論において集合とその演算に求める条件が弱すぎるために発生します。
現在ではこのパラドックスを避ける様々な方法が知られていますが、ラッセルはそのうちの一つである「階型理論」という体型を著作「プリンキピア・マテマティカ」にまとめました。

階型理論における型

階型理論を完全に説明すると長くなるため、以下では概略のみを説明します。
なお、わかりやすさを優先し未導入の記号や不正確な表現を使用している箇所がありますがご容赦ください。

階型理論の体系として、数( $0, 1, 2, \ldots$ )と、数から再帰的に構築できる集合のみを値として扱うこととし、数の定数として $0, 1, 2, \dots$ を利用することにします。
ここでいう体系とは、どんな数式が許されるかや、それにどのような意味を期待するかを定めたものです。
非常にざっくりいうと、小さなプログラミング言語を設計しているようなものといえるでしょう。

この体系において、以下のような型を考えます。

第0の型: 数( $0$ や $123$ などは第0の型に属する)
第1の型: 数の集合( $\{ 0, 1 \}$ や $\{\}$ などは第1の型に属する)
第2の型: 数の集合の集合( $\{ \{ 0, 1 \}, \{ 2 \} \}$ や $\{ \{\} \}$ などは第2の型に属する)

以降、第3の型、第4の型…も同様に定義します。
C言語などで扱われる「n次配列」と似たような概念である、と考えてもらえれば差し支えないでしょう。
説明のために $\{ \}$ という集合の表記法を使っていますが、この時点では数の定数を導入しただけであり、体系上では「第0の型」以外の値を構築できない(=集合を構築することができない)ことに注意してください。

次に変数を導入します。
変数も同様にいずれかの型に属しますが、型に応じた名前付けのルールを決めることにします。

第0の型の変数: 下付き0の英小文字を用いる( $x_0, y_0$ など)
第1の型の変数: 下付き1の英小文字を用いる( $x_1, y_1$ など)

以降、第2の型の変数、第3の型の変数…も同様に定義します。
つまり、この体系の中では変数の名前を見るだけで、その変数の属する型がわかるようになっています。
そういった意味ではハンガリアン記法に近いものがあるかもしれません。
もっとも、この体系では変数の名前が必ず型を表すため、うっかり名前と実際の型がずれている、というようなことは起こりません。

ここまでで、数を表す定数と、任意の型を表す変数が定義されました。
しかし、このままでは「第0型」以外の値(=集合)を構築する方法がありませんし、値どうしの関係を記述する方法もありません。
これらを解決するため、 $\in$ を以下のように定義します。

$x_0 \in y_1$ : $x_0$ は $y_1$ に含まれる
$x_1 \in y_2$ : $x_1$ は $y_2$ に含まれる

以降、第2の型の変数、第3の型の変数…も同様に定義します。
ここで、 $\in$ の右側に出てくる値の型は、左側に出てくる値の型より必ず $1$ だけ大きくなければなりません。
この制約は「n次配列を含むことができるのは(n+1)次配列のみである」と考えるとわかりやすいでしょう。

例えば $99 \in a_1$ や $x_{123} \in y_{124}$ などはこの体系に含まれる式ですが、 $1 \in a_2$ や $x_{12} \in y_{12}$ などはこの体系には含まれません。
「体系に含まれない」というのは、その体系で解釈できない、つまり構文エラーがあるということを意味します。
数の定数は必ず第0型であり、変数の型は名前から定まるため、式を見ただけで型が合っているかがわかるというのは面白いですね。

後は、式を任意個並べたときに「全ての式が成り立つ」とすれば、任意の集合を構築することができます。
今回はカンマ( $,$ )で区切って式を並べることにしましょう。
以下に例を示します。

　　 $1 \in a_1, 2 \in a_1, 3 \in b_1, a_1 \in x_2, b_1 \in x_2$

この列に含まれる式が全て成り立ち、各変数には式中に定義されていない要素が含まれないとすると、 $x_2 = \{ \{ 1, 2 \}, \{ 3 \} \}$ となります。

パラドックスの回避

さて、この体系でラッセルのパラドックスについて検討してみましょう。

ラッセルのパラドックスでは $X = \{ x | x \notin x \}$ という集合について考える必要がありました。
ここまで考えてきた体系に等価演算子や集合の内包表記などを導入していませんが、仮にそれらを定義していったとして、このような集合を扱うことができるでしょうか。

$x \notin x$ の部分に着目してみます。
ここで $\notin$ は $\in$ の逆で「 $x_0 \in y_1$ : $x_0$ は $y_1$ に含まれない」と定義します。
型に関する制約は $\in$ と同様で、 $\notin$ の右側に出てくる値の型は、左側に出てくる値の型より必ず $1$ だけ大きくなければならないとしましょう。

$x \notin x$ に現れる $x$ には型を示す数字が添えられていないため、このままでは体系に含まれない式であることがわかります。
このため型を示す下付き数字を補う必要があるのですが、仮に第1型の変数であるとした場合、この式は $x_1 \notin x_1$ と書き換えられることになります。
しかし $\in$ は「 $\in$ の右側に出てくる値の型は、左側に出てくる値の型より必ず $1$ だけ大きく」なければならないのでした。
$x_1 \notin x_1$ では左右に出てくる変数の型が同じなので、これは体系に含まれない式であることがわかります。
この理屈は下付き数字がいくつであろうと同じで、結局「自分自身を含まない集合」は体系内では記述しえないことがわかります。

型による性質の保証

このように、階型理論では全ての定数や変数に型を割り当てることで「自分自身を含まない集合」という記述が体系内に現れないことを保証しています。
他に、少し考えると「集合でないものの要素を取る」という記述も現れないことがわかります。
なぜなら、「集合でないもの」は第0型ですが、第-1型は存在しないので $\in$ の右側に第0型を書くことができないためです。
これらをまとめると、「型が整合するならば、ある種の望ましくない記述が現れないことが保証できる」ということができるでしょう。

ここで、節の最初に引用した型システム入門の記述を再掲します。

型システムとは、プログラムの各部分を、それが計算する値の種類に沿って分類することにより、プログラムがある種の振る舞いを起こさないことを保証する、計算量的に扱いやすい構文的手法である。

さきほど定めた体系では、記述のなかの定数や変数と言った「各部分」を、その「種類に沿って分類」したことで、「自分自身を含まない集合」という記述や「集合でないものの要素を取る」という記述といった記述を含まないことを「保証する」ことができたのでした。
この2つの類似性から、階型理論がプログラミング言語の型システムと深い関わりがあること、「各部分を型によって分類することで、ある性質を保証することができる」ということが型システムのもつ重要な側面の一つであることがわかるかと思います。

余談ですが、ラッセルが型を導入することで記述できなくした自己言及を、対角化の技法によって巧みに回避することで「無矛盾な体系が自分自身の無矛盾性を証明できない」ことを証明したのが「ゲーデルの第二不完全性定理」です。
このあたりに興味のある方は数学ガール/ゲーデルの不完全性定理がお勧めです。

型付けと安全性

かなり抽象的な話が続いてしまいましたが、ここからは「小さなプログラミング言語」を定義しながら、プログラミング言語の型について考えていきましょう。
ここでも、基本的にはわかりやすさを優先したり説明を後回しにしていたりするため、曖昧な記述や不正確な記述をしている部分があります。ご容赦ください。

型なしプログラミング言語

定数として 0, 1, 2, ... のみが存在し、以下の演算子のみを持つようなプログラミング言語を考えます。

+: 加算演算子(2つの値を左右に取り、それらの和の値を返す)
=: 等価演算子(2つの値を左右に取り、それらが同一なら 1 を、それ以外は `` を返す)
?:: 三項演算子(3つの値を取り、1つめの値が 1 なら2つめの値を、それ以外は3つめの値を返す)

つまり、この言語では数同士の加算、等価比較、条件分岐を扱うことができます。
各演算子の結合方向は特に定めず、常に () を用いて結合を明示するものとします。
この言語に含まれるプログラムの例をいくつか示します。

123
1+2
(2=2) ? 5 : (3+4)
(1+2) ? (5+6) : (3=4)

最後の例では、おそらく真偽値を期待するであろう1つめの値に加算が記述されています。
しかしながら、このようなプログラムでも構文上は正しいものになっているため、正しいプログラムに含まれることになります。
期待する意味に沿って考えれば、このプログラムを計算した値は `` になるでしょう。
このように型のない世界では、「おそらく人間が期待しているであろう型」と違う値に対しても、計算結果を得ることができてしまいます。

型付きプログラミング言語

先程のプログラミング言語において 0, 1, 2, ... を数値型の値とし、新たに真偽値型の値として true, false を導入します。
各演算子の定義も以下のように「取りうる型」を明示しましょう。

+: 加算演算子(2つの数値を左右に取り、それらの和の数値を返す)
=: 等価演算子(2つの同じ型の値を左右に取り、それらが同一なら true を、それ以外は false を返す)
?:: 三項演算子(1つの真偽値と2つの値を取り、1つめの値が true なら2つめの値を、 false なら3つめの値を返す)

この言語で (1+2) ? (5+6) : (3=4) というプログラムを考えると、 1+2 が数値になるのに対し ?: 演算子は最初に取る値が真偽値でなければならないため、型の条件を満たさず正しいプログラムではないことがわかります。

ここで、この時点の定義においては、プログラムの各部分について「その部分のみを見ただけで型がわかる」ことを覚えておいてください。
例えば (1+2) は 1 が数値型であり 2 も数値型であるため、 1+2 は正しい式であり全体として数値型になる、といった具合です。

変数と型チェック

このプログラミング言語に変数を導入しましょう。

先程の形式的体系では、変数の名前で型が判別できるようになっていました。
これは体系を扱う上では便利な反面、型の数だけ変数名の定義ルールが必要であり、実用上は大変不便です。
そこで、今回導入する変数は任意の英小文字 a, b, ... のみで表記できるものとします。

変数を扱うために、以下の演算子を導入します。

:=: 代入演算子(1つの変数と1つの値を左右にとり、変数の値を書き換えた上で値を返す)
;: 連結演算子(2つの値を左右にとり、1つめの値を評価した上で常に2つめの値を返す)

ここで問題になるのは「変数の型をどのように扱うか」です。
以下の例を考えてみましょう。

x := true; 1 + x

このプログラムでは;の左側の評価により x が真偽値になるため、 1 + x は型エラーになるべきです。
しかしながら、 1 + x という式を見ただけでは x が真偽値であることはわかりません。
これは、先程までと違い x という変数を見ただけでは型がわからず、「xに何が代入されたか」という文脈に依存するためです。

階型理論の体系や、変数を導入する以前のプログラミング言語の定義では、「型が正しい」ことと「文法上正しい」こととを区別せずに扱っていました。
ところが名前で型を区別できない変数を導入したことにより「文法上正しい」だけでは「型が正しい」ことを保証できなくなってしまいました。
これは、構文上正しいプログラムに対して「型が正しい」ことを検査する必要があることを示唆しています。
一般に、このような検査を「型検査」と呼びます。

文法と意味論

型の問題を少しの間だけ忘れて、 x := true; 1 + x というプログラムを実行できてしまった場合を考えましょう。
すると;の左側で x に true が代入された上で 1 + x が評価されることになるので、 1 + true を計算することになります。
しかしながら + は「2つの数値を左右に取り、それらの和の数値を返す」ものと考えていたので、片方が真偽値である場合にどう計算されるべきかがわからなってしまいます。

このことから、「構文上正しい」場合でも「どのように計算されるべきか」が定まらない場合があることがわかります。
一般に、前者を定めるものを「文法」、後者を定めるものを「意味論」と呼びます。
また、「意味論が未定義の計算を行ってしまうこと」を「エラー」と呼び、「型の不整合によるエラー」を「型エラー」と呼びます。

型エラーを起こしたときの挙動は実行系に依存します。
現実的には、ノイマン型コンピュータはデータをバイナリ列で保持しているため、バイナリ列を別の型と解釈した場合の演算が行われることが多いようです。
例えば 1 + true について、 true を実行系では 1 と同じバイナリ列で保持しているのであれば、計算結果として 2 が得られる、といった具合です。

型システムの安全性

先に述べた通り、 x := true; 1 + x は「文法上は正しいプログラム」ですが「型が正しく合わないプログラム」であり、なおかつ「意味論上は型エラーを起こすプログラム」です。
ここで、型検査により「型が正しく合わない」ことがわかれば、「意味が定義されていない」プログラムを検出することができることになります。

一般に、「型検査で正しく型が付けられる」場合に「型エラーが起こらない」ことが保証される場合、その型システムは「健全である」あるいは「安全である」といい、このような性質を「健全性」あるいは「安全性」といいます。
また、安全な型システムを「強い型付け」ともいい、これを備えた言語を「型安全である」「型安全性を備えている」といいます。
逆に、型システムが安全でない場合は「弱い型付け」ともいい、このような言語は「型安全でない」などといいます。

ここで注意が必要なのは、「型エラー」が指す内容は型システムの設計により異なるということです。

例として、配列のインデックスアクセスを考えてみましょう。
インデックスに利用可能なのは整数値ですが、たとえ正しく数値型が使われていたとしても、それが負数や配列のサイズ以上だった場合にはエラーを引き起こすことになります。
一般的な言語では、これは型エラーとはみなされないでしょう。
しかしながら依存型を利用すればこのようなエラーを型検査により検出可能であり、依存型を備えた言語では配列の領域外アクセスを型エラーであると考えられるかもしれません。
つまり、型安全性というのはあくまで「その言語がどのような型システムを持つか」や「その言語でどのような場合を型エラーとするか」に基いて決まる、ということです。
これは、「A言語が型安全である」といった場合と、「B言語が型安全である」といった場合に、その論点がずれている可能性があることを示唆しています。

もう一つの注意点として、型の制約を厳しくすれば型安全性を簡単に達成可能である、ということが挙げられます。
極端な例として、「いかなるプログラムにも正しく型が付けられない」ような型検査を考えてみましょう。
定義からすると、これは「型検査で正しく型が付けられる」場合が存在しない以上、型安全であるといえます。
もちろん、このような型チェックには実用性は一切ありませんし、型の制約を厳しくしなければ型安全性を得られないわけでもありません。
とはいえ、「型安全である」というだけで実用的であるとは限らず、型システムも含めた言語設計全体で判断する必要がある、ということは覚えておく必要があるでしょう。

静的型付けと動的型付け

ここまでで議論した「プログラム記述から(プログラムを実行せずに)型検査を行うこと」は静的型付けともいい、このような型システムを持つ言語を「静的型付け言語」といいます。
これに対し、「プログラムの実行中に、各データに型を識別する情報を付与して逐次型エラーが起きないかを検査すること」を動的型付けといい、このような型システムをもつ言語を「動的型付け言語」といいます。
厳密には、後者は「型付け」をしているわけではないので動的型検査などというほうが正確ですが、一般に使われる語となっています。

動的な型検査では計算する直前のタイミングで具体的な値に基づき型検査を行うため、型エラーをほぼ必ず検出することができます。
これはつまり、動的型付け言語は型安全である、ということです。
少し不思議な感じもしますが、型エラーが「『型の不整合に由来する意味論が未定義の計算』を行ってしまうこと」という定義であることを考えると、実行の直前で検査をして計算を止められる以上、動的型検査では型エラーを起こさないことが保証できる、ということになります。
このあたりは型安全性とは何かにより詳しく書かれています。

まとめ

非常に長くなってしまいました。
ざっくりまとめると、

型とは、階型理論を源流に持つ「ある性質を保証するために、種類に沿って分類する」ためのものである
型安全性とは「型エラーを起こさない」という性質である
型エラーの定義は言語によって異なるので、型安全が指す具体的な内容も言語によって異なる可能性がある
動的言語はその性質上型エラーを起こさないので型安全である

といったところです。
もう少し具体的な各言語の安全性の話や型推論の話も書きたかったんですが、階型理論に字数を割きすぎましたね…

正直なところ、今回書いた内容は(階型理論の話以外は)ほとんど型システム入門の第1章に書かれている内容をまとめ直しただけに近いです。
第1章はほぼ前提知識を必要とせず、しかもオーム社 ebook storeのサンプルで全文が読めるので、興味のある方はこちらを読むことをおすすめします。

型システム入門 −プログラミング言語と型の理論−
	Benjamin C. Pierce 住井英二郎オーム社 2013-03-26 売り上げランキング : 110982

最後にちょっと宣伝です。
年末の冬コミにサークルどろっせるのお手伝いで出展します。
スペースは「3日目土-西も38a」で、自分も開発を手伝っている「にゃんぱす！」という同人検索プラットフォームの展示と有料会員シリアルコードの販売を行う予定です。
また、開発小話をまとめた技術同人誌を(書くのが間に合ったら)こっそり頒布させていただこうと思っています。
もし3日目にコミケ来られる方がいたら、ついでにお立ち寄りいただけますと幸いです。

完全に遅刻してますが、DST(ドワンゴスタンダードタイム)的にはまだ8日のはず…
というわけで、明日の担当は @viviljp さんです。お楽しみに！