型システム

[6] 関連: データモデル

いろいろな型

型論争

[14] {動的型付け言語 | 弱い型 | 型なし | データの型を重視} と {静的型付け言語 | 強い型 | 「入れ物」の型を重視 | 型推論マンセー} の派閥は数十年にわたって形を変えながら、論点を変えながら、 参加者を変えながら、 舞台を変えながら、よくわからない宗教論争を続けています。

[4] 型付き言語 vs 型なし (or 弱い型?) とかいう糞みたいな論争まだやってるのかwwwww 好きな方を使えよwwwwwwww 2023-09-08T14:28:06.700Z

[5] 型システム利用で向上した分の生産性を型論争で浪費してるだろwww

• [8] Xユーザーのかおるこたゃさん: 「なんかたくさん反応きてて怖いんですけど、私はRustの研究をしているので当然最近の言語はこの辺の問題が解決されていることを知っており、しかし初心者が最初に触れるであろう静的型付き言語は往々としてこういうつらさを抱えてるという話です。あと動的型付き言語へのヘイトスピーチやめてください」 / X, 午後3:38 · 2024年7月11日2024-07-11T06:38:29.000Z, 2024-07-11T12:54:12.000Z https://x.com/cordx56/status/1811288936398090557
  • [9] Xユーザーのかおるこたゃさん: 「胡乱なポストが拡散されて、強い言葉のリプ・引用が多く寄せられているのでとても気分が悪いです。」 / X, 午後3:59 · 2024年7月11日2024-07-11T06:59:17.000Z, 2024-07-11T12:54:12.000Z https://x.com/cordx56/status/1811294171514208716
  • [10] Xユーザーのかおるこたゃさん: 「一部の静的型付き言語の人、動的型付き言語をバカにするのは(本来おかしいが)許せるとして、動的型付き言語を使ってる人をバカにするのはライン越えだからな。人として最低限ができてないやつと議論する気はないよ。」 / X, 午後3:48 · 2024年7月11日2024-07-11T06:48:37.000Z, 2024-07-11T12:54:12.000Z https://x.com/cordx56/status/1811291489269592357
  • [11] Xユーザーのかおるこたゃさん: 「エディタ戦争とかよくネタにされてるけど、静的型付け/動的型付けもまぁよく燃えますなぁ。」 / X, 午後9:03 · 2024年7月11日2024-07-11T12:03:07.000Z, 2024-07-11T12:54:12.000Z https://x.com/cordx56/status/1811370633055601127

[12] この界隈昔から強い言葉で人格批判レベルまで含めてやり合ってる印象あるから怖いよなあ。

[13] 考えてみればボヘミアンと貴族の階級闘争もこれの亜種だな。

[15] Bringing Peace to the Galaxy - Externals, 2024-07-24T05:40:17.000Z https://externals.io/message/106453

• [16] (削除済みツイート)
  • [17] XユーザーのYukihiro Matzさん: 「@h_sakurai わざわざ私を殺さなくても、JavaScriptから(MSが)TypeScriptを作ったように、誰かがTypeRubyを作ればいいんですよ。TypeScriptが成功したようにTypeRubyが本家Rubyより流行れば、私が足を引っ張ってるかどうかは関係ないわけで。」 / X, 午後4:34 · 2024年10月1日2024-10-01T07:34:56.000Z, 2024-10-02T04:00:24.000Z https://x.com/yukihiro_matz/status/1841018946776154431
  • [18] XユーザーのYukihiro Matzさん: 「なんで自分好みの言語を得るために、私の言語を変えようとするのだろうか。他人の物を取り上げなくても、好みに合う既存言語を使うか、いっそ自分で作ればいいじゃんかよ。」 / X, 午後4:42 · 2024年10月1日2024-10-01T07:42:45.000Z, 2024-10-02T04:00:24.000Z https://x.com/yukihiro_matz/status/1841020913804013597

[19] 「型を明示すれば速くなります」って Visual Basic が30年前に実現していた世界で草、 未だにそんなメリット語って型の普及を目指す人がいるのかwwwww

[20] 最近は AI という新要素が加わってまた一段と型論争が賑わっているようだけれども、 言ってることは今までと何も変わってないのが笑えるよねえ。 ゴミみたいな論争が変わらずずっと続くってことは、 AI はトッピングで本質的にはやっぱりなんも変わらんのだろうねーw

[21] 近頃見られる新類型は、敵方を 「AI でわけもわからずコードを書かせてる馬鹿」 扱いして藁人形するパターンらしい。

型パズル

[22] 型パズルと次元解析 (単位が合うように掛け算する) って、どっちも

• 対象の中身を深く理解してなくても
• 許される組み合わせ/形の制約だけを見て
• かなりのところまで正解っぽいものを復元できる

[23] 物理でいうと、

• 欲しい量の次元を決める
• 手元の定数や変数の次元を見る
• 掛けたり割ったりして辻褄を合わせる
• 係数や細部は分からなくても、式の骨格はかなり当たる

[24] 型でも同じで、

• 欲しい型がある
• 手元の関数やデータの型がある
• どう合成すればその型になるか探す
• 実装の意味を深く考えなくても、項の骨格がかなり決まる

ということが起きる。

[25] しかも「わかった気になりやすい」ところまで似てる。 次元解析は、式の形が合った瞬間にかなり「理解した感」が出る。 でも実際には、

• 無次元定数が違うかもしれない
• 対数や指数が潜んでるかもしれない
• そもそも支配方程式や近似条件を分かってないかもしれない

[26] つまり、骨格は合ってても物理はまだ分かってないことが普通にある。

[27] 型パズルもそれに近くて、

• この API たちはこう繋がる
• この状態遷移は encode できる
• この invariant は型で表せる
• この関数はこのシグネチャになる

みたいなのが決まると、すごく「本質を掴んだ」感じが出る。 でも実際には、

• その関数が何を計算すべきか
• 業務ルールとして正しいか
• 期待する副作用をしてるか
• パフォーマンスが許容範囲か
• UX 的に妥当か

みたいな部分はまだ全然未解決だったりする。

[28] つまり両方とも、構造制約が強いので、理解の手がかりとしてはめちゃくちゃ強いのだけど、 そのせいで逆に 「制約を満たせた = 本質を理解した」と錯覚しやすい。

[29] もちろん次元解析は超強力だし、間違いを弾くし、式の形を導くのにも役立つ。 でも物理そのものではない。 同じように、

• 型はめちゃくちゃ強力
• 間違いを弾く
• 実装や設計の骨格を与える
• 合成可能性を見せてくれる

でも、プログラムそのものの意味全部ではない。

[30] だから型パズルにハマると、

「ちゃんと次元が合った式を作れた。よって現象の本質を掴んだ」

みたいなテンションになりがちで、 そこから

「ちゃんと型が合った。よって設計の本質を掴んだ」

に滑っていく。

[31] 要するに、

• 次元解析: 現象の「ありうる形」を強く制約する
• 型: プログラムの「ありうる接続と構造」を強く制約する

で、どちらも

• 正解への探索空間をめちゃくちゃ削る
• 骨格を与える
• 明らかにおかしいものを弾く
• うまくいくと深い理解っぽく見える

のだけど

• 係数・境界条件・支配方程式に相当するもの
• 実際の振る舞い・意味・仕様の細部

までは勝手には出てこない。

メモ