科学はその方法論上のイメージよりもはるかに”ぞんざい”かつ”非合理的”なものである。
Paul Feyerabend著『Against Method（方法への挑戦）』（1975年）

プログラミング言語は魅力的な分野です。それは、計算機科学（と論理）を 社会学や人間とコンピュータの相互作用 、科学的に定量化できない直感や嗜好、そして（良くも悪くも）政治などを含む分野と結び付けてくれるからです。

プログラミング言語を話題にする場合、たいてい何らかの客観的な真実を追求する科学的議論になってしまいます。科学は完璧のオーラに包まれているため、科学的本質の核心部だけに集中し、他の部分を無視するのが正しいプログラミング言語の考え方だと単純に思ってしまうのも無理ありません。

しかし、これではプログラミング言語を面白くしている多くのものが除外されてしまいます。この隙間を埋める1つの方法は、科学の哲学に目を向けることだと思います。そうすることで、プログラミング言語の研究過程や研究方法について理解できると思います。昨年、この題材についての一般的なアイデアを ブログ （とエッセイ）に掲載しました。今回は話題を絞り、 型の意味とは？ について話します。

このブログの内容は、 Onward! Essays 2015 に提出したエッセイをまとめて（哲学的ではなく要点を絞って）います。エッセイで展開したアイデアをざっと見たい方はこのままお読みください。エッセイを読みたい（または後で読みたい）方は、 ここで完全版 をお読みください。

型の意味を探して

私は2つのことをきっかけに型の意味を探し始めました。まず、1年前にStephen Kellと型の意味について話し合った後、Stephenが これに関する興味深い論文 を発表しました。Stephenは、関数系プログラマーによって理解されている”論理型”とエンジニア系コミュニティで理解されている”データ型”の違いを明らかにしています。これは、「人が型について話す時、必ずしも同じことを考えている訳ではない」という私の考えに共感するものでしたが、その対象範囲はさらに幅広いものだと思います。

2つ目は、 型についての講義 を受け持っていた時、私が担当したコースの教材に型が便利な理由をリストアップしたものがありました。おそらく代々この講座の教官に教材として引き継がれたものだと思います。

• 静的型チェックでも動的型チェックでもエラー検出が可能
• 大規模なシステムの構築のための抽象化とサポート
• 文書化
• 効率性
• 言語の安全性

過去に、複数のプログラミング言語が上記の理由から型を使用していました。しかし、型を導入している現代のプログラミング言語の世界ははるかに複雑です。今でも型を使用する理由は上記のいずれかですが、上記全てが理由であることはほとんどありません（さらに、言語が上記のリストの理由をうちいくつかを持っているとしても、その組合せによっては”型”付けされているかどうかについて、意見が分かれることもあります）。

例えば、 Julia言語 では、パフォーマンスのためだけに型が使用されています。 TypeScript では、型は大規模なシステムの構築と文書化のために使用していますが、効率（考慮されていません）や言語の安全性（不安定です）は考慮されていません。 F#の型プロバイダ は、主にツール（とちょっとしたエラーの検出）に使用しているため、上記の理由は当てはまりません。

では、どのようにして型の意味を捉えればよいのでしょうか。まず、型の意味は進化し変化するということを理解しなければなりません。そうすれば、進化や変化の過程を観察することができます（ここで科学の哲学が役に立ちます）。そして、科学の哲学では進化や変化は普通のことであり（いいことでもあり）、科学にとって必然的なことであるとしています。今までのように型を限定的に（明確に定義された）サブエリアで使えますが、型の一般的な（あいまいな）概念について議論するのも面白いのではないでしょうか。そうすれば、興味深い哲学的な発想が生まれるのかもしれません。

型の意味はどのように変化するのか

私の最初のポイントは、”型”の意味は進化し変化するということです。そうであることは、歴史を見ればはっきりとしていますし、それは現在でも変わりません。

数学基礎論からラムダ計算まで

Bertrand Russellは、1908年に「Mathematical logic as based on the theory of type」と題した論文で、自己言及から生じる論理パラドックスを避けるべく、型理論を発表しました。この理論によると、命題には型が付与されています。n型の命題について話す命題はn+1型を持ち、自己参照命題は除外します。

