いかにして『型』は人を救うか。【ウィトゲンシュタイン / 千葉雅也】
話をあらためてシンプルにします。意味からリズムへ、というのがこの本です。
リズムというのは、デコボコなのでした。
デコボコというのは、要素がどう並んでいるかです。
とにかく「並び」が大事なんだ、とも言える。千葉雅也『センスの哲学』[1]
三・三三
論理的構文論においては、断じて記号の意味が役割を果たすようなことがあってはならない。
論理的構文論は記号の意味を論じることなく立てられねばならず、そこではただ諸表現を記述することだけが前提にされうる。三・三三一
この見解に立つと、ラッセルの「タイプ理論」の内実が見えてくる。
ラッセルの誤りは、記号の規則を立てるのに記号の意味を論じなければならなかった点に示されている。ウィトゲンシュタイン『論理哲学論考』[2]
概要と結論
なぜ、JavaScript では、TypeScript なのか。
もっと、一般化すると、なぜ型が必要なのか。
本で読んだとかではなく、人に聞かれたとき、即答できるような答えがいままでなかった。
しかし、最近、ある考えを思いついたので、思考の整理がてら書いてみようと思う。
型のメリットとは何か。
結論から、書くと、
型があると、エディタでのコードの編集に集中できるようになる。
なぜなら、コードの整合/不整合を「意味」から、記号の「並び」で扱えるようになるから。
である。
順を追って書く。
型がない場合
私が初心者のとき、JavaScript のコードを書いていたときに、
「よし書けた！」と思って、いざブラウザを見ると、エラーで動かないということが、ままあった。
// 例
let obj = { name: "Alice" };
console.log(obj.age.length);
// ブラウザのエラー:
// Uncaught TypeError: Cannot read properties of undefined (reading 'length')
// at <anonymous>:1:21
型のない状況で、こういうエラーに対処するには、どうすればよいのか。
- コードを読んで、意味を都度、頭の中で、考える。
-
objには、name以外のプロパティがないんだな。だから、objにname以外にアクセスするプロパティを書いてはだめだな。
-
- 実際にブラウザを見て、エラーが出ていないか確認する。
まず、コードの意味を都度考える必要がある。
そして、人間が一度に、認識できる情報量には、当然限界があるので、すべてを把握できない。
だから、ブラウザなどで、動作確認する必要がある。
まとめると、頭の中でそのプログラムの意味考える必要がある。
そして、実際に動作を見る必要もある。
つまり、高頻度で、複数の箇所に意識を向ける必要があるのだ。
必然的に、認知負荷が高くなる。
型システムとは何か
プログラミングの型の原点は、バートランド・ラッセル（哲学者、論理学者、数学者）の提唱した型理論がもとになっている。
この型理論は、ラッセルが、「ラッセルのパラドックス」という数学の集合論上の問題を解消するために創始したものだ。
さらにいえば、ラッセルが、ゴットロープ・フレーゲ（哲学者、論理学者、数学者）の著書『算術の基本法則』の公理系の矛盾を発見した。
その矛盾が、「ラッセルのパラドックス」だ。
フレーゲは、自身の著した『算術の基本法則』の公理系にある、矛盾=「ラッセルのパラドックス」を解消できなかった。
ラッセルのパラドックス
型とは、簡単に言えば、規則をもった、データの種類である。
上のパラドックスの解消は、非常に簡単に言えば、
規則が生まれ、その規則によって、矛盾が発生しなくなる。
Wikipedia からの引用で大変恐縮だが、
Wikipedia の型システムの定義を引用する。
（型システムは）プログラムが計算する値の種類に従って句（phrase）を分類することで、
そのプログラムがある動作をしないことを証明する扱いやすい文法的手法である。 (Pierce 2002)[3]
型のメリット
より根源的に言えば、型は、プログラミング言語という言語世界において、
「ラッセルのパラドックス」を起こさせないためにあるともいえる。
だが、これは私の手に余る話なので、ここでは深く立ち入らない。
作業者目線で考えると、型のメリットは、以下のように、いえる。
コードの整合/不整合を「意味」からではなく、記号の「並び」で検出できる。
この「並び」というのは、千葉雅也氏の『センスの哲学』での言葉遣いから、使わせていただいた。
この「並び」で解決するというのは、「型」にかぎらず、「静的解析（static program analysis）」の神髄であろう。
この結果、
「意味」ではなく、記号の「並び」のレイヤーで、コードの整合/不整合を制御できる。
人間が脳で、「意味」を考える手間が減り、認知負荷が減る。
ということになる。
つまり、機械的かつ自動的に検出できるということだ。
具体的には、エディタのサジェスチョンや、CLI の静的解析で、機械的、自動的に、文法的にコードの誤謬を検出できる。
これによって、頻繁に、コード自体の意味や、実際の動作など多方面に意識を向ける必要があるものが、
エディタや、CLI などに、注意をむければよいということになる。
つまり、
型があると、エディタでのコード編集に集中できる
のだ。
実例
上記の例であげたコードは、「TypeScript - VS Code」 の環境だと次のようなエラーがでる。
蛇足
昨日公開したこちらの記事もよろしくお願いいたします 🙇
冒頭のウィトゲンシュタインの言葉について、何も触れずに最後まで来てしまったが、
ウィトゲンシュタインも、「意味ではなく、並び」という話をしているのだと思う。
-
千葉雅也『センスの哲学』(文藝春秋)2024 年 第 5 章 https://books.bunshun.jp/ud/book/num/1639182700000000000W ↩︎
-
ウィトゲンシュタイン、野矢茂樹 訳『論理哲学論考』(岩波文庫)p.34 ↩︎
Discussion