はじめてのかたりろん

最近生活していくうえで、型理論が必要になってきたので、若干勉強したのだった。
まー、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:「読まない」と同じ意味