プログラミングに近い話をすると、1940年にAlonzo Churchによって型がλ計算に加えらました。しかし、あくまでも論理と数学基礎論に照らして展開しています（プログラミング言語という言葉でさえ使われ始めたのは1955年頃です）。面白いのは、Churchは型の導入をそれほど勧めておらず、λ計算では主にパラドックスを避けるため（および全プログラムを値に還元するような、 強い正規化プロパティ のように全プログラムを値に還元するの）に便利とされました。

式型から演算型まで

Stephen Kellが論文に述べた初期の頃の型の話は飛ばして、ML言語の初期の頃の型について触れたいと思います。ML言語は、（全ての式に型がある）λ計算の様式と（整数型や実数型のような従来の型がある）エンジニア様式を組み合わせています。ChurchやRussellが基礎となる型について特定していないことをあえてここで書いておきます。彼らにとって重要だったのは、型がどのように構成されたかでした。

MLのような言語では、型は演算によって生成される 値の集合 を示しています。これは今でも有力な型の考え方なのではないでしょうか。そして、ほとんどのプログラミング言語の理論や方法論はこの考えを元に構築されています（プログラミング言語に関する証明で言えば、τ型の演算はv∈τとなる値vを生成すると言えるかもしれません）。

しかしながら、”型は値の集合”という見方は、型システムの面白い部分を捉えていません。例えば、作用システムを使用している言語（あるいはHaskell monad）では、演算をトラッキングすることができます（私の書いた coeffects captures what computations require では別の例を挙げています）。トラッキングの結果、演算がint & {write ρ,read σ}型を返すかもしれません。これは、演算によって int 値を生成したことを意味し、同時にメモリ領域ρに何かを書き込み、メモリ領域σから値を読み込んだことになります（このため、σを保護するためのロックは必要ありません）。これは明らかに”型は値の集合”という概念の範囲を超えています。型を関係として捉えるのも選択肢の1つだと思います。

健全でない型システム、比較的健全な型システム、健全な型システム

ここまで、話を一直線に進めてきましたので、”型”の究極の概念を追求していくかのように思われていると思います。しかし、最近の興味深い型の発展を見ていると、型は一方向ではなく、あらゆる方向へ発展しています。下記にいくつか例を挙げてみました。

• 健全な型システム 。あるいは依存型言語と言ってもいいと思いますが、この型システムは、論理でリンクに戻り、従来の”言語の安全性”プロパティを拡張します。しかも、面白いことにプログラミングに対する考えを変えてくれます。十分な精度の型があれば、自動プログラミングもできるかもしれません。

• 健全でない型システム は、別の方向に展開しているもので、TypeScriptやDartが含まれます。TypeScriptやDartにおいて、型は主に文書化やコードの構成に使われ、論理プロパティの証明には使用されていません。そのため、簡単さと使いやすさに特化しています。そしてそれは、ジェネリックの共変性などの安全性の欠陥を作ってしまいます。しかし、ランタイム時に実行されるので言語の安全性を脅かすものではありません。

• 比較的健全な型システム は、F#の型プロバイダに対する私の分類です。型プロバイダは従来のML言語の安全性プロパティを保持していますが、相対的なものとしています。”世の中がうまく機能”していれば、安全性は提供されます。例えば、世界銀行のような型プロバイダが他の国々を静的型付けした場合、国が消えない限り安全性は提供されます。

型の概念が変わり進化することに納得していただけたと思います。私はこれらを同じもの（同じように定義されたもの）のインスタンスとして扱うのが実用的だと思います。型は、プログラミング言語の研究において、ある分野の考えを別の分野に適応できるようにしてくれる バウンダリーオブジェクト だと思います。

矛盾した論理と概念の拡張

科学の哲学を見ると、意味の進化と矛盾はそれほど珍しいことではありません（冒頭で引用したFeyerabendの言葉のように、”科学はその方法論上のイメージよりもはるかに”ぞんざい”かつ”非合理的”なものである。”のです）。

