この記事は http://www.cl.cam.ac.uk/~srk31/blog/2014/10/07/ この文書の和訳である。原文も別に個人的には興味深いとは言い難いし、CSについての専門知識は全然ないので適任でもなんでもないのだが、例によって「POSTD」の日本語訳( http://postd.cc/7-deadly-sins-of-talking-about-types/ )が余りにも余りなので、私にわかる限りでもう少しマトモな翻訳にするとどうなるか試してみる。Markdownの脚注と[ ]内は訳者の（余計な）補足である。

型を語るということの七つの大罪

「型を求めて In Search of Types」という小論で、私はプログラミングにおける「型 type」という語を取り巻く様々な概念と目的と態度についての、感情抜きの冷静な批評を試みました。それでも所々で、私の感情がかなり透けて見えてしまっているのではないかと思います。しかしこの記事では、より臆面なく大演説をぶち上げる予定です。[型に関する]ある種の言明ないし態度には本当にイラつかされます。最近、Strange Loopでもそうしたものに幾つか出くわしました（カンファレンス自体は素晴らしいものだったということは付け加えておきます）。なので、「型」について語る（騙る）多くの人々によって犯されている大罪の一覧を書き留めることにしたのです。

問題になっているのが、レトリックの点についてだということは付け加えておくべきでしょう。私を苛立たせるのは、人々が真っ当で見通しの良い議論をしていない、という点です。彼らの結論が間違っているということでは必ずしもありません。私はOCamlでそれなりの量のプログラミングをしていますし、型検査器から多くの価値あるものが得られることは明白です。しかし、型システムの擁護者は、しばしば、その限界や望ましからざる副作用を認めずに、恰も奇跡の治療法であるかのように売り込もうとします。プロパガンダや不当に一般化された主張を越えて議論を先に進めてもらえないもんでしょうかね？

「型」という語の下に潜む様々な別々の概念のもつれを解きほぐすのにしばしば苦戦させられるということがこの状況に一役買っています。私のこの小文は、このもつれぶりに、[それを解きほぐそうというよりは]より直接に挑もうとするものです。もっとも、以下の大演説では、願わくは有用な区別を幾つか提示しようと思います。

抽象化を型チェックと区別できていない

これが一番気に入らない点です。殆どどんな言語でもデータの抽象化というものは提供されるものです。更に進んでその上に静的なチェックのシステムを構築している言語もあるわけですが、本当にお願いですから、この両者を混同しないで頂きたいものです。

この混同が、なんやかんやの言語についてまったく見掛け倒しの正当化を行うために何回も何回も使われるのを目にします。恰も両者が同じものであるかのように、データ抽象の恩恵を乗っ取って型システムの恩恵を持ち上げるのに使われるのを目にします。

Strange Loopで行われた「文字列的に型付けられたプログラミング」（ママ）というディスカッションでは、Snively/Laucherのトークセッションでも、Chris MorganのRust風味のトークセッションでも、まさにこれが行われていました。なるほど、（Morganの挙げた例を借りれば）HTTPヘッダが単なる文字列ではなくそれを越えて抽象化され得るし（通常は）そうされるべきだ、ということは事実です。しかし、この抽象化をし損ねるということと、コンパイル時の型チェックを省いてしまう、ということとは同じことではありません。それはあくまでデータ抽象が省かれてしまっているというだけです。もし後者を省けば前者も省いたことになるに決まっているというインチキな議論が行われるのをいつもいつもいつも目にします。これは端的に間違っています。型チェックは、ソフトウェアについて実行時以前に保証を得るための一手段に過ぎません。それは素晴らしいものではあるのですが、唯一の手段だというわけでもありません。手段と目的を混同しないようにしてください。

構文上のオーバーヘッドが問題であるかのようなふりをする

Sniveley/Laucherのトークセッションでは、動的言語を好む人々は構文が簡潔だから動的言語を好んでいるのだというコメントがありました、これはもしかしたらそうなのかもしれません。しかし私は違和感を覚えざるを得ません。それは「人々が型システムを嫌うのはただ型注釈の構文的オーバーヘッドのためにほかならない」というこれとは別の主張を仄めかしているように思えるのです。これは明らかに誤っています！ 型システムは型注釈を書くことを強制するだけではありません。それは、型チェックを通るかどうかを中心にコードを組み立てることを我々に強制するのです。型チェックというものは定義上、ある特別な種類の構文論的推論なのですから、これは不可避のことです。

