>>964
何を型といってるかによるけど違いはないよ。
高階関数がどこまで扱えるかどうかは言語によるけど。
ただ >>954 のように型を集合と考えるのに対して >>956 の挙げた
型を命題とする見方は typed lambda の応用に独特だと思う。
この辺のイントロでよくまとまってるのは >>951 の5章かな。
もっと平易なのがよければ冗長だけど↓
ttp://nicosia.is.s.u-tokyo.ac.jp/pub/essay/hagiya/7bits/shoumei_kata