键入代数和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函数的外观或任何其他高增长函数,则可获得奖励积分.

Answer 1

在最明显的水平,您可以识别↑↑b

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

并且↑↑↑b就是

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

所以一切都可以用一些长函数类型来表达(因此有些长元组类型......).但我不认为对于熟悉的Haskell类型(基本上用...or或上面写的那些)来说,任意向上箭头符号都有一个方便的表达式?,因为我无法想到任何常见的数学对象对基础集的大小具有大于指数的组合依赖性(没有去递归数据类型,这太大了)...也许在组合集理论中有一些这样的对象？(你的问题似乎[对我来说]更多关于集合的大小而不是类型的特定内容.)

(您链接的维基百科页面已将这些对象连接到Ackermann函数.)