■
やすみがおわるよ！
考察もしないし感想も書かないやつがオタを名乗るんじゃねぇ！
■
帰ってきたので、久し振りに自炊。
ひとりぐらしが最適化されすぎると、自分の料理が恋しくなるという風潮があり、まあ、なんだかんだ。
僕の料理における必勝法は、「しょうゆかけて火を通せば、なんかできる」というものであり、しょうゆは偉大だと思うんだ。
みりんとか、料理酒とか、別に無くてもわからないよね、というか、あれが食品にどういう効果をもたらしているのか知らない。そもそも料理酒とみりんの違いがわからない。
ほんとのみりんを選ぼうと言われたところで、そもそもみりんがなんなのかわからない！
http://ja.wikipedia.org/wiki/みりん
あれ？やっぱりみりんは酒だよな…（最近Wikipediaに頼りすぎ）。じゃあなんでアレとかアレとか、はみりんと料理酒を一緒に入れるんだろうか。謎。
はじめてのかたりろん
最近生活していくうえで、型理論が必要になってきたので、若干勉強したのだった。
まー、JavaのGenericsとかってF subだなーとか、その程度を理解したと思ったら
http://d.hatena.ne.jp/sumii/20060404/1144111484
問題となった（なったか？）例のアレのところにそのまんま書いてあった。
たとえばJavaのgenericsにはF-bounded polymorphismが入っていますが、これなどはまさにTAPLに書いてあるSystem FやF-subの話が元にあります
人の書いた文書をちゃんと読んでない証拠だと思う。
http://lambda-the-ultimate.org/node/1430
ふむ、関連してそうだな…気が向いたら読む（=「あとで読む*1」と同じ意味）
System Fってすっごいむずかしそうだなー、と思ってたら、そんなに難しくなかった。
まず、「型付きλ」というのがあって、これは、
f :: A -> B
という型の関数と、
a :: A
というなんか値があったら、
f a
は、
f a :: B
という型になりますよー、っていうそれについて、やたら細かく書いてある、というだけ。
ただ、この、「型付きλ」だけだと、こういう↓
id a = a
多相型が表現できない。
ので、型の変数を使えるようにしたのが、「System F」。それだけ。
もっとなんか凄い巨大なシステムのことだと思とったよ。「System F」などというシヴイ名前を付けているのが、僕の誤解を招く原因になったのだと思う。
（なお、僕は、大変大雑把に理解したところで理解を停止する傾向があるので、あんまり信用しないこと）
System Fは、型の変数に型をそのまま束縛するしかできない、けど、まあ、なんか色々束縛する条件を付けられるようにしたのがF sub。（←いくらなんでも適当すぎる）
OCamlのObjectiveがモロにそれっぽい。JavaのGenericsが多分そんな感じ。upper boundとかの用語がここらへんっぽい。
とりあえず、読んでる本は、「型理論」とかいう本と、問題となった（なったか？）TAPL。
どっちも買ったときは、「多分積むなー」と思ってたんだけど、予想どおり、積んであったというなんかそんな。
たまに、こうやって読んだりしてしまうから、「積むのわ悪くないんだよ」とかいうようなエクスキューズ（てなに？）が生まれてしまって罪悪感が減って、僕は今日も積むのだと思った。
とりあえず、「型理論」のほうが、ちょーーー簡潔にしか書いてなくて、いや、ほんと、もっと説明してよ！て感じなので、TAPLで説明を読みつつ、型理論のほうで日本語の対応を読みつつって感じで。
*1:「読まない」と同じ意味
■
死ぬわけにいかないので書く。「関数型言語」ってなんじゃとかに関係したりしなかったりする話。
「関数型言語」という表現は、何を言いたいかわからなくもないけど、よくわからない表現であると思う。
何をもって関数型言語とするのか？何ができたら関数型言語になれるのか？mapが書けたらよいですか？（ここで、Cで書いたmapをひっぱり出してくるとよい）
でも、定義があやふやなわりに、関数型言語というのは、それなりの共通認識はあるように思う。
と、いうあたりは、宗教戦争になったりせずに、それなりに仲良く区切ってもらえることと思う。（違う、という人も、ここはぐっと我慢してあげてください）
この区切りはなんじゃろなー、と、思ったときに、「型システムが、理論から始まってるか、既にあるものに後付けで理論が付いてきてるか」というような区切りはそれなりにしっくりくるように思った。
ここで、型についてそういうふうに考えると、みっつの区切りができることと思う
- あとづけで型理論がある。もしくは、型システムはあるけど、理論はよくわからない（Cの子供たち…とか書くとALGOLの人達に怒られるところ）
- 型理論ありきで型システムがある
- 型が適当（型が無い…とか書くと偉い人達から怒られるところ）
さて、ここらへんの話から、無理矢理LLの人気の秘密を暴いていく話へと路線変更していこう。
型理論とかをちゃんとやり始めると、ちょろっとなんかあるたびに、「今ある型システムを基盤固めして、その上に拡張を考える、んで、そこらへんがちゃんと動くのを証明」とかっていうのが行われてて大変そうというのが伝わってくることと思う。
例えば、上で書いた"F"だと、型を作る型…C++でいうtemplateのようなもの…を表現できないので、さらに、拡張する必要がある。これをやり始めると、пとかの文字が出てきたような気がして、僕の限界を越えたように感じたのだった。
そうすると、「C++では既に実現されてるし、ボクはこんなにもそれを扱えるのに、なんで、こんなややこしい理論をわざわざ勉強する必要が？既にあるのを使えばいいじゃなーい」、と、いうような考えになってしまうわけだ。
…けど、やっぱり、それだと、やっぱり無理があって、色んな概念を綺麗に分割しないで、いっしょくたにして扱った結果として、誰にもわからないC++のテンプレートの仕様ができあがったのでした。
まあ、これはどっちが良いかは難しいところで、ちゃんと理論を組み立てつつ、じわじわとやっていったら、C++の型システムのような強力な型システムが生まれるのは大分遅れてただろうし（今もC++以外生まれてない？D？素敵なHaskellの家族達が力を合わせればあるかも）、ましてや、それが、実戦で使われてるコンパイラの機能として当たり前に実装されている（か、どうかはきわどいけど）、なんてことはなかなか難しかったのではないかと思う。
理論に寄りすぎてもいけないし、実践によりすぎてもいけない…って、普通に情報量0な結論じゃないか。
（情報量0の結論の例 : 時と場合を考えて使いわけよう。相手の事情を理解して、最善の結果が生まれるよう努力しよう）
と、いうわけで、道は、「うだうだと理論を確実に組み立てていく」「いきあたりばったりで必要な機能をくっつけていく。必要以上に複雑になっても知らん」のどちらかしかない…ほんとうか？
そこで、型の弱い子の出番なんじゃないかと。
型の弱い子ならば、「実行時にテンプレートっぽいクラスから似たクラスを大量生産」とか、あっさり実現できちゃう！
複雑ですか？全然そんなことないです！クラスもオブジェクト！ふつーのオブジェクトとして扱ってあげれば問題無いですぅー。
そう！彼らは、型の偉い人達がうんうん唸りながら（かどうかは知らない）いかにして矛盾無く柔軟なシステムが作れるか…を考えてるところを、「型チェックをパスする」という超ウル技を使うことによって、あっさりと通過するのである！
彼らは気が向いたら、Objectクラスを弄れば、システム全体を簡単に変更できる！とか喜ぶような鬼畜な奴らなのである！
ややこしい理論もややこしい実装もいらない！必要なのは、実行時にシンボルテーブルを書きかえることだけ！たったそれだけで柔軟なシステムが！あなたのもとに！
その代償は、型安全が失われるのと、実行効率が落ちるのとのふたつ。それは、引き換えに値する代償なんだろうか。
いや、もっと大事なものが失われてるよ！処理系の実装がつまらないんだ！
型の弱い子の処理系は、最適化とかやり始めたら知らんけど、動かすだけでよいんだったら、大体見当付いちゃうんだよなー（とか書くと、実際試してもないのに適当なこと言わないようにと怒られる）。
まとめ: 型の弱い子は実装がつまらないのでどうでもよい（僕の中で）
