- "How to duck type? - the psychology of static typing in Ruby" (邦訳: ダックタイピングの手引き？ - Rubyでの静的型付けの心理学) という記事は意味不明文書なので読む価値はありません (訳は良くできています)
- 「静的ダックタイピング」という用語は「原動機なしバイク」のようなもの。
近年(FIXME)、「ダックタイピングなんたらの静的型けの心理学」という呟きが Twitter 上で散見される。 筆者ら(FIXME)には何のことかサッパリ判らない、狂気すら感じる呟きであったので気になってサーベイ(ggrks) してみたら邦訳記事があった。邦訳記事を数行読んでもサッパリわからないのでオリジナルを読んで見たところ、 これは訳が悪いのではなく(いや訳は実際大変良い)、単に元記事がトンデモ系なだけであった。 トンデモ系文章を読んでフンフンとうなづきながら何か判ったトンデモさんが増えないように釘を刺さねばならない。
静的型システム、静的型検査、静的型推論、とにかく静的型ナンタラというものは型を使った 静的なプログラム検証技術である。
静的なプログラム検証、とは、プログラムを実際に動かさずにプログラムに何か良い性質があるか どうか検査することだ。何か良い性質、とは、これは場合によっていろいろだ。プログラムを実行しても Segmentation fault が絶対起こらないとか、一般保護例外が絶対起こらないとか、デッドロックが起こらないとか、 必ず金が儲かるとか、死後裁きに遭わないで済むとか、そういう話である。君が良いと思う性質を 静的に検証できればいいですね。
静的な検証と言っても、じっとプログラムのプリントアウトを見台に置いて座すこと数時間、 クワッ！「見えたァあああ、これは安全！」タツジン！！とかそういう事ではない。 実際のプログラムを何かしら大幅に簡略化したものをある意味動かしてみてそれが上手くいっているかどうか 確かめるのだ。この簡略化にもいろいろレベルがある。凄く簡単にすれば検証もすぐ済むから凄く静かだけど 大したことは検証できない。元のプログラムとほとんど同じであれば何かすごいことが検査できるかもしれないが 検証にも時間がかかる。経済だよキミ。コスト対効果ってやつだ。
例えば一番簡単な静的なプログラム検証はプログラムを実行する前にパースしてみて文法があっているかどうか 調べることだ。これはあまりに簡単すぎて普通は静的検証とは言わないのだが、ロケットを飛ばしてみて月着陸寸前に ここの何行目にミススペルがあったのでプログラムの実行を中断しますテヘッっという通信をロケットから 受け取りたくなければ、まあ、費用もかからないし、事前にやっといて損はないだろう。
凄くコストの掛かる方の静的検証はモデル検査とか呼ばれる奴が代表。要はプログラムを実際に動かすのだが、 さすがにそのまま動かしていたらキリが無いので色々と簡略化する(連中はカッコよく、抽象化する、と言っている)。 例えば整数は無限にあるから整数に関するプログラムの検証は虱潰しにではテストしていられない（無限である）が、 整数を素数か合成数かと大まかに二つに抽象化してやるとうまくするとそのレベルでは虱潰しが有限で現実的な物になる、 かもしれない。で、うまくすると…この関数は必ず合成数しか返さないので東工大生が狂喜乱舞しないので会社は黒字になる、ということが証明できたりする。抽象化の度合いによっては検査に膨大な時間とメモリ、つまり金がかかる訳だが、どこまで頑張るかは、世知辛いけどお財布とか、マジでコケた時にどれくらい損が出るかとかを考えることになる。
静的型検査というのはこの中間位の検査方法だ。型検査ではプログラムを抽象化して安価に実行する、 というよりはむしろプログラムの部品部品の型を見て組み合わせ部分の整合性を確認する。 外科手術で使う麻酔ガスを始めとするガス管のつなぎの部分はガスの種類に寄って異なってデザインされており、 間違ったガスが -- 例えば麻酔ガスの所に二酸化炭素が -- 流れないようになっているのだが、 これに似ている。 ボンベ、チューブ、マスク、それぞれ接続するところが合っていれば、正しいガスが流れてくる。 とりあえず接続してみてから医者が（看護師でもいいですけど、まあ、高職位が責任を取らないとネ！）試しにマスクを被ってみて、 ペロッ、これは麻酔ガs zzzzz...とか一々やらなくても安全が保証できる。 コストがかからない。 実際にガスを吸わないところがキモなのでこれは覚えておいて欲しい。 (一方の動的型検査ではチューブの形を見るのではなく、実際にガスを吸ってみる。)
静的型検査が剛直であるというのはそういう点だ。どう見たって安全じゃないですか、 ほら、ボンベから患者の口までこう流れてるんだから麻酔ガスしか流れないっすよ？ 決まった規格のプラグ付きでないと使えないとか面倒くさくないっすよ？ とは言ってもこれは規則で決まっているんだ、規則は規則、キミも人事に睨まれたくは無いだろう？ 悪いようにはならないヨ。
例えば次のようなコードを大抵の静的型システムは排除する:
10 * (if true then 10 else "hello") // 何の言語かは知らない。お前にも読めんだろ？
どう見たって安全じゃないですか、ほら、条件節は true なんだから掛け算の右辺は常に整数っすよ？ でも排除するのである。規則は規則、キミも人事に睨まれたくは無いだろう？これだ。
大抵の静的型システムと書いたがもちろんキミは頭が素晴らしくいいのでちゃんと空気を読んで if e0 then e1 else e2 の型は e0 が常に true であることを発見した場合、e1 の型であって e2 の型は無視する、 みたいな静的型システムを作ることができますよね？私は面倒なのでやらないけど。
もちろんガス会社が麻酔ガスのボンベに水素ガスを詰めていたらどうしようもないが、 それはこの型システムで抑えるべき安全性ではない。 (これはどんな安全性に関しても同じ事だ。幾ら静的プログラム検証でプログラムの正しさが検証されていても、 今まさにベテルギウスが爆発してガンマ線バーストでメモリ内容が吹っ飛んでプログラムがおかしくなることはある。が、もちろんそれは検証の責任ではない。)
また、このプラグの形による静的安全性は、流れるガスの種類が想定ないであることしか保証しない。 ガス圧が100気圧くらいで患者が風船のようにボン！となるかもしれないがそれはもちろん保証外である。 ガス圧も静的に保証したいなら圧力調整弁を買いなさい。破裂した患者から訴えられるのが嫌で、 調整弁を買うお金があるなら。
ついでだから、求められる安全性というものは相対的なものだという事も言っておこう。 例えば、ボンベ、チューブ、マスクのプラグの形が合っていなければ使えないという安全性のデザインは 野戦病院では全くの邪魔でしかないかもしれない。
普通の街の病院、ボンベ、チューブ、マスクのプラグの形が合っていなければ使えないはずのところでも、 ガスを間違えて患者が死んだり植物状態になったりすることがある。 バカが間違ったプラグでもよく噛んでから無理やり力技でハメて使ってしまうからである。 手術を受けるのが怖くなりましたか？静的型検査にもこういうのがある。
型を使って静的に検証したので、必ず(CPUにバグがあるとか飼い猫がマシンの上でおしっこをしたとか、 想定外の自体が無い限りは)何か良い性質が保証されている場合は、強い型付けがされている、などと言う。
一方、型を使って静的に検証したので、まあ、大抵、何か良い性質があるんですが、 たまに、ほら、ね？わかるでしょう、あなたもオトナだ。金か？金が欲しいのか？ みたいなのは弱い型付けという。 要するに気休めでしかない。剛力(あやめではない)がいる病院の麻酔システムはプラグがちゃんとしていても 弱い型付けしかされていないかもしれない。 基本的に弱い型付けは何の保証にもならないので、普通の人間は相手にしない。 弱い型付けは弱い型付けしか無い言語を使わされている人間があれこれ悩むものである。 キミはもちろんそういう人間ではないね。えっ？オトナ？あ、そう。
一方動的ナンタラとは。動的検査というのはプログラム実行中に何かしら良い性質が保たれていることを検査する。 兎に角プログラム実行中に何か調べて条件分岐すりゃあ動的検査と言えんこともないので、ここは動的型検査に 限って話す。
動的型検査ではプログラム実行中にプログラム内を流れる実際の値の型を見てそれが今からやる演算に対して 使えるものかどうか確かめる。麻酔ガスのマスクの所で手術中、本当に麻酔ガスが流れているかどうか、 常に味見をするようなものである。医師（か看護師）は窒息するかもしれないが患者の家族からは訴えられないし、 医師（か看護師）は交換が効くアセットである。もちろん理事長のあなたは交換が効かない。そういうものでしょう？
動的型検査が柔軟だというのはそういう点だ。野戦病院では資材が足りないからプラグの形なんかでチューブやら なんたら複数揃えてられない。だから適当につなぐ。適当につないでもどこかクリティカルな所で実際に流れてくるやつが安全かどうか確かめればいいわけだ。野戦病院では理事長はいないし、医師や看護師が吸ってたら困るから、誰が他人が試しに吸うことになるが誰が？ お察しください。
例えば次のようなコードを大抵の動的型システムでは何の問題もない:
10 * (if true then 10 else "hello") // 何の言語かは知らない。お前にも読めんだろ？
掛け算を行うとき、動的型付き言語では必ず引数が数値であることを動的型検査によって確認するはずだ (その言語が 2 * "こんにちは" = "ぼくあひるちゃん！こんにちはこんにちは！！" という 大変ユニイクな文字列の掛け算概念を提唱していない限り。 筆者ら(FIXME)はパなんとかとかルなんとかという言語の事は知ってるから指摘不要)
だらららら(何か埋草を書きましょう)
そういう見切り発車は困る、という場合はテストをやる。テストの方法にはいろいろある。各部品に分けたテスト はユニットテストと言う。小部品に分けてテストするのでテストすべき組み合わせが減りコストが下がる。 ユニットテストが終わった小部品を組み合わせて全体として上手く動くのかを見るのが結合テスト。 まあこの辺は私は詳しくない。
筆者ら(FIXME)は静的型検査と動的型検査のどちらが良いのかを主張しない。 まあ、基本的に静的方検査の方が理論とか難しいのでカッコイイ、というのはあるが…
静的型付き言語を使っていても、全ての保証したいこと、特にプログラムを動かせば私が大金持ちになってイケメンになっている、とか、が静的型システムで保証できるわけではない。 むしろ静的型システムで保証できることは非常に限られている。その上、保証したいことを強くした場合、 型システムが非常に難解になったり、プログラムに沢山型を書かなくてはいけなくなったり、 いろいろと使いにくくなってくる。 「静的型ぁ？あいつら静的型で強い安全とか言ってるけど何が保証できるってんだよ？馬鹿？」 とか仰る静的型付けの無い括弧の多い言語使用者がままいらっさるが、そういう意味である。 そんな時は静的型付き言語使用者ももちろん動的な検査を行う。それは文字通り動的型検査と呼ばれたり、 プログラム中でプログラムの型が扱えないような言語では適当な条件分岐を行なって調べる。
筆者ら(FIXME)は、まあプログラムが型アノテーションでややこしくなったり、 プログラマが PhD を取らない限り読めない型が出てこない限りは、 静的型で確かめられることは静的型で確かめたらぁ？残りは動的でいいっしょ、という立場である。
- "How to duck type? - the psychology of static typing in Ruby" (邦訳: ダックタイピングの手引き？ - Rubyでの静的型付けの心理学) という記事は意味不明文書なので読む価値はありません (訳は良くできています)
- 「静的ダックタイピング」という用語は「原動機なしバイク」のようなもの。