2008-09-13 圏の圏が閉圏であるならラムダ計算ができる 圏一般論 プログラム意味論 n個の型パラメータを持つ総称型は、C1×...×Cn→D という関手だと思ってよいだろう。総称関数は自然変換、あるいは自然変換を少し拡張した概念で定式化できるだろう。世間で総称型/総称関数といっているものがすべてこのようにみなせるわけではないが、タチのいいものに限れば、関手と自然変換だと思ってもよい。圏の圏Catはデカルト閉だから、そこで普通のラムダ計算ができる。このラムダ計算はタチの良い総称計算だと思っていい。別にCatに限る必要もなく、デカルト性が必要なわけでもない。モノイド閉圏になるようなレルム上では総称ラムダ計算ができるはずだ。