Type algebra and Knuth's up arrow notation

Question

Reading through this question and this blog post got me thinking more about type algebra and specifically how to abuse it.

Basically,

1) We can think of the Either A B type as addition: A+B

2) We can think of the ordered pair (A,B) as multiplication: A*B

3) We can think of the function A -> B as exponentiation: B^A

There's an obvious pattern going on here: Multiplication is repeated addition, and exponentiation is repeated multiplication. This led Knuth to define the up arrow ↑ as exponentiation, ↑↑ as repeated exponentiation, ↑↑↑ as repeated ↑↑, and so on. Thus, 10↑↑↑↑10 is a HUGE number.

My question is: how can the function ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑ be represented in algebraic data types? It seems like ↑ should be a function with an infinitite number of arguments, but that doesn't make much sense. Would A↑B simply be [A] -> B and thus A↑↑↑↑B be [[[[A]]]]->B?

Bonus points if you can explain what the Ackerman function would look like, or any of the other hypergrowth functions.

Answer 1

At the most obvious level, you could identify a↑↑b with

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

and a↑↑↑b is just

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

so everything can be expressed in terms of some long function type (hence as some immensely long tuple type ...). But I don't think there's a convenient expression for an arbitrary up-arrow symbol in terms of (the cardinality of) familiar Haskell types (beyond the ones written above with ... or ↑), since I can't think of any common mathematical objects that have larger-than-exponential combinatorial dependencies on the size of the underlying sets (without going to recursive datatypes, which are too big) ... maybe there are some such objects in combinatorial set theory? (Your question seems [to me] more about the sizes of sets than anything specific to types.)

(The Wikipedia page you linked already connects these objects to the Ackermann function.)