TechFULの中の人

TechFULスタッフ・エンジニアによる技術ブログ。IT関連のことやTechFULコーディングバトルの超難問の深掘り・解説などを紹介

プログラムの「型」を支える理論

プログラミング言語における重要な概念の一つに、「」があります。

しかし型という概念は、プログラミング言語において必須ではありません。
それにもかかわらず多くの言語に型が備わっているのはなぜでしょうか?

この記事ではその理由や、型を支える理論について手短に説明します。

用語の整理

そもそも型とは

プログラミング言語における型とは、データを役割で分類したときのその種類を区別するものです。

例えば C++ では 3 は int 型、"TechFUL" は string 型などです。勿論これらは言語に依存します。

後述しますが、このような基本的な型は基底型と呼ばれます。

それだけではなく、「整数を受け取って整数を返す関数」であれば int→int 型のように、基底型を複合した型も存在します。

静的/動的型付き言語

プログラミング言語を型の仕様で大まかに分類してみましょう。

  • 静的型付き言語(Java, Rust, C++ など)
  • 動的型付き言語(Scheme など)
    • 実行時に型を付与する言語です。
  • 型を持たない言語(シェルスクリプトなど)
    • 上2つ以外に、そもそも型を持たない言語もあります。

(実際には静的型付けと動的型付けが混在していることも多々あるため、参考程度に留めてください)

この記事では静的型付き言語のみ扱います。

言語の安全性

言語が安全であることを正確に定義するのは難しいですが、言語の安全性とは、一言で言えば「不正な動作を許さない」性質です。

例えば配列外への書き込みを行った際に未定義動作を発生させる言語は安全ではありません。
このような言語では、意味のないプログラムがどう振る舞うのかを完全に理解するためにはメモリやコンパイラの内部までをも知る必要があり、現実的ではありません。

特に C や C++安全な言語ではありません何故なら配列外参照などの未定義動作が除外されないからです。
一方で JavaC#、Rust などは安全な言語です。

言語の安全性を担保することが、(静的)型システムを導入する大きなモチベーションとなっています。

注意点として、言語の安全性は後程述べる型安全性とは異なります。実際先述の動的型付き言語Schemeは静的型システムを持ちませんが、安全な言語です。

型システム

型システムとは

型による分類を用いて、プログラムがある種のバグを起こさないことを理論的に保証する形式手法を型システムと呼びます。

型システムではプログラムにどのような型がつくのかを静的に解析し、型がつかないプログラムを排除します。つまり「型がつく」=「(特定の)バグが存在しない」です。

ある種のバグを「起こさない」ことを保証するという点で、型システムは保守的です。つまりバグを「起こさない」ことは証明できても「起こす」ことは証明できません。それ故に、正しく振る舞うであろうプログラムを排除してしまうこともあります。

さらに全てのバグをカバーできるというわけではなく、あくまでもある側面の安全性を保障しているだけです。


しかし型システムを導入するメリットは、それらのデメリットより遥かに大きいです。

型システムでできること
  • バグ検出

最も基本的であり、かつ強力です。
例えば 1 + "abc" のような意味のないプログラムを、実行せずとも排除することができます。静的に解析できることから、早期のバグ発見が可能となります。

この例は明らかですが、より複雑に絡み合ったプログラムにおいて型によるバグ検出は大きな助けとなります。

さらに型が適切に設定されていれば、大きな仕様変更の際、実際にコンパイラにかけることで変更箇所の目途を付けることも可能です。

  • 安全性

型システムによる静的解析は、先程述べた言語の安全性を守る大きな役割を果たしています。

実際は、型による検査だけではゼロ除算などを防げず不十分であるため、適切なタイミングで実行時エラーを出す等の手法と組み合わせて使われます。

  • ドキュメント化

プログラムのドキュメント(プログラム中のコメント含む)はしばしばプログラムより古くなり、整合性が崩れることがあります。

それに対し型は現在のプログラムの状態をそのまま反映しており、プログラムを読み書きする人間が振る舞いを理解する助けとなります。

  • 抽象化

