title: Type algebra and Knuth's up arrow notation
body: <p>Reading through <a href="https://stackoverflow.com/questions/9190352/abusing-the-algebra-of-algebraic-data-types-why-does-this-work">this question</a> and <a href="http://www.haskellforall.com/2012/01/haskell-for-mainstream-programmers.html" rel="nofollow noreferrer">this blog post</a> got me thinking more about type algebra and specifically how to abuse it.</p>
  
  <p>Basically, </p>
  
  <p>1) We can think of the <code>Either A B</code> type as addition: <code>A+B</code></p>
  
  <p>2) We can think of the ordered pair <code>(A,B)</code> as multiplication: <code>A*B</code></p>
  
  <p>3) We can think of the function <code>A -&gt; B</code> as exponentiation: <code>B^A</code></p>
  
  <p>There's an obvious pattern going on here:  Multiplication is repeated addition, and exponentiation is repeated multiplication.  This led <a href="https://en.wikipedia.org/wiki/Knuth&#39;s_up-arrow_notation" rel="nofollow noreferrer">Knuth to define the up arrow</a> ↑ as exponentiation, ↑↑ as repeated exponentiation, ↑↑↑ as repeated ↑↑, and so on.  Thus, 10↑↑↑↑10 is a HUGE number.  </p>
  
  <p>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 <code>A↑B</code> simply be <code>[A] -&gt; B</code> and thus <code>A↑↑↑↑B</code> be <code>[[[[A]]]]-&gt;B</code>?</p>
  
  <p>Bonus points if you can explain what the <a href="https://en.wikipedia.org/wiki/Ackermann_function" rel="nofollow noreferrer">Ackerman function</a> would look like, or any of the other <a href="http://www.mrob.com/pub/math/largenum.html" rel="nofollow noreferrer">hypergrowth functions</a>.</p>