このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

圏の圏が閉圏であるならラムダ計算ができる

n個の型パラメータを持つ総称型は、C1×...×Cn→D という関手だと思ってよいだろう。総称関数は自然変換、あるいは自然変換を少し拡張した概念で定式化できるだろう。

世間で総称型/総称関数といっているものがすべてこのようにみなせるわけではないが、タチのいいものに限れば、関手と自然変換だと思ってもよい。

圏の圏Catはデカルト閉だから、そこで普通のラムダ計算ができる。このラムダ計算はタチの良い総称計算だと思っていい。別にCatに限る必要もなく、デカルト性が必要なわけでもない。モノイド閉圏になるようなレルム上では総称ラムダ計算ができるはずだ。