Imre Lakatosの発表した 概念の拡張 とリサーチプログラム の2つの考えは、型を理解する上で応用できると思います。

リサーチプログラム

科学を全体的に見ると、競合する リサーチプログラム を確認することができます。どのリサーチプログラムにも参加者がリサーチの際に当然のものとする仮定が 中核 にあり、方法の補助ベルトや興味深い研究課題を持っています。核心部はリサーチプログラムごとに存在し、必ずしも互いに一致しているとは言えないかもしれません。型の場合、あるリサーチプログラムの提案者は 型システムの安全性 を型の基本的な性質として、健全でないシステムは 型システム とはしません。別のリサーチプログラムの提案者は実用的使いやすさを核心部とし、過度に複雑なシステムを嫌います。

Lakatosが指摘するように、これはごく普通に科学では見られることであり、1つのリサーチプログラムの範囲内にいれば、特に影響はないとしています。しかし、リサーチプログラムの概念を念頭に置いておけば、なぜ型に関する多くの無意味な議論があるのか理解できます。

概念の拡張

Lakatosが発表したもうひとつの興味深い考えは 概念の拡張 です。ここでは、反例（または定着したモデルに当てはまらない事例）が発見された場合、概念（例えば型）の意味がどのように変化し改善されていくのかを説明しています。Lakatosは概念の拡張を数学に照らして展開しています。妥当な定義があるところに、（想定されていない）反例が見つかると、定義を改善する必要が出てきます。

今まで起きた型のあらゆる発展もこれで説明することができます。例えば、”型は値の集合”というとても簡単な定義内で、演算の作用をトラッキングするために型を使うと、この定義には当てはまりません。あるいは、”型安全性”という定義で、世界の国々の話をする際に型を使用する場合、型安全性プロパティを相対化する必要が出てきます。

さらに、Lakatosは反例や想定外の事例に対する共通の反応についても説明しています。私が特に気に入っているのは、monster-barrersで、普通ではない事例をモンスターと分類し、正常に機能している社会への受け入れを拒むと言う考えです。不安定な型システムを議論する際にmonster-barrersは珍しくありません。残念なことに、めったに下記のような立派な形で現れることはありません。

微分係数を持たない関数に、ひどく悩まされ恐怖で身震いし顔を背けます。
Charles Hermite（1893年）

型の定義への挑戦

ここまでの説明で、”型の状況”は全体として混沌としたものであることが分かっていただけたかと思います。これを受けて、 リサーチプログラム を適切に文書化し、 概念の拡張 を探し出し、それぞれに取り組んできた異なる型の考え方を分類してまとめた方がいいと言う人も出てくるでしょう。確かに一部の一般的な科学的作業では、そうしたことが役に立つかもしれません。しかし、ここで一番言いたいのは、こうしたことに体系的な法や秩序を 求める べきではないということです。私は、アリストテレスを現代科学的なアプローチの始祖と認識しそれを嘆き悲しんだ、Pirsigの有名な本に出てくるパイドロスに共感を覚えます。

パイドロスは、アリストテレスが万物に名前を付けて分類することに多いなる喜びを感じていることを察した。…彼はそこに、歴史に現れた多くの自己満足的で無知なる教師の原型を見たのだ。この退屈な儀式、盲目的なルーティン、命名の永遠の反復により、生徒たちが持つ創造的な精神は無残にも葬り去られることになった。
Robert Pirsig著『Zen and the Art of Motorcycle Maintenance（禅とオートバイ修理技術）』

パイドロスの言い回しは、科学的手法に傾倒した読者からすると、少し大げさすぎるかもしれませんが、その中に真実が含まれていることも確かです。 型 や他の概念の創造的な使用は、確立された現代のルールや原理をしばしば打ち破ります。それらと調和しながらうまくやるためには、過去を振り返って方法を見つけるしかありません。きっと、型に関する歴史的な展開が助けになるはずです。

同様の立ち位置を取る人物に、哲学者のPaul Feyerabendがいます。彼は、せっかくの奇抜な（そして面白い）アイデアも、明晰さや正確さを追い求めることで、その思考の範囲が制限される（結果的に科学の損失となる）と説明します。