大規模なソフトウェア開発においては、特定機能を持ったひとまとまりの部品(モジュール)をまず作成し、その後それらを組み合わせるという手法がよく用いられます。

その際型はモジュールのインターフェイスとして、モジュールの機能を要約する形で現れます。

インターフェイスが明確であれば、設計の段階においてモジュールの具体的な実装を考えずに抽象的な設計をすることができます。このように型は抽象的で、かつ洗練された設計を手助けする役割を担っています。

単純型付きラムダ計算

導入

多くのプログラミング言語の型システムの土台となっている単純型付きラムダ計算をご紹介します。


無しラムダ計算は、簡単に言えば名前を持たない関数を扱う計算体系です。

例えば「整数を受け取り、1 を足す関数」は、通常の記法であれば f(x) :=x+1 のように f という名前をつけて記しますが、型無しラムダ計算では  
 {\lambda x. x+1 } のように記します。


単純型付きラムダ計算は、関数のみから成るシンプルな型無しラムダ計算に型を付与したものです。

文字通り関数のみであるため、数や真偽値(true, false)などは存在しません

これでは何の意味もないかのように思えますが、Church 数Church ブール値と呼ばれる関数によって数や真理値を表現することができるので、純粋なラムダ計算のみでもこれらは扱えます。
(ですがより直接的に扱える方が便利なため、定義に組み込むことも多々あります。このように型システムでは、より複雑な型システムを構成するために、項や型の定義を「拡張」することがしばしば行われます。)

  \mathsf {\lambda x:T. x } (型   \mathsf T の引数   \mathsf x を受け取り、  \mathsf x をそのまま返す関数)といった具合に、引数に型注釈をつけて書きます。

関数への適用はすべて前置記法で記します。つまり f(3) ではなく (f\ \ 3) のように書きます(単純型付きラムダ計算に数はないので参考として)。


型と項は、より正確には次のように定義されます。

型:

\mathsf  {T := A \mid T \rightarrow T }
(ただし \mathsf A は int や string などの基底型

項:

\mathsf  { t := x \mid (\lambda x:T. t) \mid (t\ t)}

括弧は適宜省略します。
定義が再帰的になっていることに注意してください。(似たような記法であるBNF記法はTechFULでもしばしば出題されます!)

直観的には、型は基底型を型構成子→で組み合わせたもの、項は関数とそれへの適用を組み合わせたものです。

さらに項のうち \mathsf  { \lambda x:T . t } の形をしているものをといいます。


ラムダ計算の項は、プログラムに対応しています。
プログラムに対応するということは、それを実行し、計算するということも考えられそうです。

項を別の項に変換する操作を評価といい、項  \mathsf t \mathsf t' に1ステップで評価されることを  \mathsf {t \longrightarrow t'} と書きます。

もちろん、どのような項にでも変換できるという訳ではありません。
項の評価はあらかじめ定められた評価規則に従って行います。

評価規則は次の3つです。

ここで  \mathsf {t_i} は項、 \mathsf {v_i} は値です。

上2つは「横線の上側が成り立つならば、下側が成り立つ」という意味です。

最後の   \mathsf {  [x \mapsto v_2 ] t_{12} } は、 \mathsf t_{12} 中に出現する束縛されていない*1  \mathsf x を全て  \mathsf v_2 に置き換えた項を表します。


ある  \mathsf {t_1,t_2,\dots,t_n} が存在して  \mathsf{s \longrightarrow t_1 \longrightarrow t_2 \longrightarrow \cdots \longrightarrow t_n \longrightarrow t} となるとき、 \mathsf {s \longrightarrow^* t } と書きます。

この評価規則からわかるように、値と呼ばれるラムダ項はそれ自体意味のあるプログラムであり、かつそれ以上評価できません。これが「値」と呼ばれる所以です。

なお、評価規則では型の情報を全く使っていません。これは型を使わずともプログラムの実行自体は可能である、という事実に対応しています。


