私の小論 “In Search of Types” では、プログラミングで使われる“型”という言葉の概念や目的、考え方について、公平な批評を心がけました。所々で、私の真剣さを感じ取っていただけるはずです。このブログ記事では逆に、思い切って堂々と批評していきます。いくつかの意見や考え方に、私は苛立ちを隠せません。先日参加したStrange Loopでも、このような状況に陥りました（補足しますが、すばらしいコンファレンスでした）。この機会に、“型”について多くの人が（誤って）語った“重大な誤り”をリストアップしていきます。

ここで話す内容は、説得力のあるものです。私が苛立ちを覚えるのは、人々が正当かつ透明性のある議論を行っていないことに対してです。結論に誤りがあってはいけません。私は、OCamlである程度の数のプログラミングを行っており、それは型チェックから多くの価値を得ることができるシンプルなものです。しかし型システムを支持する人たちは、それが持つ制限や好ましくない副次的影響の知識を持たずして、これを有効な解決策として頻繁に販売しようとします。過去の宣伝活動や包括的な発言について議論をしませんか？

問題が起こる要因は、“型”という言葉に潜む多くの異なる概念をひも解くのに、しばしば手こずることです。私の小論では、これをひも解くことに真っ向から立ち向かっています。以下に挙げる私のわめきがそれを区別する役に立つことでしょう。

抽象化とチェックの区別ができていない

これが、私が最も不満に思うことです。ほとんどのプログラミング言語は、データの抽象化を提供しています。中には、静的チェックシステムの構築をこの上で開始している言語もありますが、どうか、どうかこの2つを混同しないでください。

プログラミング言語を正当化する理由として曖昧な表現が何度となく使われるのを、よく目にします。あたかも2つが同じものであるかのように、データの抽象化の利益を奪うことで型システムの利益が得られると宣伝したりしています。

Strange Loopでの“文字列型プログラミング”（sic）に関するディスカッションでは、 Snively/Laucher のセッションとChris Morganの Rust-flavoured のセッションの両方で、まさにこの2つを混同していたのです。確かに、HTTPヘッダ（Morganの例を借りると）は、かなりシンプルな文字列に抽象化することができますし、（通常は）すべきです。しかし、抽象化しないからといって、コンパイル時の型チェックが省かれるわけではありません。データの抽象化を省いただけです。データの抽象化を省いたら、コンパイル時の型チェックが省かれる、という間違った議論を行っている人たちを何度となく見てきました。明らかにこれは誤りです。型チェックとは、ソフトウェアの起動を予め保証する1つの方法にすぎません。すばらしいことに、他にも方法はいくつかあります。どうか、手段と目的とを混同しないでください。

構文上のオーバーヘッドが問題だと装っている

Snively/Laucherのセッションでは、簡潔な構文であるという理由で動的言語が好まれる、ということも話していました。言っていることは正しいと思いますが、私はこれには違和感を覚えます。なぜなら、型システムが好まれないのはアノテーションの構文上のオーバーヘッドが問題だと言っているように取れるからです。これは間違っています。型システムはアノテーションを書くためだけのものではありません。型チェックの際にコードを構築させる、という働きもあります。当然ながら、型チェックは特定の構文上の推論なので、これを避けて通ることはできません。

型アノテーションのオーバーヘッドに対する嫌悪を表すことは、それを表面上の問題として片づけてしまう1つの手段ではあります。しかし、これは表面上の問題ではありません。コードがどのように構築されるべきなのかという、型チェックの大きな成果なのです。また（もしかしたら皮肉かもしれませんが）、ポリモーフィズムでもあります。型付き言語では、正しいと認識されるポリモーフィズムだけが、受け入れられます。型付きではない言語では、任意の複雑なポリモーフィズムは、表現することができません。Rich Hickeyは、 transducersのセッション で、人に理解されやすいポリモーフィズムのパターンが、どのようにして正確な論理回路上でキャプチャすることを極端に難しくしてしまうのか、という良い例をあげてくれました。通常、それらは、言葉では表せないプルーフシステムを得てキャプチャされます。最終的に明らかに正しいコードに対しては、型チェックしません。

自分の信念の外側にあるものを見下している

型付き言語から遠ざかる人がいても、それは彼らが愚かで知識に欠けているからだとか、数学を怖がっているからというわけではありません。遠ざかるのには、実質的な理由があるのです。上から目線にならないようにしてください。

型レベルプログラミングを良いものとして提示している

分別のある人であれば、プログラミング言語を、異なるベースレベルと型レベルのフラグメントに二分することを受け入れないでしょう。Gilad Brachaは、これを“影の世界”の問題と 呼んでいます 。レベル0のコンストラクタから抽出するために、まったく新しいレベル1のコンストラクタのセットなどを必要とします。これはアンチパターンであり、合成性の失敗です。実質的な理由を正当化できないというわけではありません。MLのモジュールシステムはこのようなものですが、それは様々なシステムのデザインの制約の下で、数学を活用する方法を誰も理解していないからです（これはもちろん、健全性の証明も含みます）。しかし、どうか型レベルプログラミングは価値のあるものであると装うことはやめてください。これはその場しのぎの解決策で、おそらく一時的なものです。個人的に、私は仕様書の全てを、通常のコードを書くときと大体同じ言語で書きたいと思っています。正確性を証明するのはツールの仕事ですし、それが必要不可欠なら、失敗だったと教えてください。（さらに、砕けた説明も使うべきです。理想的には、反証や必要最低限の証明できない提案を加えます。これを正しく行っている型チェックを、私は知りません）。