議論の条件を”明確にする”ことは、完全な理解が必要とされる懸案事項の補足的、かつ知られざる主要な特徴を暴き出すどころか、全く異なる領域の論理と常識を基礎とした既存の概念によって、それらを埋め尽くすだけである。…そして、この充填のプロセスを通じて、一般的な論理の法に従うことを余儀なくされる。

つまり、調査の過程が、既知の知識の狭いチャネル内へと導かれるため、根本的な概念を発見する可能性が大幅に低減されるのだ。
Paul Feyerabend著『Against Method（方法への挑戦）』（1975年）

型に関するプログラミング言語の記事を読んでいる時、上記の引用がよく頭に浮かびます。新しいアイデアは、確実に”修正”できる”技術的な欠陥”があるため、拒否されることがしばしばです。しかし、そうした修正を施してもアイデアを前進させるわけではありません。それどころか、既存の文脈の枠組みにアイデアを閉じ込めるだけです。さらに悪いことには、その文脈にふさわしくない部分は捨て去られることも多々あります。

Feyerabendが自らの立場を主張する時、彼は人道主義的な見地に立ちつつ、歴史的な事例を援用します。科学の歴史に目を向けた場合、（現在から振り返れば）大きな革新と言われるアイデアが、非科学的なアイデアとして当時は扱われ（、経験的予測の良好な視界は提供しないと思われ）ていたという事例がいくらでもあるのです。

ある程度の不確さがいいことだと主張するFeyerabendのような極端な視点を取る必要はもちろんありません。むしろ、（Feyerabendのように）科学全体について論じるより、（Lakatosのように）個々のリサーチプログラムについて論じるか、あるいは（Kuhnのように）リサーチパラダイムについて論じた方がいいでしょう。LakatosのリサーチプログラムとKuhnのリサーチパラダイムはどちらも、その初期段階が多くの場合において、不正確であり不完全であることを（そして、一般に認められた真実とは矛盾していることさえ）示しています。

というわけで、一歩引いた（しかし、恐らくより受け入れやすい）立ち位置として、 確立されたリサーチプログラム においては型の厳密な定義は求めるものの（例えば、関数型言語における集合ベースの型概念について話す時）、リサーチプログラムとして完全にまとまっていないものについて話す時は（例えばF#の型プロバイダや、TypeScriptまたはDartといった健全でない型システムの場合）、その厳密な定義は求めるべきではないという立場を取ることができるのではないでしょうか。

明確に定義された型なしでやりくりする

まとめると、 型 は狭い範囲に限定した場合、厳密な定義を伴って使用することはできますが、実のところ厳密な定義のある形式的な概念ではありません。では、特定のリサーチプログラムの範囲外で型を運用する場合、どのようにしたらいいのでしょうか？

私の提案の一部は、 エッセイの完全版 に書いていますが、残念ながらこの質問に完全に答えることはできません。ただ、厳密な定義を必要としない科学の哲学的な思考法はいくつかあります。また、これらの方法は、確立されたリサーチプログラムの狭く厳密な範囲内において運用する厳密なメソッドを補完できるはずです。

言語ゲームと型の使用法

用語の意味を理解する1つの方法は、それがどのように使われているかを見ることです。”意味の使用説”を唱えた有名な哲学者はLudwig Wittgensteinですが、彼は、言葉を使うことができる特定の文脈において繰り広げられる 言語ゲーム を通じて、私たちは意味を理解すると述べています。例えば「これはコンピュータです」と言う時、あなたは言語ゲームにおいて 直示的定義 を使っているのであり、そういった話し方に慣れ親しんでいる聞き手にとって、何がコンピュータであるかを示しているのです。

プログラミングや型に関して言えば、何が興味深い言語ゲームとなるでしょうか。考えられる一例が Expression problem です。このパズルを解くことで、システムの抽象化とエラーチェックのプロパティのいくつかが明らかになり、（Wittgensteinの個々の言語ゲームのように）型システムの具体的な視界が開けてきます。一方で、厳密な定義を必要としないシステムについて、興味深いことを私たちに教えてもくれるのです。もし私たちがこれとは違った同種の興味深いパズルを発見できれば、それを解くことによって、より広い意味で型を理解することが可能となるでしょう。