型嫌いというものがどんなものでも型注釈のオーバーヘッドに由来するものであるというのは、それを表層的問題だとして片付けてしまうひとつの方法ではあります。しかし、この問題はまったく表層的なものではありません。それは、コードがどのように組み立てられなければならないかに対して型チェックというものがもたらす深遠な影響についての問題なのです。それはまた、（ことによると皮肉なことに）多相性についての問題でもあります。型付けられた言語では、正当性が証明されうるような多相性のみが許容されます。これに対して、型付けられていない言語では、任意の複雑な多相性をも表現することができます。Rich Hickeyのtransducerトークセッションでは、人間には理解できるような多相性のパターンを精確に論理システムに捉えることが極めて難しくなるということがいかに容易に生じうるかの好例が挙がっていました¹。そうした多相性は過度に制約的にしか捉えられず、そのために表現力の不足した証明体系しか与えられないのです。その結果として、明らかに正当なコードであるにもかかわらず型チェックを通らない、というようなものが出てきます。

信仰を持たぬ人々を見下す

もし誰かが型付き言語に近寄らないようにしているとしても、その人たちがバカだとか学が足りないだとか数学を恐怖しているのだとかいうことにはなりません。近寄らないのにはまったく妥当な実際上の理由があるのです。見下したような話し方はやめてください。

型レベルプログラミングを良いものであるかのように提示すること

およそ正気の人間なら、あるプログラミング言語をベースレベルと型レベルというはっきりと別々の断片へと二分することが望ましいのだ、などとは論じたりできないはずです。Gilard Brachaはこれを「影の世界」問題と呼んでいます ² 。レベル0の構造に対して抽象化を行うためには新たにレベル1の構造が一揃い必要で、このレベル1の構造に云々…というわけです。これはアンチパターンであり、合成性(compositionality)の失敗です。だからといって、これが実際上の理由から正当化されないというわけでもありません。MLのモジュールシステムが現状のようであるのは、様々な設計上の制約の下で（もちろんこれには型システムの健全性が証明できるということが含まれます）それより巧くやるための数学的理論が未だわかっていないからです。でもお願いですから、型レベルプログラミングが望ましいものであるかのようなふりをするのはやめてください。それは、その場しのぎのひどいシロモノであり、願わくは、あくまで一過性のものであるに過ぎません ³ 。個人的には、仕様の全てを通常のコードを書くのに使う言語と多少とも同様の言語で書き下ろしたいものだと思います。正当性を証明するのはツールの仕事ですし、もし証明に失敗したらそう教えてくれなければいけません。（その際には、またそれを率直なやり方で説明してくれるべきです。理想的には反例を提示するとか、証明不能な命題を余計なものを削ぎ落した形で示すとかすべきです。が、目下のところ、これをしてくれるような型検査器を私は知りません。）

Curry-Howardフェティシズム

Curry-Howard同型対応は[証明と型システムの間の]興味深い数学的な等価性ではありますが、どうしたらソフトウェアを効率的に書けるかについての議論をなんら推し進めるようなものではありません。

「型安全性」を巡る曖昧なものいい

異なった多くのことを表すのに用いられるフレーズがこれです。古臭い意味での「型安全性」は、かの有名な「Javaは型安全でない」という覚書に因んで「Saraswatスタイル」の型安全性と呼ぶことにします。（もちろんこの語はSaraswatによって発明されたわけではありません―それは当時このフレーズの持っていた「標準的」意味だったのです。）この[意味での型安全性]は価値ある性質です。しかし、それは実際にはメモリに関してのもので、データ型に対してのものではありません。この性質は、「ワード」型しか備えていないような言語⁴についても（Saraswat本人の言葉遣いにほんの少し手を加えればですが）定義できるのです。また、これは静的な型検査ともまったく関係がありません。どんな「動的に型付けられた」言語でも、この「型安全性」は成立しています。この性質が有用なのは、マシンに密着した低水準でプログラムしようと言うのでない限り、多くの犠牲を支払うことなしにそれを実装できるからです。多くの実装は実行時検査のオーバーヘッドを緩和するためにコンパイル時の構文論的推論、つまり型検査を用いていますが、これは個々の実装の具体的事情に過ぎません。

Saraswatの意味での型安全性は、通常、とてもよいことです。しかし、コードの殆ど任意の正当性を証明するというには程遠いものです。型システムがなければ「型安全性」は得られないなどといって、問題を混同するのはよくあるやり方です。別々の考えをこのようにわざと混同することによって、相対的に異論の余地の少ないSaraswatの意味での安全性の価値を利用して、「型システム」もまた同じくらい易しい明々白々なものであるかのように描くわけです。証明にはコストが掛かります。どのくらい支払うべきかは為すべき仕事次第の問題です。悩む余地のない簡単明瞭なものなどではまったくありません。

不都合な真実には触れないでおく