カリー=ハワードをやみくもに崇拝している

カリー=ハワードは数学的に同価値の興味深いものですが、ソフトウェアを効率的に書く方法についての議論を進めるものではありません。

“型安全性”を曖昧にしている

この言葉は、多くの異なるものを意味するのに使われてきました。時代遅れの“型安全性”のことを、有名な “Javaは型安全ではない” のメモから、私は“Saraswatスタイル”と呼んでいます。（もちろんSaraswatによってつくられた言葉ではありません。当時はこれが“基本的な”意味でした）。これは価値のあるプロパティです。しかし実は、メモリであってデータ型ではありません。“言葉”のデータ型のみの言語に関して定義できるものです（Sarawatの言葉から、少し変えて使っています）。また、静的チェックとは何の関係もありません。“型安全性”が含むのは、“動的に型付けされた”言語です。これが使いやすいプロパティである理由は、マシンを忠実にプログラミングしたいと思わない限り、多くの犠牲なしで実装できるからです。はからずも、多くの実装はオーバーヘッドな実行時間を減らすために構文のコンパイル時処理や、いわゆる型のチェックを使っています。これが実装の詳細です。

Sarawatスタイルの型安全性は、一般的には非常に良いものです。しかし、任意に近い正確なコードのプロパティを提供することとは、まるで違います。型システムを使わないから“型安全性”がないなどと言って、問題を混乱させることはよくあります。この区別されたアイデアの故意的な混乱は、比較的議論にならないSaraswatスタイルの安全性の価値を利用し、“型システム”を非常に単純なものに塗り変えます。証明にはコストがかかり、タスクによっては適切な出費なのです。単純からは程遠いものです。

不都合な真理を省略している

全員が装飾的な型システムと一緒にモダン言語のみを使えば、正確性の問題は全て解決するでしょうか。もしそう思うなら、クールエイドの飲み過ぎです。しかし、明らかに私たちの仕事は自発的なオカルトメンバーであふれています。簡単に言いましょう。型システムは、仕様と検査において、万能な解決策にはなりません。定義によって制限されています。これは構文的な場合だけを推論し、表現の粒度のみを明示します。それでもやはり便利ですが、現実的になってみましょう。

型チェックで現実的な到達可能性や、プロパティの活性をチェックしようとしても、うまくはいかないでしょう。形式的な感覚では、実行可能そうに、あるいは 実行されてきた ように見えますが、得られるシステムは、専門家が認識するような型チェックと似たところはほとんどありません。注記として、表面上の与えられた型スタイルが“大きすぎて”、しばしば“人の手による推論”に見合わないということです。これはさして驚くべきことではありません。プログラムの既存の構文分解に反した働きをしているからです。活性や到達可能性を特定してチェックするために、プログラムをある種のフローグラフで表す必要があります。そしてフローは多岐にわたる機能とモジュールになる可能性があります。しかし、これはコードの表現的な見方ではありませんし、大抵の人が必要としているコードの構文でもありません。

私たちは一歩進んで、これを受けとめる必要があります。一度受け入れたからといって、何が違うのでしょう？　私たちはコードを（意図的に）型を分類し直す必要なく、優れたSMTソルバのような、自動的に推測し段階的な改善を同化させるモデルを必要としています。常に言語を切り替えることなく、仕様の強度を高められるようにしなければいけません。異なる言語間でも、型付けされたコード、型付けされていないコードを統合する必要があるのです。

こういった考え方は、少しずつ段階的な型付けのような主流になってきていますが、まだその道のりは遠く険しいものです。中でも複数の言語への対応は、私たちのインフラとして、広範囲で発生する問題です。現状では、ある特定の方法で言語条件を満たします。一度のコンパイラの型チェックで全プログラムの不変量を確立させるのです。複数の言語を受け入れたら、もはや、このようなやり方はできなくなります。代わりに言語ごとのコンパイル時サービスではなく、より一般的なコンポジション時サービス内で可変の実装を行うことが必要になります（ヒント：リンカと呼ばれるもの。つまり、リンカのような働きは、言語が中立な場合において、コンパイラによって出力される情報で証明と計装の両方を実行しなければいけません。最近、私がこの話題に触れたことを知っている皆さんなら、身近に感じるでしょう。どうぞ質問してください！）。

証明するべきものを証明せずにコーディングすることは、実際、今後も続いていくでしょう。一方で、遅延結合と、事前の推測によって限られた適用性は、必要条件ではありますが実行を決定するものではありません。これらを除外することは、有益ではありますが、同時に価値を排除してしまう可能性もあるのです。所定のプロダクトのために全体的な価値を最適化する方向で、コストと利益を考えることが、これらの問題を考える上での正しい方法と言えます。現在、私たちの議論を支配しているドグマやレトリック、妄信的な信頼からは離れています。

終わりに

私の気持ちを吐き出したので、建設的なまとめに入っていきましょう。すでに述べたとおり、問題の一部は、“型”について語るときの曖昧さだと思っています。“型”や“型システム”の代わりに、以下の他の言葉を使って、果たして意味が正確に伝わるかどうか試してみてください。どの言葉が最適かを決めることは、意図した意味が伝わっているかどうかを判断する、よい頭の運動になると思います。

• データの抽象化
• データ型
• 述部、提案
• 証明、証明システム
• インターフェース仕様（言語）
• （コンパイル時）チェック
• 仕様、検査
• 不変量（“型”が通常指定しているもの！）

他にも考えついたら、ぜひ教えてください。