ステレオタイプと型の意味

私たちが取ることができる別の方向性に、Hilary Putnamの ステレオタイプ という考え方があります。異なるリサーチプログラムで作業している場合、作業している人たちは、それぞれ違う型の定義を持っている可能性がありますよね。一方、ある意味では、彼らは 同じこと を話しているとも言えます。Putnamによる意味の定義は非常に興味深いもので、複数のリサーチプログラムをカバーすることができるため、型について話すような状況下においては、とても便利です。

Putnamによると、意味の重要な部分を担うのが、実体の典型的または標準的な特徴を記述する ステレオタイプ です。その実体がどの種に属しているかを、その特徴によって識別します。ただし、ステレオタイプは厳密ではありません（どちらかというとヒューリスティックと言った方が近いでしょう）。Putnamの例に従うと、典型的なトラには縞模様がありますが、縞のないホワイトタイガーだってトラですからね。さて、ここで1つ未解決の疑問が残ります。型のステレオタイプ的な特徴とはどんなものなのでしょうか。あるものが型システムであることを、どうやって識別すればいいのでしょうか。

科学的実体と型による実践

前述の2つの哲学原理は型の意味に焦点を当てていますが、より実践的な態度で、厳密な定義の型なしに 作業 する方法を模索することも可能です。Ian Hackingは、このアプローチを用いています。過去の多くの事例を参考にしながら、興味深い仕事だからといって、複雑な理論が必要なわけではないことを示しました。 “科学の歴史において、理論的仮定を全く含んでいなくても、重要な考察は存在する。”

Hackingのメモに、（科学に関する私たちの見解を歪ませる）歴史書に出てくるのは理論家だ、という興味深い記述があります。 “理論を作り上げる人と実験者の間には、ある種の階級格差が存在する。…科学が制度化され出した頃から、私たちは理論への偏向を示し始めた。”

計算機科学への実験的アプローチに対する偏見にもかかわらず（エンジニアリングという言葉でさえ、一部のサークルではネガティブな意味を持つことがあるようです）、計算機科学のほとんどの領域は実験主義に基づいていると私は信じています。先に誕生した実験というアプローチは、後から出てきた”上流階級”の理論の背後で静かに身を潜ませている状態なのです。プログラミング言語の実験について、私たちが話し、公開できるような方法を見つけなければなりません。

私は 以前のエッセイ で、（一部の型の概念が、ある特定のシステムの構築にどのように役立つかということを示しながら）プログラミング言語の実験にケーススタディのようなものが利用できるかもしれないということを提案しました。また、スクリーンキャストの形式で発表できる Future Programming Workshop は、別の魅力的なオプションです。物理学におけるHackingの例を参照しつつ（あなたがどんな電磁気学の理論を信じているかは関係ありません）、 単極誘導モーターの の動きを観測することができます。

まとめ

このブログの投稿は、型に関する話題で起こりがちな誤解についての部分的な回答として書いた 以前のエッセイ から、鍵となるアイデアの一部を抜粋して紹介するものです。ついでにそのエッセイ（より多くのアイデアを紹介しているので、ぜひご覧ください）の概要を以下に記しておきます。

“型の定義とは何か？” この質問に明確かつ正確な回答を与えられれば、そこから生じる多くの誤解や無意味な議論を避けることができる。しかし、この質問に対して、そのような明確かつ正確な回答を持ってしまった場合、科学の前進を鈍化させ、”知識の成長を妨げ”、”調査の道筋を既知の狭いチャネル内に引き入れてしまう”ことにもつながりかねない。

つかみどころのない型の定義（そんなものは存在しない）を探し求めるより、形式的で正確な定義を必要としない型で作業ができるような革新的な方法を探し求めなければならないと私自身は信じています。特定のリサーチプログラムで実施される厳密なリサーチにこれを加えれば、きっと役に立つはずです。