haskell - 类型代数和 Knuth 向上箭头表示法

Question

通读this question和 this blog post让我更多地思考类型代数，特别是如何滥用它。

基本上，

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

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

3) 我们可以将函数 A -> B 视为求幂:B^A

这里有一个明显的模式:乘法是重复加法，求幂是重复乘法。这导致Knuth to define the up arrow ↑ 为求幂，↑↑ 为重复求幂，↑↑↑ 为重复 ↑↑，依此类推。因此，10↑↑↑↑10 是一个巨大的数字。

我的问题是:函数↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑如何用代数数据表示类型？看起来 ↑ 应该是一个具有无限个参数的函数，但这没有多大意义。 A↑B 就是 [A] -> B，因此 A↑↑↑↑↑B 就是 [[[[A ]]]]->B？

如果您能解释 Ackerman function 的含义，可加分看起来像，或任何其他 hypergrowth functions .

Answer 1

在最明显的层面上，您可以通过以下方式识别 a↑↑b

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

a↑↑↑b 只是

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

所以一切都可以用某种长函数类型来表达(因此是一些非常长的元组类型......)。但我认为就熟悉的 Haskell 类型(的基数)而言，没有一个方便的表达式来表示任意向上箭头符号(除了上面用 ... 或 ↑ 编写的类型之外) )，因为我想不出任何常见的数学对象对基础集合的大小有大于指数的组合依赖性(不使用太大的递归数据类型)......也许有组合集合论中有一些这样的对象吗？ (在我看来，你的问题更多地是关于集合的大小，而不是特定于类型的问题。)

(Wikipedia page you linked 已将这些对象连接到阿克曼函数。)