ステキな型システムのあるモダンな言語をみんなが用いさえすれば、正当性の問題は全部解決しますよね、そうでしょ？　もしそんなことを信じているとしたら、あなたは[カルト教団が集団自殺に使った]クールエイドの飲み過ぎでラリってるに違いありません。しかしながら、見たところ、我々の業界は自発的なカルト信者で溢れかえっているようです。端的にいいましょう。型システムは仕様記述と検証を一発解決するようなものではありません。それらは定義上、限られたものです。型システムは構文論的にしか推論しませんし、式表現という粒度でしか仕様を記述しません。それでも型システムはなお有用ではありますが、どうか現実的になってもらいたいものです。

コードの到達可能性、あるコードがデッドコードでないという性質(liveness property)を型検査器でチェックしてみたらいいでしょう。そんなのは成功するはずがありません。形式的な意味では、実は型検査器で到達可能性をチェックすることは可能であり、実際にされてもいます。しかし、その結果として得られるシステムは型システムの普通の利用者が、ああこれは型システムだと認識できるようなものとは殆ど共通点のない代物です。この論文の著者たちは、このシステムが生み出す顕示的に型スタイルによるような仕様記述が「デカすぎ」で、「人間による推論には不向きである」と注記しています。これはまったく驚くべきことではありません。というのも、彼らはプログラムの既存の構文論的分解という粒度で作業しているからです。到達可能性を記述しチェックするには、プログラムをある種のフローのグラフとして表現しなければなりませんし、そこでのフローはほぼ確実に多数の関数と多数のモジュールにまたがるものになります。これは式表現的なコードの見方ではありませんし、また殆どの人々はそれを構文論的にコードしたいとは思わないでしょう。

もうちょっと大人になって、この現実を受入れましょう。で、ひとたびそれを受け入れたとなれば、ほかにどうしたらいいのでしょう？ たとえばよりマシなSMTソルバーとかそういった、我々にコードを打ち直し(re-type)/再型付け(re-type)させずに済むような（この洒落はワザとです）、自動推論に於ける漸進的改善を可能にするモデルが必要です。しじゅう言語を切り替えることなしに仕様記述の力をステップアップしていくことができる必要があります。型の付いたコードと型の付いていないコードとを統合する必要がありますし、別々の言語の間でもそうできなければいけません。

ゆっくりながら、こうした考え方が、たとえば漸進的型付け(gradual typing)のように、牽引力を持ち始めていますが、道程は遥かです。特に、複数の言語を共存させることは、情報技術のインフラに深甚な影響をもたらします。これまでのところ、我々は言語をそれぞれあるひとつの特定のやり方で実装しています。つまり、コンパイラ内蔵の型検査器で、プログラム全体の不変条件を確立するわけです。もし多言語を抱えることになると、こういう風にものを作っていくことはもはやできなくなります。言語ごとのコンパイル時の仕事ではなく、よりジェネリックなコンポジション時の仕事として、不変条件を強制するという問題に取り組む必要があります。（ヒント：これはリンカーと呼ばれています。簡単に言えば、証明とinstrumentationとが混じったものを、コンパイラが出力する記述的情報を頼りに言語中立的に遂行するリンカー的サービスが必要になるのです。最近の私の発表を聞いたことがあれば、これはお馴染みの話のはずです。興味があれば直接聞いてください！）

当面の間は、証明したいものの全てを証明はできないままコーディングをする、という活動が継続することになります。他方で、遅延束縛は、それのせいで真に実行時前に行われるような推論を適用することが制約されざるを得なくなるのですが、いまや実装ごとの決定の問題ではなくしばしば必須の要求事項になっています。これらを無くしてしまえば面倒はなくなりますが、それらの持つ価値も無くしてしまうことになります。ある製品の総体的価値を最適化するやり方でコストと便益を考量すること、それこそが、これらの問題について考える唯一正しい方法です。それは我々の論議を目下のところ支配しているような、ドグマ、レトリック、盲目的信仰からは、遠く隔たったものです。

コーダ

さて、これで私の思いの丈は吐き出しましたから、建設的たらんとするコーダへと入って行きましょう。既に述べたように、問題の一部は「型」について語る際に我々が曖昧なものいいをしているということにあります。「型」とか「型システム」とか言う代わりに、以下の代替的語彙の一覧から、意図されている意味を伝達するものがないかどうかチェックしてみることをおすすめします。どの術語が適切かを決めるのは、実際にどの意味が意図されているかを理解するための、よい思考訓練になります。

データ抽象
データ型
述語、命題
証明、証明系
インターフェース仕様記述[言語]
[コンパイル時]検査器
仕様記述、検証
不変条件（ふつう「型」が記述しようとしているのはこれです！）

ほかになにか思いついたらぜひ知らせてください！