2018-06-02

私と型システムとポエム

最近巷では俄に型システムについての言及が増え、型システムポエマーが増えてる気がするので自分もその時流に乗りたい。

完全にポエムだけどなんかあったら随時指摘ください。直します。

TL;DR

言いたいことはまとめると次

型システムは程度問題なのでちょうどいいところを探すべき
型は万能でも強さが正義でもない(だから未だに研究されてる)
よく知りもしないくせに計算機科学を侮辱するのはやめろ

予防線

あくまでポエムですので中身はないです

私は型理論専攻で学位はとったものの研究者ではないのであまり信用しすぎないように

型システムの過去

型システムは大まかに次のような利点があるとされてきた(個人的主観)

「異常」なプログラムを検出する仕組み
静的解析による分かりやすいエラーメッセージ
型そのもののドキュメント性
IDEでのcompletionに貢献
最適化に貢献
(数学に正しく裏打ちされたsemantics)

型システムの分類と主な特徴

当たり前だが型付き言語も一枚岩ではなく、色々違いがあるので少し分類をしておく。下に行くほど強い。

型なし(動的型)言語

言語: untyped lambda calculusやLL系言語など

LL系とは言ったものの例えばPythonは最近type annotationがかけるし、あるいは型のない言語でもIDEが静的解析を行い実質型システム相当のチェックを行う言語があったりするので型の恩恵を一切受けない言語はイマドキそう多くはない。型システムの人間からは型なしは型なしとして一緒くたにせざるを得ないが、別に型なしを嫌っているわけではない。それも一つの言語の在り方である。まぁ私は死んでも書きたくないけどな。

クソザコ型(データサイズアノテーション)言語

言語: C

かつて非型システムの人間にとって「型」とはこれであった。今でもこれを型システムと思ったまま脳みそがアップデートされていない人間もいると思う。要は変数にint, floatなどのアノテーションがつき、これは実行時のその値のデータサイズを表す。大半の型付きの言語はこの機能を内包しているが、これはあくまで現実のコンピュータのアーキテクチャに寄り添ったエンジニアリング的観点により導入されることが多い。これを型システムと呼んでもいいかは諸説ある。私は呼ばない。

割と単純な型をもつ言語

言語: simply typed lambda calculus、関数型はあるがジェネリクスを入れてないような一部の言語

ジェネリクスを入れると考えることが多くなるのでこの辺で落ち着くという選択肢もある。Goとかはこれかな？(よく知らないで言ってる)。すごく単純なプログラムしか書かないなら、静的解析も楽でコンパイルも早くそれなりに型の恩恵も受けられてよい落とし所だと思う。ただライブラリを作る人にとっては抽象化への障壁が大きすぎると感じるかもしれない。

頑張れば型推論の決定性を保てる言語

言語: OCaml, Java, C#など

多くの(現場で使われるような)静的型付き言語はここに属することが多い。 (実際はいろいろな事情によりできてない言語が多いが)OCamlに代表されるようにジェネリクスとサブタイピングまで入れても型推論は決定的にできる。型を人間は書きたくないが抽象化はさせろという人にとっては最も都合の良い着地点になる。現状多くの人に受け入れられているように見えるので成功した型システムの一つと言っていいと思う。この言語ではオーバーローディングなどの型推論を阻む仕組みに対してどのように対抗するかというのが大きな問題になる。現状では政治力と運用でカバーしていることが多いような気もする。

typeclass/rank n types/higher kind polymorphism言語

言語: Haskell2010, Haskell(GHC), Scala

型推論の決定性を窓から投げ捨てて暗黒面の力を手に入れたやつ。OCamlは職人技のような言語デザインで決定性を保っていたのでそこに少し拡張を入れたり少し条件を緩めたりするだけであっという間に暗黒面に堕ちてしまうので意図せずこっちに転がってる言語もたまにある。明確に意図してここに足を踏み入れた言語は(実用面でも使える言語となると)限られてくるが、型推論を気にせず理論的に便利な道具をたくさん追加できて気持ちよく型レベルプログラミングとかで遊べるようになる。しかし暗黒面と称されるようにここから先は地獄である。依存型の誘惑を振り払うのは難しい。

依存型言語

言語: Idrisなど

依存型を持つ言語はAgda, Coqなど色々あるがだいたいは証明用途なのでプログラミング言語とは呼べない。実用で使う人は多分いない。

強けりゃいいってもんじゃない

型システムには色々あるし上の分類も本当はもっと細かくわけられる。が、大事なのは強ければいいというものではない。

強い型システムはだいたい次のような問題との戦いになる

型推論が効かなくなってクソ長い型を書かされる
コンパイル時間が増加する
言語ごとの型システムの限界に阻まれる
コンパイラを制御するために型レベルプログラミングで人間が消耗する

人間が消耗するというのは笑い事ではない。型レベルプログラミングとは型システムの限界との戦いであるし、そこで目的を達成するためには型レベルのエンジニアリングが必要になる。大変不毛なコードを書くことを強いられたりコンパイラの推論能力ギリギリを攻める羽目になったりする。実行時エラーをコンパイルエラーにするために途方もないコストを支払う羽目になる。

