あなたの仕事にも使える考え方、型理論

型って堅苦しくない

いきなりの親父ギャグで読むのをやめないでください。
型理論とは嘘つきのパラドックスを代表する自己言及を含むパラドックスについてラッセルの考えた理論です。
ビジネスでは論理思考が必要だとか、論理的な議論とか言う癖に自己啓発本では一向に論理学の本が出ないか、出ても入門で終わるものばかりなのはどうしてでしょうね。そういうのに載ってない論理学や数学の話です。
それで型理論とは大論理学者のラッセルがそもそもパラドクスが起きるような文章は不適切なのだから排除しろと公園で子どものボール遊びを禁止する高齢者のように自己言及の文やその他問題が起きそうな文を作れないように決めたルールとその適用方法です。
「わたしは嘘つきです」と普通言わないだろう、述語が「嘘つきです」ならば主語にわたし等の一人称の単語は選べないというルールを入れることでパラドクスを回避できます。このように作れる文を制限して何も論理学に問題はないと蓋をしましたが、それでうまくいくでしょうか？
まあラッセルの努力も虚しく、ゲーデルの不完全性定理よりこの型理論をもってしてもパラドクスが起きる文章が作れてしまうことが証明されてしまいました。

いやダメじゃん。使えないじゃん、となると思うでしょうが、この型理論は中々どうして現代まで形を変えて生き残っている訳があります。入力したらダメな変数があるという考え方はある分野にとって、とても有効で安全性をもたらしました。そうプログラミングの世界では型理論の発展形、型システムは常識です。
オセアニアでは常識(ネットミーム)ということではないですが、型がプログラミングで重宝されるのは入力値を制限できるからです。プログラミングでは、プログラミングに限らず入力がその後の処理に不適切なものであればエラーとして扱って処理しないというのは大事なことです。プログラミングで例えるとわかりにくいので、別のもので例えていきましょう。

例えば食品工場だったら入力とは材料を機械にかけたり、機械を動かしたりが該当しますが、例えば材料の中に毒物が混入していたりしたらその後できる食品が毒物混入物になって人に被害を与えるかも知れません。
例えば洗濯機に衣服以外を入れないようにポケットの中を空にしなかったら故障するかも知れません。
例えば病気で足が勝手に動いてしまう人がいて運転中に足が跳ねて間違えてアクセルとブレーキを間違えたらどうなるでしょう。

上の例えから分かるように入力の制限が大事なことと分かってもらえたと思います。また入力制限他にも型理論は色々示唆をくれます。でも全然堅苦しくないですよね。

今記事は一旦この辺りでしめたさせていただきます。
続きはまた次回。