Чтение через этот вопрос и этот пост в блоге заставил меня больше думать о типа и, в частности, как злоупотреблять им.
В принципе,
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
be [[[[A]]]]->B
?
Бонусные баллы, если вы можете объяснить, как выглядит функция Ackerman или любой другой функции hypergrowth.