类型代数和Knuth的上箭头符号

Question

阅读这个问题和这篇博客文章让我更加思考类型代数，特别是如何滥用它。

基本上，

1）我们可以将Either A B类型视为加法：A+B

2）我们可以将有序对(A,B)视为乘法：A*B

3）我们可以将函数A -> B视为指数：B^A

这里显然有一个模式：乘法是重复的加法，指数是重复的乘法。这使得Knuth定义了上箭头 ↑ 作为指数，↑↑ 作为重复指数，↑↑↑ 作为重复的 ↑↑，以此类推。因此，10↑↑↑↑10是一个极大的数字。

我的问题是：如何在代数数据类型中表示函数↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑？看起来↑应该是带有无限数量参数的函数，但这并没有太多意义。那么A↑B是否简单地为[A] -> B，因此A↑↑↑↑B将是[[[[A]]]]->B？

如果您能解释Ackerman函数或任何其他超增长函数的样子，将获得额外的分数。

- Mike Izbicki

---

我认为这个问题无法以真正的规范方式完成。将aˣ与x->a进行识别已经有点特例化，只是恰好在aˣ⁺ʸ和aˣ+aʸ以及aˣʸ和(aˣ)ʸ之间具有同构性。但这些同构并不完全是规范的。 - leftaroundabout

Answer 1

在最明显的层面上，你可以将a↑↑b与

((...(a -> a) -> ...) -> a)  -- iterated b times

而 a↑↑↑b 就是

(a↑↑(a↑↑(...(a↑↑(a↑↑a))...))) -- iterated b times

因此，一切都可以用某些长的函数类型（因此作为某些极长元组类型...）来表示。但我认为在熟悉的Haskell类型（除了上面用...或↑编写的类型）中，没有方便的表达任意上箭头符号的表达式（在基础集合大小上具有超指数组合依赖关系的常见数学对象不存在，除非使用递归数据类型，这太大了）...也许在组合集合论中有一些这样的对象？ （你的问题似乎[对我来说]更多地涉及集合的大小而不是特定于类型的任何内容。）

（您链接的维基百科页面已经将这些对象与Ackermann函数联系起来。）

- Fixnum