そして最後に、項に型を付けるための型付け規則があります。
型付け規則では、文脈という変数と型の対応の列を用いた規則が用いられます。

文脈という概念を導入するのは、同じ項であっても、その内部に現れる自由変数の型によって全体の型が異なるからです。
これは、「a+b」という式の型がa,bの型に依存することに似ています。a,b がともに int 型であれば int 型ですし、ともに string 型であれば string 型でしょう。a,b の型が異なるなら型付けできません。

「文脈  \mathsf \Gamma のもとで項  \mathsf {t} は型  \mathsf {T} を持つ」ということを  \mathsf {\Gamma \vdash t:T} と表します。

型付け規則は次の3つです。

以上が、単純型付きラムダ計算の構成要素です。

「おかしくないプログラム」とは

プログラムが「おかしくなる」という概念を、型システムにおいても導入してみましょう。

イメージとして、例えば三項演算子を持つプログラミング言語のプログラムにおいて「("abc" ? 0 : 1)」のような式があったとしましょう。
これは条件部が真偽値でなく評価できないにもかかわらず、値ではありません。このようなプログラムは「おかしいプログラム」であると見なしてよいでしょう。

このような推察から、おかしいプログラムに対応するラムダ項は「それ以上評価できないが、値ではない項」であると特徴付けられます。
裏を返せば、「おかしくないプログラム」は、型システムにおける「値に評価される項」であるといえます。

型安全性

ここまではずっと単純型付きラムダ計算の定義を述べてきましたが、ここから本題となる定理を見ていきましょう。

単純型付きラムダ計算において評価の関心のある項は、自由変数を含まない、閉じた項です。何故なら完全なプログラムは常に閉じているからです。
そして正しく型付けされた閉じた項、つまり  \mathsf {\emptyset  \vdash t:T} なる項  \mathsf t に対し、次の定理が成り立ちます。


定理(型安全性)
 \mathsf {\emptyset  \vdash t:T} ならば、ある値  \mathsf v が一意に存在して  \mathsf {t \longrightarrow ^* v}.


型安全性は型システムの最も基本的な性質です。

この定理は正しく型付けされた閉じた項が値に評価されること、つまり「正しく型付けされたプログラムはおかしくならない」ことを意味しています!*2

これにより、型システムはバグがないことを理論的に保証する強いツールとなっているのです。

数理論理学との繫がり

ここまでは主にプログラムの話題についてお話ししました。

型システムはプログラミング言語の理論としての側面に加え、論理や証明を定式化する数理論理学という分野とも深いつながりがあります。

驚くべきことに、型システムにおけるプログラム(項)と数理論理学における証明には以下のような直接的な対応があります。これを Curry-Howard 同型対応と呼びます。

ここでの論理は直観主義論理(古典論理から排中律を除いたもの)です。

つまり命題 P の証明を直接書かずとも、それに対応する型を持つ項が存在することを示せば、P が正しいと示せるのです。

一見関連性があるようには見えない証明とプログラムの間にこのような非常に強いつながりがあることは興味深いです。


さらに型システムを拡張することで、対応する論理体系も拡張されます。
例えば System F と呼ばれる型システムは型の量化を許しますが、これは述語の量化を許す二階述語論理に対応しています。

終わりに

「型」という概念はプログラマにとって非常に身近な存在ですが、その背景には緻密で広大な理論があり、それにより我々は型の恩恵を得ることができます。

普段はあまり意識することはないかもしれませんが、プログラムを読み書きする際に型がどのように使われているのかを観察することでより良いコーディングが可能となるでしょう。

参考文献

[1] Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002, 648p.

*1:一言でいうと  \mathsf {\lambda x.} 部に現れる変数が束縛変数、それ以外が自由変数です。厳密な定義は書ききれなかったため割愛させていただきます…

*2:余談ですが、Robin Milnerによる型システムを提唱する論文の冒頭に型システムの説明としてほぼ同じ文章があります(well-type programs cannot “go wrong” )。