この質問とこのブログ投稿を読んで、型代数、特にそれを悪用する方法についてもっと考えるようになりました。
基本的、
Either A B1)型は足し算と考えることができます:A+B
(A,B)2) オーダーペアは乗算と考えることができます:A*B
A -> B3) 関数は累乗と考えることができます。B^A
ここで起こっているのは明らかなパターンです: 乗算は足し算の繰り返しであり、べき乗は掛け算の繰り返しです。これにより、クヌースは上向き矢印↑ を累乗、↑↑ を累乗の繰り返し、↑↑↑ を ↑↑ の繰り返しなどと定義しました。したがって、10↑↑↑↑10は巨大な数です。
私の質問は: 関数 ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑ を代数データ型でどのように表現できますか? ↑ は無限個の引数を持つ関数であるべきだと思われますが、それはあまり意味がありません。A↑B単にそうで[A] -> Bあり、したがってA↑↑↑↑Bそうでしょうか[[[[A]]]]->B？