京都大学大学院 情報学研究科 通信情報システム専攻 修士2回生の五十嵐雄です．大学では，プログラミング言語理論，その中でも特に型システムの研究をしています．
この記事では，私が特に力を入れて研究している漸進的型付けという種類の型システムについて紹介します．プログラムや型システムといった基本的な概念から解説していくので，プログラミング経験のない人も安心して読み始めてもらえたらと思います．
目次
はじめに
プログラムとはコンピュータへの命令を記述したものです．2018年現在，私たちの生活は数多くのプログラムに支えられています．
あなたがこの記事を Windows が入ったパソコンで見ているなら，まずその Windows がプログラムです．お家にテレビや冷蔵庫があれば，それらの中にもプログラムが内蔵されているでしょう．空いた時間にスマートフォンでゲームをするなら，遊んでいるゲームも全てプログラムです．
バグ: プログラムの誤り
プログラムのほとんどは，人間が書いたものであるか，人間が書いたものをコンピュータが解釈できるように変換したものです．願わくば，いつでも正しいプログラムを書きたいものですが，人間は間違いを犯す生き物ですから，その人が意図しない命令をコンピュータに与えてしまうことがあります．
これは，数学の試験で間違った答案を提出してしまうのによく似ています．自分は正解だと確信しているのにバツがついて答案が返ってきたという経験は誰しも一度はあるでしょう．プログラムを書いていても，同じことが頻繁に起こります．そのようなプログラムの誤りのことをバグと呼びます．
試験で間違った答えを書いたとしても，ちょっとばかり悪い点が返ってくるだけで済みますが，プログラムのバグはもっと深刻です．例として，飛行機のコックピットのプログラムを考えてみましょう．このプログラムは，着陸ボタンを押したらタイヤを出すといった，飛行機の基本的な動作を制御することを意図して作られたものだとします．
さて，非常に安直ですが，このプログラムに「着陸ボタンを押してもタイヤが出ない」というバグが混入したらどうなるでしょうか．たちまち数百人の命がかかった一大事に発展しますね．前述の例は少し極端ですが，現代のプログラムは，大勢の命や大金が関わる場面にもたくさん用いられています．プログラムのバグはできる限り少なくしなければなりません．
バグを防ぐために
さて，どうしたらバグを防げるでしょうか．みんなで何度もプログラムを見直しすれば良いでしょうか．しかし，考えてみてください．自分の数学の答案をクラス全員で見直して，本当に全部の間違いがなくなったと言い切れるでしょうか．少なくとも，私はあまり自信を持てません．
プログラムのバグも同じことです．人間が特に決まりもなく見直しをする限り「絶対」はありえません．バグのない安全なプログラムを書くには，プログラムを検査し，バグがないことを保証する手段が必要なのです．
私の研究領域である型システムは，まさにそうした要求を達成するためのものです．非常に大雑把に言うと，型システムとはプログラムにある種のバグがないかを検査するシステムのことです．
検査のルールを数学の言葉を使って定義することで，プログラムのある種の安全性を数学的に証明します．例えば「型システム A の検査を通過したプログラムにはある種のバグが存在しない」といったことが数学的に証明できます．
繰り返し「ある種の」という補足をしているのは，プログラムのバグや安全性に様々な種類があり，多くの型システムはその一部の側面にのみ着目するからです．
このような数学に裏打ちされた技術は，現代のプログラミング言語のほとんどに備わっています．世の中には様々なプログラミング言語がありますが，それぞれの言語ごとに専用の型システムが開発されており，安全なプログラムを記述できるように工夫がされています．
多くのプログラミング言語は，プログラムの実行中やプログラムをコンピュータが理解できる命令に変換する過程で，自動的に型システムを動作させプログラムのバグを発見するため，誰でも簡単に型システムの恩恵を得られるようになっています．
この記事について
この記事では，私が研究している「漸進的型付け」という特殊な型システムの話をします．流石に，定義を出して証明を始めるというのは乱暴ですから，研究の前提知識や背景，概要といったストーリーに重点を置いて解説をしていきます．プログラミングに馴染みのない人のために，例え話も交えながら進めていきます．
まず，次の2章では，型システムについてもう少し詳しく解説をします．3章では既存の型システムの問題を述べます．4章では，3章の問題をもとに筆者の研究対象である漸進的型付けについて説明します．5章で筆者が第一著者として執筆した論文を少しだけ紹介して，6章でまとめとします．
導入: 型システム
ここでは，型システムの概要を説明します．
型システムの概要
プログラム上で扱えるデータには様々な種類があります．整数，小数，文字，文字列など，挙げていったらキリがないほどです．型とは，このデータの種類のことです．例えば，42 の型は整数型，”abc” の型は文字列型です．
型システムとは，この型に基づいてプログラムを検査し，バグがないかを調べるシステムのことです．型システムによる検査を型検査と言い，型検査を行うことを「型を付ける」と言ったりします．
例として，典型的な足し算 (+) の型検査を見てみます．この + は整数の足し算のみに用いられるもので，整数以外のデータを与えるとおかしな動作（つまりバグ）を起こすとしましょう．
まずは，型検査でバグがないと判断される例として，3 + 5 というプログラムを考えます．+ は整数型のデータを二つ受け取ります．そして，3 も 5 も整数型です．+ に渡したデータの型と，+ が要求する型が一致しているので，型システムはバグがないと判定します．
次に，型検査でエラーとなる例として，”abc” + 42 というプログラムを考えます．+ は整数型のデータを二つ受け取ります．しかし，”abc” が文字列型です．+ に渡したデータの型と，+ が要求する型が一致していないので，型システムはバグがある（かもしれない）と判定します．
「かもしれない」と書いたのは，一般に型システムは，バグが存在しないのにバグがあると誤認識してしまう可能性があるからです．これは研究者や技術者がサボっているわけではなく，解決できない問題であることが理論的に知られています．
型システムの二大分類
世の中に型システムは数多くありますが，これらは大きく二つに分けられます．一つは，静的型付けの型システムです．これは，プログラムの実行前に型検査を行う型システムのことです．もう一つの分類は，動的型付けの型システムです．これはプログラムの実行中に型検査を行う型システムのことです．
これらにはそれぞれ長所と短所があり，相補的な関係にあります．私の研究を理解するのには欠かせない内容なのですが，ちょっと難しい話なので，しばらくたとえ話で進めていきます．
架空の「静的型付け市」と「動的型付け市」という市を考えましょう．それぞれの市には「市民に生年月日を書いた書類を提出してもらう」という仕事があり，市の名前の型システムとそっくりな形式で仕事をしています．まずは静的型付け市の様子を見てみましょう．
静的型付け市では，書類の内容を事前に検査する機械を導入しており，機械の検査を通った書類しか受け取らないことにしています．機械はとても優秀で，年が西暦で書かれているか，数字のみが使われているかといった様々な条件を確認します．
担当者は，提出される書類が機械の検査を通っていることを知っているので，次々にハンコを押して受理していくだけでよく，素早く仕事を済ませることができます．ただ，機械は融通が利かず，漢数字や汚い字を一切受け付けてくれないので，一部の市民からは不満の声も上がっています．
さて，一方の動的型付け市は，機械を使わず，市の担当者が書類の検査と受理を行なっています．動的型付け市の担当者はとても親切で，漢数字や汚い字で書いてあったとしても，担当者が読めると思えば受理してくれます．修正が必要な場合は，その場で手続きをストップして市民に修正するように促します．
市民は，生年月日の形式を気にしなくてよく，適当に書いても書類を受理してもらえるので負担が少ないです．ただ，書類を人手で検査するのに時間がかかるため，待ち時間が長いという苦情が時折寄せられています．
一旦，たとえ話から型システムの話に帰って来ましょう．上のたとえ話では，市民の提出する書類がプログラム，市役所の担当者がコンピュータ，書類の受理作業がプログラムの実行，書類の検査が型検査にそれぞれ対応しています．以下に静的型付けと動的型付けの説明・長所・短所をまとめます．括弧の中には対応するたとえ話を再掲しています．
- 静的型付け
- 説明
- プログラムの実行前に型検査を行い，型検査を通過したプログラムしか実行することができない（市民が提出した書類を事前に機械で検査し，市役所の担当者は機械の検査を通過したプログラムしか受け取らない）
- 長所
- プログラムを事前に型検査するため安全性が高い（書類を事前に機械で検査するので，読めない書類を誤って受理してあとの処理ができないといった自体が起こらない）
- コンピュータは型システムの検査の結果を利用してプログラムを高速に実行できる（担当者は，書類が機械の検査を通過したことを知っているので，ハンコを押すだけで素早く仕事を終えられる）
- 短所
- 型システムの検査を通過するまでプログラムを実行することができず開発が難しい（機械の検査を通過するまで書類を受け取ってもらえないので手続きが難しい）
- 説明
- 動的型付け
- 説明
- プログラムの実行中に型検査をする（市役所の担当者が書類の検査を行う）
- 長所
- 事前に型検査をしないので，すぐにプログラムを実行して試すことができる（機械による検査をしないので，すぐに書類を担当者に渡して手続きを進めることができる）
- 短所
- プログラムの実行中に型検査のエラーで中断してしまうことがある（書類に不備があり手続きの途中で書類が差し戻されてしまうことがある）
- 実行時の型検査によりプログラムの実行に時間がかかる（市役所の担当者が書類の検査を行うので手続きに時間がかかる）
- 説明
漸進的型付けにいたるまでの問題意識
静的型付けと動的型付けは，どちらかが全てにおいて優れているというわけではなく，それぞれ向き不向きがあり，状況に合わせて使い分けられています．しかし，現実のプログラム開発では，初めは動的型付けでプログラムを開発し，徐々に静的型付けを導入していくといったように，両方の型システムを混ぜて使えた方が便利な場合があります．
2章の市役所の例で考えてみましょう．先ほどは生年月日だけを取り扱っていましたが，今度は住所も取り扱うことにします．生年月日は非常にシンプルな情報だったので，機械による検査が簡単でした．
しかし，住所はとても複雑なので，検査するための機械はとても高価で導入するのは大変です．そこで，生年月日は機械で検査して，住所は市役所の担当者が検査するようにできれば都合が良いです．
現実のプログラム開発でも，このように二つの方式を組み合わせて使いたくなる場面が出てきます．しかし，こうした要求を達成できる型システムはそれほど研究されておらず，特に二つの型システム間の移行をスムーズに行えるような型システムは存在しませんでした．
筆者の研究対象: 漸進的型付け
漸進的型付けとは，ひとつのプログラムの中で静的型付けと動的型付けをスムーズに組み合わせるための手法です．プログラムを書く人は，特別な注釈を付けることによって，静的型付けをする部分と動的型付けをする部分を自由に選ぶことができます．
再び市役所の書類で例えると，書類中に複数の項目があるときに，機械で検査する部分と担当者が検査する部分を自由に選択できるようなものです．
漸進的型付けは，うまく用いることができれば，静的型付けと動的型付けの良いとこ取りができるため非常に注目されています．2006年に最初の論文 [1] が発表されてから急速に研究が進み，現在ではいくつかの有名なプログラミング言語に導入されています．
しかし，漸進的型付けは，基礎理論こそ徐々に成熟してきていますが，まだまだ発展途上の分野です．そもそも，静的型付けと動的型付けは長年研究が続けられており，それぞれに大量の研究成果があります．
それらを単純に組み合わせるだけでもたくさんのパターンが考えられ，その上，それぞれの組み合わせもたいてい一筋縄では行きません．静的型付けと動的型付けのメリットを十分に引き出すためには様々な工夫が必要になってきます．
また，単純に組み合わせるという研究以外にも，現実のプログラミング言語へ応用するため様々な側面から研究が行われています．この記事を読んでいる皆さんにも，最先端の研究に関わり，論文を発表するチャンスは十分にあります．次の章では，実際に私が発表した論文について少しだけ説明をします．
筆者の研究: 漸進的型付けの拡張
私は，2017年の夏に，漸進的型付けを多相型という特別な型で拡張するための理論について論文を執筆しました [2]．漸進的型付けの理論では，漸進的型付けが満たすべき5つの性質が数学の定理の形で提唱されており，多相型を含んだ言語でそれら全ての性質について議論した論文は知られていませんでした．
そこで，プログラミング言語を数学的に形式化した「ラムダ計算」というモデルをもとに，5つの性質が成り立つような，漸進的型付けと多相型を組み合わせたモデルを定義しました．私の論文では，5つの性質のうち4つは証明できたのですが，残りのひとつの証明が非常に大変で，現在も予想として残されています．
終わりに
この記事では，私の研究領域である型システム，特にその中でも漸進的型付けについて紹介しました．非常に高度な話題でしたが，例え話を通して雰囲気だけでも掴んでもらえたら嬉しいです．
最後に，漸進的型付けが注目されていると述べましたが，それでも，論文の数は漸進的型付けの研究が盛んな学会で全体の数パーセントあれば上々といったところです．この記事で説明したのは研究領域の氷山の一角で，プログラミング言語や型システムひとつ取っても様々な研究が存在します．
もし，この記事を読んで「漸進的型付けの研究をしたい！」と思ってもらえたら，それはとても嬉しいことなのですが，一方でみなさんが一つのトピックに固執してしまうことへの危惧も感じます．
みなさんが実際に研究をするころには，分野のトレンドが大きく変わっているかもしれません．みなさんも，より多くを学び興味の対象が変わっていくかもしれません．今みなさんの目に映っている技術や流行だけにとらわれず，自分の興味に素直に従って，広く研究を見渡すのが良いでしょう．
このメディアは，みなさんにそうした広い視点を持ってもらうために作られたもので，他の記事もとても参考になるはずです．理系・文系の垣根を越えて，最先端の研究を楽しんでもらえたらと思います．
参考文献
- Jeremy Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. Scheme And Functional Programming Workshop.
- Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. ICFP 2017.
