ニコニコ大百科

プログラム言語は型を対象、関数を射とした圏を成すという説やね
圏になれば関手により大概の「素性のいい」数学的操作と対応付けられるし素性のいい圏はだいたい集合の圏になるので扱いやすい
仕様のせいでそうはならんやろとなることがあるみたいだけど

ニコニコ大百科にカリーハワード同型対応があるとは。
このあたりの類似性からどこかの天才が何かを閃いて、プログラミングの概念自体を一新するようなパラダイムシフトが何か起きないかと10年以上前から待っているのだけど何も起きない。