それと現実世界との兼ね合いという問題もある。実際にプログラムを書くためにはどこかで現実世界の仕組みとブリッジする必要があり、現実世界は型がガバガバなのでその境界付近にすべてのしわ寄せが行く。これは型システムというか静的解析の宿命で、HaskellやScalaに限らずRustなんかでも顕著であるというのが私の経験則としてある。

よくある誤解

さて型システムはよく誤解されていて、間違った言説を垂れ流す人間が後を絶えないのでしょうがなくいくつか訂正をここにいれる。ここに上げた誤解を型システムが専門の人間に吹き込み続けると泡を吹いて絶命するのでやめよう。

「型のある言語は型を書く必要がある」

一番良く見るやつ。戦犯度が高い。二度とその口を開くなという気持ちになる。

型推論という仕組みがあるので一般には嘘であるが、一部の言語は言語のデザインとして(理論的限界ではない)型宣言を強制しているのでそのへんからくる誤解だと思う。Javaお前のことやぞ。

「型とか見ればわかるんだからチェックする意味なくない？」

クソザコだとまぁそういう面は多少ある。弱い型システムでも一応次のような利点はあるよって言ってる。

タイポと仕様変更に対する予防: 型が変わったことを検知できるのでAPIを安心して破壊できる
間違った使い方をさせないようにライブラリ作者がユーザーを縛る: あらゆる可能性を想定するのはしんどいので

「IDEが色々教えてくれるから型とかいらん」

そのIDEがやってるのは実質静的解析だぞ

「将来的に型推論が発展したら型を書かなくてよくなる」

これができるかどうかは決定性依存であり、System Fなどそれなりに「強い」型システムは決定的でないことが示されてしまってるのでそのへんは理論が発展しようがどうしようもない。そして型を書かなくてよい型システムはすでにある。その意味では型推論はすでに十分に発展したとも言える気がする。

「将来的に型から実装を導けるようになる」

なわけない。IntからIntへの関数がいくつあると思ってるんだ。実際にはparametricityが効いてて型から実装を導ける場合はあるけどそれはそれなりに特殊な状況に限られる。

ただまぁ「満たすべき条件」から実装を導くという研究はそれなりにある。個人的に型システムとして実現されるとは思ってないが、指定した条件を満たす関数をコンパイラが提案してくれるみたいなのはそのうち多分出てくると思う。

「依存型っていうのがいいんでしょ？」

依存型を導入することは定理証明をすることと紙一重である。まじで地獄なのでおすすめしない。

「Javaでは〜」

Javaが静的型付き言語の代表みたいな言い方はやめろ。

「LL言語でも型入れればいいのに」

これは結構微妙な問題も含んでいて、一部のLL言語では動的に色んなことできますみたいなのが売りになってたりするのでそういうところを壊さずにちゃんと型をつけるのは結構難しい。あと技術的にはできても、ライブラリとかとの兼ね合いもあるから実際にそういうのを突っ込むのは難しいのではないかと思ったりする。そういう意味で、既存の型なしの言語に型を入れるよりも、似たような文法でちゃんと型のつく言語を作って既存のを駆逐するほうが早いと思う。みんな頑張ってくれ。

型システムのこれから

ここからは完全に私の狭い観測範囲からの妄言になるけど、型システムは強くしたり合体させたりするフェーズは終わりつつあると思う。これからはむしろ特定の状況にマッチした静的解析を乗っけた言語をいっぱい作って属性で特化させるんじゃないかなと。例えばRustはregion推論をベースに先陣を切ったけど、そういうふうに「こんな静的解析が乗ってますよ」みたいな一芸型システムをMLに突っ込んだみたいな言語が増えてきそう。

自分はモナドとかエフェクトとかやってたからエフェクト関係でそういう言語ほしいな〜と思いつつ、実際は現実のAPIを呼ぶところをどうやって解決するかとか、あとはまともに使えるようにするためには決定性の壁とか色々あって厳しかったりして難しいかなぁって感じ。

おまけ

エンジニアリング業界では、Javaがそれなりに鍵を握ってるような気もする。一部の人達はJavaが型付き言語の代表格だと思ってるフシがありそのへんから誤解というのが生まれるのだろうけど、逆に言えばJavaが今だんだん変わろうとしているというのはそういう層に正しい型システムと型付き言語によるプログラミングを浸透させるきっかけにもなるだろうし。

あとは型システムに対して適当を言うのは本当にやめよう。私はついったーでそういう発言に対してよくキレているが、そういう適当はこれまでの偉大な計算機科学者たちの生み出してきた素晴らしい業績への冒涜にほかならないからである。すべての人間が型理論を勉強するべきとは思わないが、多くの人が積み上げてきた理論に反することをなぜそんなにも簡単に口にできるのか不思議でならない。

というようなことをよろしくしたいんだけど、本当によろしくしたい層には届かないんだよこういうのは。